mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsClosedImmersion f
H : Scheme.Hom.ker f ≤ Scheme.Hom.ker g
⊢ lift f g H ≫ f = g

Tactic:
nth_rw 2 [← f.toImage_imageι]
  simp [lift, -Scheme.Hom.toImage_imageι, g.toImage_imageι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget (topologically fun {X Y} x x_1 f ↦ IsLocallyClosed (Set.range f))

Tactic:
apply +allowSynthFailures topologically_isZariskiLocalAtTarget'

Goal state after:
case inst
X Y Z : Scheme
f : X ⟶ Y
⊢ (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] f ↦ IsLocallyClosed (Set.range f)).RespectsIso

case hP
X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → TopologicalSpace.Opens β),
    TopologicalSpace.IsOpenCover U →
      Continuous f →
        (IsLocallyClosed (Set.range f) ↔ ∀ (i : ι), IsLocallyClosed (Set.range ((U i).carrier.restrictPreimage f)))
Module: Mathlib.AlgebraicGeometry.Morphisms.Immersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ ∀ {X Y Y' S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
    IsPullback f' g' g f → IsImmersion g → IsImmersion g'

Tactic:
by
    intro X Y Y' S f g f' g' H hg
    let Z := Limits.pullback f g.coborderRange.ι
    let e : Y' ⟶ Z := Limits.pullback.lift g' (f' ≫ g.liftCoborder) (by simpa using H.w.symm)
    have : IsClosedImmersion e := by
      have := (IsPullback.paste_horiz_iff (.of_hasPullback f g.coborderRange.ι)
        (show e ≫ Limits.pullback.snd _ _ = _ from Limits.pullback.lift_snd _ _ _)).mp ?_
      · exact MorphismProperty.of_isPullback this.flip inferInstance
      · simpa [e] using H.flip
    rw [← Limits.pullback.lift_fst (f := f) (g := g.coborderRange.ι) g' (f' ≫ g.liftCoborder)
      (by simpa using H.w.symm)]
    infer_instance

Goal state after:
Module: Mathlib.RingTheory.Finiteness.FinitePresentationLocal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : ∑ i ∈ s.attach, l i • ↑i = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ (∑ x ∈ s.attach, ↑x * l x - 1) * f q = 0

pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ l ∈ Finsupp.supported S S ↑s.attach

Tactic:
· rw [← hl]
      simp only [Finset.coe_sort_coe, smul_eq_mul, mul_comm, sub_self, zero_mul]

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
s✝ : Set S
hs✝ : Ideal.span s✝ = ⊤
s : Finset S
h₁ : ↑s ⊆ s✝
hs : Ideal.span ↑s = ⊤
h : ∀ (i : ↥s), FinitePresentation R (Localization.Away ↑i)
hfintype : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
l : ↑↑s →₀ S
hl : (Finsupp.linearCombination S Subtype.val) l = 1
g' : ↥s → MvPolynomial (Fin n) R
hg' : ∀ (g : ↥s), f (g' g) = ↑g
h' : ↥s → MvPolynomial (Fin n) R
hh' : ∀ (g : ↥s), f (h' g) = l g
I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g, g' g * h' g - 1}
A : Type u_1 := MvPolynomial (Fin n) R ⧸ I
q : MvPolynomial (Fin n) R
⊢ l ∈ Finsupp.supported S S ↑s.attach
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
⊢ ¬IsNilpotent
        ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField))
          ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f)) ↔
    ¬IsNilpotent ((algebraMap (A ⊗[K] ↥B') (A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)) f)

Tactic:
not_iff_not

Goal state after:
K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
⊢ IsNilpotent
      ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField))
        ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f)) ↔
    IsNilpotent ((algebraMap (A ⊗[K] ↥B') (A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)) f)
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ LocallyOfFinitePresentation f ↔ affineLocally (fun {R S} [CommRing R] [CommRing S] ↦ RingHom.FinitePresentation) f

Tactic:
rw [locallyOfFinitePresentation_iff, affineLocally_iff_forall_isAffineOpen]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocallyNoetherian Y
inst✝ : LocallyOfFiniteType f
⊢ LocallyOfFinitePresentation f

Tactic:
refine ⟨fun {U hU V hV} hUV ↦ ?_⟩
  let := (f.appLE U V hUV).hom.toAlgebra
  have : IsNoetherianRing Γ(Y, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
  exact Algebra.FinitePresentation.of_finiteType.mp (f.finiteType_appLE hU hV hUV)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap) f

Tactic:
HasRingHomProperty.iff_appLE (P := topologically GeneralizingMap)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, UniversallyClosed f → IsAffineHom f → (∃ R, Y = Spec R) → IsIntegralHom f
hY : ¬∃ R, Y = Spec R
⊢ IsIntegralHom f

pp: X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hY : ∃ R, Y = Spec R
⊢ IsIntegralHom f

Tactic:
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover]
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁
    rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂
    exact fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩

Goal state after:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hY : ∃ R, Y = Spec R
⊢ IsIntegralHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: case inr
X : Scheme
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst✝ : JacobsonSpace ↥(Spec S)
this :
  ∀ {X : Scheme} [Subsingleton ↥X] [IsReduced X] {f : X ⟶ Spec S},
    (∃ R, X = Spec R) → (IsFinite f ↔ LocallyOfFiniteType f)
hX : ¬∃ R, X = Spec R
⊢ IsFinite f ↔ LocallyOfFiniteType f

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (P := @IsFinite) X.isoSpec.inv,
      ← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType) X.isoSpec.inv]

