Skip to content

Commit

Permalink
chore: adapt to multiple goal linter 2 (#12361)
Browse files Browse the repository at this point in the history
A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.
  • Loading branch information
adomani committed Apr 30, 2024
1 parent 335470e commit fe96aa4
Show file tree
Hide file tree
Showing 87 changed files with 613 additions and 562 deletions.
5 changes: 4 additions & 1 deletion Archive/Wiedijk100Theorems/BirthdayProblem.lean
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,10 @@ theorem birthday_measure :
· rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
rfl
rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff]
rotate_left; (iterate 2 right; norm_num); decide; (iterate 2 left; norm_num)
rotate_left
iterate 2 right; norm_num
· decide
iterate 2 left; norm_num
simp only [Fintype.card_pi]
norm_num
#align theorems_100.birthday_measure Theorems100.birthday_measure
Expand Down
6 changes: 3 additions & 3 deletions Archive/Wiedijk100Theorems/BuffonsNeedle.lean
Original file line number Diff line number Diff line change
Expand Up @@ -284,9 +284,9 @@ lemma integral_min_eq_two_mul :
∫ θ in (0)..π, min d (θ.sin * l) = 2 * ∫ θ in (0)..π / 2, min d (θ.sin * l) := by
rw [← intervalIntegral.integral_add_adjacent_intervals (b := π / 2) (c := π)]
conv => lhs; arg 2; arg 1; intro θ; rw [← neg_neg θ, Real.sin_neg]
simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi,
intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg,
(by ring : -(π / 2) + π = π / 2), two_mul]
· simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi,
intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg,
(by ring : -(π / 2) + π = π / 2), two_mul]
all_goals exact intervalIntegrable_min_const_sin_mul d l _ _

/--
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/Algebra/Lie/Weights/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -363,7 +363,8 @@ lemma mem_posFittingCompOf (x : L) (m : M) :
obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
exact this n k
intro m l
induction' l with l ih; simp
induction' l with l ih
· simp
simp only [lowerCentralSeries_succ, pow_succ', LinearMap.mul_apply]
exact LieSubmodule.lie_mem_lie _ ⊤ (LieSubmodule.mem_top x) ih

Expand Down Expand Up @@ -602,7 +603,8 @@ lemma independent_weightSpace [NoZeroSMulDivisors R M] :
simpa only [CompleteLattice.independent_iff_supIndep_of_injOn (injOn_weightSpace R L M),
Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.not_mem_erase χ)
intro χ₁ s
induction' s using Finset.induction_on with χ₂ s _ ih; simp
induction' s using Finset.induction_on with χ₂ s _ ih
· simp
intro hχ₁₂
obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
specialize ih hχ₁
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Module/Zlattice/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -518,8 +518,8 @@ theorem Zlattice.rank [hs : IsZlattice K L] : finrank ℤ L = finrank K E := by
have h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ L) =
(Set.range b).toFinset.card := by
rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
rfl
exact Subtype.coe_injective.comp (Basis.injective _)
· rfl
· exact Subtype.coe_injective.comp (Basis.injective _)
rw [finrank_eq_card_chooseBasisIndex]
-- We prove that `finrank ℤ L ≤ finrank K E` and `finrank K E ≤ finrank ℤ L`
refine le_antisymm ?_ ?_
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Polynomial/UnitTrinomial.lean
Original file line number Diff line number Diff line change
Expand Up @@ -273,10 +273,10 @@ theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k
rw [this] at hp
exact Or.inl (hq.trans hp.symm)
rw [tsub_add_eq_add_tsub hmn.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm
rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm'
exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm)
exact hmn'.le.trans (Nat.le_add_right n k)
exact hmn.le.trans (Nat.le_add_right n k)
· rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm'
· exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm)
· exact hmn'.le.trans (Nat.le_add_right n k)
· exact hmn.le.trans (Nat.le_add_right n k)
#align polynomial.is_unit_trinomial.irreducible_aux2 Polynomial.IsUnitTrinomial.irreducible_aux2

theorem irreducible_aux3 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n)
Expand Down
42 changes: 21 additions & 21 deletions Mathlib/AlgebraicGeometry/AffineScheme.lean
Original file line number Diff line number Diff line change
Expand Up @@ -267,7 +267,7 @@ theorem fromSpec_range :
Set.range hU.fromSpec.1.base = (U : Set X) := by
delta IsAffineOpen.fromSpec; dsimp
rw [← Category.assoc, coe_comp, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
exact Subtype.range_coe
· exact Subtype.range_coe
rw [← TopCat.epi_iff_surjective]
infer_instance
#align algebraic_geometry.is_affine_open.from_Spec_range AlgebraicGeometry.IsAffineOpen.fromSpec_range
Expand Down Expand Up @@ -555,26 +555,26 @@ def _root_.AlgebraicGeometry.Scheme.affineBasicOpen
theorem basicOpen_union_eq_self_iff (s : Set (X.presheaf.obj <| op U)) :
⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U) = U ↔ Ideal.span s = ⊤ := by
trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ
trans
hU.fromSpec.1.base ⁻¹' (⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U)).1 =
hU.fromSpec.1.base ⁻¹' U.1
· refine' ⟨fun h => by rw [h], _⟩
intro h
apply_fun Set.image hU.fromSpec.1.base at h
rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.fromSpec_range]
at h
simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
ext1
refine' Set.Subset.antisymm _ h
simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
intro x _
exact X.basicOpen_le x
· simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion]
congr! 1
· refine congr_arg (Set.iUnion ·) ?_
ext1 x
exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _)
· exact congr_arg Opens.carrier hU.fromSpec_base_preimage
· trans
hU.fromSpec.1.base ⁻¹' (⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U)).1 =
hU.fromSpec.1.base ⁻¹' U.1
· refine' ⟨fun h => by rw [h], _⟩
intro h
apply_fun Set.image hU.fromSpec.1.base at h
rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.fromSpec_range]
at h
simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
ext1
refine' Set.Subset.antisymm _ h
simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
intro x _
exact X.basicOpen_le x
· simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion]
congr! 1
· refine congr_arg (Set.iUnion ·) ?_
ext1 x
exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _)
· exact congr_arg Opens.carrier hU.fromSpec_base_preimage
· simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]
Expand Down
11 changes: 6 additions & 5 deletions Mathlib/AlgebraicGeometry/FunctionField.lean
Original file line number Diff line number Diff line change
Expand Up @@ -56,8 +56,9 @@ noncomputable instance [IsIntegral X] : Field X.functionField := by
have hs : genericPoint X.carrier ∈ RingedSpace.basicOpen _ s := by
rw [← SetLike.mem_coe, (genericPoint_spec X.carrier).mem_open_set_iff, Set.top_eq_univ,
Set.univ_inter, Set.nonempty_iff_ne_empty, Ne, ← Opens.coe_bot, ← SetLike.ext'_iff]
erw [basicOpen_eq_bot_iff]
exacts [ha, (RingedSpace.basicOpen _ _).isOpen]
· erw [basicOpen_eq_bot_iff]
exact ha
· exact (RingedSpace.basicOpen _ _).isOpen
have := (X.presheaf.germ ⟨_, hs⟩).isUnit_map (RingedSpace.isUnit_res_basicOpen _ s)
rwa [TopCat.Presheaf.germ_res_apply] at this

Expand Down Expand Up @@ -87,9 +88,9 @@ theorem genericPoint_eq_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsO
symm
rw [eq_top_iff, Set.top_eq_univ, Set.top_eq_univ]
convert subset_closure_inter_of_isPreirreducible_of_isOpen _ H.base_open.isOpen_range _
rw [Set.univ_inter, Set.image_univ]
apply PreirreducibleSpace.isPreirreducible_univ (X := Y.carrier)
exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
· rw [Set.univ_inter, Set.image_univ]
· apply PreirreducibleSpace.isPreirreducible_univ (X := Y.carrier)
· exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
#align algebraic_geometry.generic_point_eq_of_is_open_immersion AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion

noncomputable instance stalkFunctionFieldAlgebra [IrreducibleSpace X.carrier] (x : X.carrier) :
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -301,8 +301,8 @@ theorem AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AffineTargetMo
· introv hs hs'
replace hs := ((topIsAffineOpen Y).basicOpen_union_eq_self_iff _).mpr hs
have := H f ⟨Y.openCoverOfSuprEqTop _ hs, ?_, ?_⟩ (𝟙 _)
rwa [← Category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_isIso hP]
at this
· rwa [← Category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_isIso hP]
at this
· intro i; exact (topIsAffineOpen Y).basicOpenIsAffine _
· rintro (i : s)
specialize hs' i
Expand Down
25 changes: 13 additions & 12 deletions Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,9 @@ instance (priority := 900) quasiCompactOfIsIso {X Y : Scheme} (f : X ⟶ Y) [IsI
intro U _ hU'
convert hU'.image (inv f.1.base).continuous_toFun using 1
rw [Set.image_eq_preimage_of_inverse]
delta Function.LeftInverse
exacts [IsIso.inv_hom_id_apply f.1.base, IsIso.hom_inv_id_apply f.1.base]
· delta Function.LeftInverse
exact IsIso.inv_hom_id_apply f.1.base
· exact IsIso.hom_inv_id_apply f.1.base
#align algebraic_geometry.quasi_compact_of_is_iso AlgebraicGeometry.quasiCompactOfIsIso

instance quasiCompactComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCompact f]
Expand Down Expand Up @@ -171,14 +172,14 @@ theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _).
exact H
· rintro X Y H f S hS hS'
rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS
delta QuasiCompact.affineProperty
rw [← isCompact_univ_iff]
change IsCompact ((Opens.map f.val.base).obj ⊤).1
rw [← hS]
dsimp [Opens.map]
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
exacts [isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i),
topIsAffineOpen _]
· delta QuasiCompact.affineProperty
rw [← isCompact_univ_iff]
change IsCompact ((Opens.map f.val.base).obj ⊤).1
rw [← hS]
dsimp [Opens.map]
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)
· exact topIsAffineOpen _
#align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal

theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
Expand Down Expand Up @@ -323,8 +324,8 @@ theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme
convert congr_arg (X.presheaf.map (homOfLE _).op) H
-- Note: the below was `simp only [← comp_apply]`
· rw [← comp_apply, ← comp_apply]
simp only [← Functor.map_comp]
rfl
· simp only [← Functor.map_comp]
rfl
· simp only [Scheme.basicOpen_res, ge_iff_le, inf_le_right]
· rw [map_zero]
choose n hn using H'
Expand Down
8 changes: 6 additions & 2 deletions Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
Original file line number Diff line number Diff line change
Expand Up @@ -393,12 +393,16 @@ theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U :
replace hs : S ⊓ U.1 = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs
have hs₁ : ∀ i : s, i.1.1 ≤ S := by
intro i; change (i : Opens X.carrier) ≤ S
refine' le_trans _ inf_le_left; swap; exact U.1; erw [hs]
refine' le_trans _ inf_le_left; swap
· exact U.1
erw [hs]
-- Porting note: have to add argument explicitly
exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i
have hs₂ : ∀ i : s, i.1.1 ≤ U.1 := by
intro i; change (i : Opens X.carrier) ≤ U
refine' le_trans _ inf_le_right; swap; exact S; erw [hs]
refine' le_trans _ inf_le_right; swap
· exact S
erw [hs]
-- Porting note: have to add argument explicitly
exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i
-- On each affine open in the intersection, we have `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂`
Expand Down
54 changes: 27 additions & 27 deletions Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
Original file line number Diff line number Diff line change
Expand Up @@ -180,25 +180,25 @@ theorem affineLocally_iff_affineOpens_le (hP : RingHom.RespectsIso @P) {X Y : Sc
erw [Subtype.range_val]
convert e
have := H ⟨(Opens.map (X.ofRestrict U'.openEmbedding).1.base).obj V.1, ?h'⟩
erw [← X.presheaf.map_comp] at this
rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc,
← X.presheaf.map_comp]
convert this using 1
dsimp only [Functor.op, unop_op]
rw [Opens.openEmbedding_obj_top]
congr 1
exact e'.symm
case h' =>
apply (X.ofRestrict U'.openEmbedding).isAffineOpen_iff_of_isOpenImmersion.mp
-- Porting note: was convert V.2
erw [e']
apply V.2
· erw [← X.presheaf.map_comp] at this
· rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc,
← X.presheaf.map_comp]
· convert this using 1
dsimp only [Functor.op, unop_op]
rw [Opens.openEmbedding_obj_top]
congr 1
exact e'.symm
case h' =>
apply (X.ofRestrict U'.openEmbedding).isAffineOpen_iff_of_isOpenImmersion.mp
-- Porting note: was convert V.2
erw [e']
apply V.2
· intro H V
specialize H ⟨_, V.2.imageIsOpenImmersion (X.ofRestrict _)⟩ (Subtype.coe_image_subset _ _)
erw [← X.presheaf.map_comp]
rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc, ←
X.presheaf.map_comp]
convert H
· convert H
· dsimp only [Functor.op, unop_op]; rw [Opens.openEmbedding_obj_top]
#align algebraic_geometry.affine_locally_iff_affine_opens_le AlgebraicGeometry.affineLocally_iff_affineOpens_le

Expand Down Expand Up @@ -230,16 +230,16 @@ theorem sourceAffineLocally_isLocal (h₁ : RingHom.RespectsIso @P)
apply h₃ _ _ hs
intro r
have := hs' r ⟨(Opens.map (X.ofRestrict _).1.base).obj U.1, ?_⟩
rwa [h₁.ofRestrict_morphismRestrict_iff] at this
· exact U.2
· rfl
· suffices ∀ (V) (_ : V = (Opens.map f.val.base).obj (Y.basicOpen r.val)),
IsAffineOpen ((Opens.map (X.ofRestrict V.openEmbedding).1.base).obj U.1) by
exact this _ rfl
intro V hV
rw [Scheme.preimage_basicOpen] at hV
subst hV
exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1)
· rwa [h₁.ofRestrict_morphismRestrict_iff] at this
· exact U.2
· rfl
· suffices ∀ (V) (_ : V = (Opens.map f.val.base).obj (Y.basicOpen r.val)),
IsAffineOpen ((Opens.map (X.ofRestrict V.openEmbedding).1.base).obj U.1) by
exact this _ rfl
intro V hV
rw [Scheme.preimage_basicOpen] at hV
subst hV
exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1)
#align algebraic_geometry.source_affine_locally_is_local AlgebraicGeometry.sourceAffineLocally_isLocal

variable (hP : RingHom.PropertyIsLocal @P)
Expand Down Expand Up @@ -271,9 +271,9 @@ theorem isOpenImmersionCat_comp_of_sourceAffineLocally (h₁ : RingHom.RespectsI
rw [← h₁.cancel_right_isIso _
(Scheme.Γ.map (IsOpenImmersion.isoOfRangeEq (Y.ofRestrict _) f _).hom.op),
← Functor.map_comp, ← op_comp]
convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3
· rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc]
exact Subtype.range_coe
· convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3
· rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc]
exact Subtype.range_coe
#align algebraic_geometry.is_open_immersion_comp_of_source_affine_locally AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally

end AlgebraicGeometry
Expand Down
38 changes: 19 additions & 19 deletions Mathlib/AlgebraicGeometry/OpenImmersion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -118,8 +118,8 @@ def affineCover (X : Scheme) : OpenCover X where
intro x
erw [coe_comp]
rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
erw [Subtype.range_coe_subtype]
exact (X.local_affine x).choose.2
· erw [Subtype.range_coe_subtype]
exact (X.local_affine x).choose.2
rw [← TopCat.epi_iff_surjective]
change Epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forgetToSheafedSpace.map _))
infer_instance
Expand Down Expand Up @@ -561,9 +561,9 @@ theorem range_pullback_snd_of_left :
rw [Set.range_comp, Set.range_iff_surjective.mpr, ←
@Set.preimage_univ _ _ (pullback.fst : pullback f.1.base g.1.base ⟶ _)]
-- Porting note (#10691): was `rw`
erw [TopCat.pullback_snd_image_fst_preimage]
rw [Set.image_univ]
rfl
· erw [TopCat.pullback_snd_image_fst_preimage]
rw [Set.image_univ]
rfl
rw [← TopCat.epi_iff_surjective]
infer_instance
#align algebraic_geometry.IsOpenImmersion.range_pullback_snd_of_left AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left
Expand All @@ -578,9 +578,9 @@ theorem range_pullback_fst_of_right :
rw [Set.range_comp, Set.range_iff_surjective.mpr, ←
@Set.preimage_univ _ _ (pullback.snd : pullback g.1.base f.1.base ⟶ _)]
-- Porting note (#10691): was `rw`
erw [TopCat.pullback_fst_image_snd_preimage]
rw [Set.image_univ]
rfl
· erw [TopCat.pullback_fst_image_snd_preimage]
rw [Set.image_univ]
rfl
rw [← TopCat.epi_iff_surjective]
infer_instance
#align algebraic_geometry.IsOpenImmersion.range_pullback_fst_of_right AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right
Expand Down Expand Up @@ -703,13 +703,13 @@ theorem image_basicOpen {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] {U
-- Porting note (#10691): was `rw`
erw [PresheafedSpace.IsOpenImmersion.invApp_app_apply] at e
rw [Scheme.basicOpen_res, inf_eq_right.mpr _] at e
rw [← e]
ext1
-- Porting note: this `dsimp` was not necessary
dsimp [Opens.map]
refine' Set.image_preimage_eq_inter_range.trans _
erw [Set.inter_eq_left]
refine' Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)
· rw [← e]
ext1
-- Porting note: this `dsimp` was not necessary
dsimp [Opens.map]
refine' Set.image_preimage_eq_inter_range.trans _
erw [Set.inter_eq_left]
refine' Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)
refine' le_trans (Scheme.basicOpen_le _ _) (le_of_eq _)
ext1
exact (Set.preimage_image_eq _ H.base_open.inj).symm
Expand Down Expand Up @@ -740,8 +740,8 @@ def Scheme.OpenCover.pullbackCover {X : Scheme} (𝒰 : X.OpenCover) {W : Scheme
erw [coe_comp]
rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ,
TopCat.pullback_fst_range]
obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x)
exact ⟨y, h.symm⟩
· obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x)
exact ⟨y, h.symm⟩
· rw [← TopCat.epi_iff_surjective]; infer_instance
#align algebraic_geometry.Scheme.open_cover.pullback_cover AlgebraicGeometry.Scheme.OpenCover.pullbackCover

Expand All @@ -763,8 +763,8 @@ def Scheme.OpenCover.pullbackCover' {X : Scheme} (𝒰 : X.OpenCover) {W : Schem
erw [coe_comp]
rw [Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ,
TopCat.pullback_snd_range]
obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x)
exact ⟨y, h⟩
· obtain ⟨y, h⟩ := 𝒰.Covers (f.1.base x)
exact ⟨y, h⟩
· rw [← TopCat.epi_iff_surjective]; infer_instance

theorem Scheme.OpenCover.iUnion_range {X : Scheme} (𝒰 : X.OpenCover) :
Expand Down
Loading

0 comments on commit fe96aa4

Please sign in to comment.