Goal state after:
case inr
X : Scheme
inst✝² : Subsingleton ↥X
inst✝¹ : IsReduced X
S : CommRingCat
f : X ⟶ Spec S
inst✝ : JacobsonSpace ↥(Spec S)
this :
  ∀ {X : Scheme} [Subsingleton ↥X] [IsReduced X] {f : X ⟶ Spec S},
    (∃ R, X = Spec R) → (IsFinite f ↔ LocallyOfFiniteType f)
hX : ¬∃ R, X = Spec R
⊢ IsFinite (X.isoSpec.inv ≫ f) ↔ LocallyOfFiniteType (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝¹ : CompactSpace ↥X
this✝ : X.IsQuasiAffine
r : ↑Γ(Y, ⊤)
this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
⊢ IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
    (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)

Tactic:
have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ (f.appTop r)

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsAffineHom f
inst✝ : Y.IsQuasiAffine
this✝² : CompactSpace ↥X
this✝¹ : X.IsQuasiAffine
r : ↑Γ(Y, ⊤)
this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r)
this :
  IsLocalization.Away ((ConcreteCategory.hom (Hom.appTop f)) r)
    ↑Γ(X, X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r))
⊢ IsPushout (Hom.appTop f) (Y.presheaf.map (homOfLE ⋯).op) (X.presheaf.map (homOfLE ⋯).op)
    (Hom.appLE f (Y.basicOpen r) (X.basicOpen ((ConcreteCategory.hom (Hom.appTop f)) r)) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ f (Classical.arbitrary I) ≫ cF.π.app j = s.π.app j

Tactic:
rw [this _ j]

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cone F
cG : Cone G
f✝ : (Cone.postcompose α).obj cF ⟶ cG
hf : ∀ (i : I), IsPullback (cF.π.app i) f✝.hom (α.app i) (cG.π.app i)
hcG : IsLimit cG
s : Cone F
j : I
f : I → (s.pt ⟶ cF.pt) := fun i ↦ ⋯.lift (s.π.app i) (hcG.lift ((Cone.postcompose α).obj s)) ⋯
this : ∀ (i j : I), f i = f j
⊢ f j ≫ cF.π.app j = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected

Goal state before:
pp: I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f (Classical.arbitrary I) = s.ι.app j

Tactic:
rw [this _ j]

Goal state after:
I : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} I
inst✝¹ : IsConnected I
inst✝ : Category.{v_2, u_2} C
F G : I ⥤ C
α : F ⟶ G
cF : Cocone F
cG : Cocone G
f✝ : cF ⟶ (Cocone.precompose α).obj cG
hf : ∀ (i : I), IsPushout (cF.ι.app i) (α.app i) f✝.hom (cG.ι.app i)
hcF : IsColimit cF
s : Cocone G
j : I
f : I → (cG.pt ⟶ s.pt) := fun i ↦ ⋯.desc (hcF.desc ((Cocone.precompose α).obj s)) (s.ι.app i) ⋯
this : ∀ (i j : I), f i = f j
⊢ cG.ι.app j ≫ f j = s.ι.app j
Module: Mathlib.AlgebraicGeometry.Morphisms.Flat

Goal state before:
pp: X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst✝ : Flat iX
hUS : IsAffineOpen US
hUX : IsAffineOpen UX
hUT : IsCompact ↑UT
hUT' : IsQuasiSeparated ↑UT
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch
  exact isIso_pushoutSection_of_isQuasiSeparated_of_flat_right _ _ _ _ hUS hUX hUT hUT'

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain ≫ g.hom) ⁻¹ᵁ h.domain ≫
          f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain) ≫
        h.hom =
    (X₁.isoOfEq ⋯).hom ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        f.hom ∣_ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain ≫
          (Hom.isoImage g.domain.ι (g.hom ⁻¹ᵁ h.domain)).inv ≫ g.hom ∣_ h.domain ≫ h.hom

Tactic:
morphismRestrict_ι_image_ι_isoImage_inv_assoc,

Goal state after:
case H
X₁ X₂ X₃ Y : Scheme
inst✝⁴ : PreirreducibleSpace ↥X₁
inst✝³ : IrreducibleSpace ↥X₂
inst✝² : Nonempty ↥X₃
f : X₁.PartialMap X₂
inst✝¹ : IsDominant f.hom
g : X₂.PartialMap X₃
inst✝ : IsDominant g.hom
h : X₃.PartialMap Y
⊢ (Hom.isoImage (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).ι
          ((TopologicalSpace.Opens.map (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv.base).obj
            ((TopologicalSpace.Opens.map (f.hom ∣_ g.domain).base).obj
              ((TopologicalSpace.Opens.map g.hom.base).obj h.domain)))).inv ≫
      ((Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain)).inv ∣_ (f.hom ∣_ g.domain ≫ g.hom) ⁻¹ᵁ h.domain ≫
          f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain) ≫
        h.hom =
    (X₁.isoOfEq ⋯).hom ≫
      (Hom.isoImage f.domain.ι (f.hom ⁻¹ᵁ g.domain.ι ''ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
        (↑f.domain).homOfLE ⋯ ≫
          (Hom.isoImage (f.hom ⁻¹ᵁ g.domain).ι ((f.hom ∣_ g.domain) ⁻¹ᵁ g.hom ⁻¹ᵁ h.domain)).inv ≫
            f.hom ∣_ g.domain ∣_ g.hom ⁻¹ᵁ h.domain ≫ g.hom ∣_ h.domain ≫ h.hom
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X ⤏ Y
inst✝¹ : f.IsDominant
g : Y ⤏ Z
inst✝ : g.IsDominant
⊢ (f.comp g.representative.toRationalMap).IsDominant

Tactic:
RationalMap.comp_def

Goal state after:
X Y Z : Scheme
inst✝³ : PreirreducibleSpace ↥X
inst✝² : Nonempty ↥Y
f : X ⤏ Y
inst✝¹ : f.IsDominant
g : Y ⤏ Z
inst✝ : g.IsDominant
⊢ (f.representative.comp g.representative).toRationalMap.IsDominant
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: X Y Z : Scheme
inst✝¹⁰ : PreirreducibleSpace ↥X
inst✝⁹ : Nonempty ↥Y
S : Scheme
inst✝⁸ : IrreducibleSpace ↥Y
inst✝⁷ : Nonempty ↥Z
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : Z.Over S
f : X ⤏ Y
inst✝³ : f.IsDominant
inst✝² : IsOver S f
g : Y ⤏ Z
inst✝¹ : g.IsDominant
inst✝ : IsOver S g
⊢ IsOver S (f.comp g)

Tactic:
by
  rw [isOver_iff, ← comp_toRationalMap, comp_assoc, comp_toRationalMap,
    isOver_iff.mp ‹g.IsOver S›, comp_toRationalMap, RationalMap.isOver_iff.mp ‹f.IsOver S›]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ⊤.ι ''ᵁ (X.topIso.hom ≫ 𝟙 X) ⁻¹ᵁ f.domain = f.domain

Tactic:
Category.comp_id,

Goal state after:
case e
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ ⊤.ι ''ᵁ X.topIso.hom ⁻¹ᵁ f.domain = f.domain
Module: Mathlib.AlgebraicGeometry.Birational.Composition

Goal state before:
pp: case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage X.topIso.hom (X.topIso.hom ⁻¹ᵁ f.domain)).inv ≫ (X.topIso.hom ∣_ f.domain ≫ 𝟙 ↑f.domain) ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.hom

Tactic:
Category.comp_id,

Goal state after:
case H
X Y : Scheme
inst✝ : IrreducibleSpace ↥X
f : X.PartialMap Y
⊢ (Hom.isoImage X.topIso.hom (X.topIso.hom ⁻¹ᵁ f.domain)).inv ≫ X.topIso.hom ∣_ f.domain ≫ f.hom =
    (X.isoOfEq ⋯).hom ≫ f.hom
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U V : (D.obj i).Opens
hU : IsCompact ↑U
H✝ : c.π.app i ⁻¹ᵁ U ≤ c.π.app i ⁻¹ᵁ V
this : ∀ (j : Over i), CompactSpace ↥((opensDiagram D i U).obj j)
H : ((c.π.app i ⁻¹ᵁ U).ι ≫ c.π.app i) ⁻¹ᵁ V = ⊤
j : Over i
fji : j ⟶ Over.mk (𝟙 i)
hj : (D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ D.map (Over.Hom.left fji) ⁻¹ᵁ V
⊢ D.map j.hom ⁻¹ᵁ U ≤ D.map j.hom ⁻¹ᵁ V

Tactic:
simpa [show fji.left = j.hom by simpa using fji.w] using hj

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Directed

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
X : Scheme
𝒰 : X.OpenCover
inst✝ : Preorder 𝒰.I₀
hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ Hom.opensRange (𝒰.f i) ≤ Hom.opensRange (𝒰.f j)
H : TopologicalSpace.Opens.IsBasis (Set.range fun i ↦ Hom.opensRange (𝒰.f i))
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
this : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
k : 𝒰.I₀
h : (fun i ↦ Hom.opensRange (𝒰.f i)) k ≤ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i)
y : ↥(𝒰.X k)
hy : (𝒰.f k) y = (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x
⊢ Hom.opensRange (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) ≤ Hom.opensRange (𝒰.f i)

Tactic:
rw [Scheme.Hom.opensRange_comp]
      exact Set.image_subset_range _ _

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.I₀
⊢ P
    ({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
          f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.f
      j)

Tactic:
dsimp only

Goal state after:
case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)).left,
      f := fun x ↦ Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f x) S)) }.I₀
⊢ P (Over.Hom.left (pullback.fst (Hom.asOver f S) (Hom.asOver (𝒰.f j) S)))
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
      f := fun x ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }.I₀
⊢ P
    ({ I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
          f := fun x ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }.f
      j)

Tactic:
dsimp only

Goal state after:
case refine_2
P : MorphismProperty Scheme
S : Scheme
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝³ : W.Over S
inst✝² : X.Over S
inst✝¹ : Cover.Over S 𝒰
inst✝ : Hom.IsOver f S
j :
  { I₀ := 𝒰.I₀, X := fun x ↦ (pullback (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)).left,
      f := fun x ↦ Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f x) S) (Hom.asOver f S)) }.I₀
⊢ P (Over.Hom.left (pullback.snd (Hom.asOver (𝒰.f j) S) (Hom.asOver f S)))
Module: Mathlib.AlgebraicGeometry.Cover.Over

Goal state before:
pp: P : MorphismProperty Scheme
S : Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : IsJointlySurjectivePreserving P
X W : Scheme
𝒰 : Cover (precoverage P) X
f : W ⟶ X
inst✝⁶ : W.Over S
inst✝⁵ : X.Over S
inst✝⁴ : Cover.Over S 𝒰
inst✝³ : Hom.IsOver f S
Q : MorphismProperty Scheme
inst✝² : Q.HasOfPostcompProperty Q
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : Q.IsStableUnderComposition
hX : Q (X ↘ S)
hW : Q (W ↘ S)
hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)
j : (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).I₀
⊢ (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).f j ≫ W ↘ S = (Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).X j ↘ S

Tactic:
exact (pullback.fst (f.asOverProp S) ((𝒰.f j).asOverProp S)).w

Goal state after:
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_1.refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ IsCompact { carrier := s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅, is_open' := ⋯ }.carrier

Tactic:
dsimp only

Goal state after:
case refine_1.refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : IsCompactOpenCovered f U
s : Set ι
hs : s.Finite
V : (i : ι) → i ∈ s → Opens (X i)
hc : ∀ (i : ι) (h : i ∈ s), IsCompact (V i h).carrier
hU : ⋃ i, ⋃ (h : i ∈ s), f i '' ↑(V i h) = U
⊢ IsCompact (s.sigma fun i ↦ if h : i ∈ s then ↑(V i h) else ∅)
Module: Mathlib.Topology.Sets.CompactOpenCovered

Goal state before:
pp: case refine_2
S : Type u_1
ι : Type u_2
X : ι → Type u_3
f : (i : ι) → X i → S
inst✝ : (i : ι) → TopologicalSpace (X i)
U : Set S
x✝ : ∃ V, IsCompact V.carrier ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = U
V : Opens ((i : ι) × X i)
hc : IsCompact V.carrier
heq : (fun p ↦ f p.fst p.snd) '' V.carrier = U
⊢ IsCompactOpenCovered f U

Tactic:
· obtain ⟨s, t, hs, hc, heq'⟩ := hc.sigma_exists_finite_sigma_eq
    have (i : ι) (hi : i ∈ s) : IsOpen (t i) := by
      rw [← Set.mk_preimage_sigma (t := t) hi]
      exact isOpen_sigma_iff.mp (heq' ▸ V.2) i
    refine ⟨s, hs, fun i hi ↦ ⟨t i, this i hi⟩, fun i _ ↦ hc i, ?_⟩
    simp_rw [coe_mk, ← heq, ← heq', Set.image_sigma_eq_iUnion, Function.comp_apply]

Goal state after: