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

Goal state before:
pp: case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ⨆ i ∈ s, X.basicOpen i ≤ U

Tactic:
rw [iSup₂_le_iff]
    exact fun i _ ↦ X.basicOpen_le i

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
⊢ D.t'' i j k ≫ D.t'' j k i ≫ D.t'' k i j = 𝟙 (pullback (D.f' i j) (D.f' i k))

Tactic:
by
    delta GlueData'.t''
    if hij : i = j then
      subst hij
      if hik : i = k then
        subst hik
        ext <;> simp
      else
        simp [hik, Ne.symm hik, fst_eq_snd_of_mono_eq]
    else if hik : i = k then
      subst hik
      ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq, pullback.condition_assoc]
    else if hjk : j = k then
      subst hjk
      ext <;> simp [hij, Ne.symm hij, fst_eq_snd_of_mono_eq]
    else
      ext <;> simp [hij, Ne.symm hij, hik, Ne.symm hik, hjk, Ne.symm hjk,
        pullback.map_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f

Tactic:
← Over.comp_left_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left ((prodComparisonIso (pullback f) R S).hom ≫ (prodComparisonIso (pullback f) R S).inv) ≫
      pullback.fst (R ⊗ S).hom f ≫ pullback.fst R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.fst ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst R.hom f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.fst (R ⊗ S).hom f ≫ pullback.snd R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f

Tactic:
← Over.comp_left_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left ((prodComparisonIso (pullback f) R S).hom ≫ (prodComparisonIso (pullback f) R S).inv) ≫
      pullback.fst (R ⊗ S).hom f ≫ pullback.snd R.hom S.hom =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.fst S.hom f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Over

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      Hom.left (prodComparisonIso (pullback f) R S).inv ≫ pullback.snd (R ⊗ S).hom f =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f

Tactic:
← Over.comp_left_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X R✝ : C
f : R✝ ⟶ X
R S : Over X
⊢ Hom.left ((prodComparisonIso (pullback f) R S).hom ≫ (prodComparisonIso (pullback f) R S).inv) ≫
      pullback.snd (R ⊗ S).hom f =
    Hom.left (prodComparisonIso (pullback f) R S).hom ≫
      pullback.snd ((pullback f).obj R).hom ((pullback f).obj S).hom ≫ pullback.snd S.hom f
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ IsOpen[inst✝] (⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s)

Tactic:
rw [isOpen_iff_forall_mem_open]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set ↑(ofOpenSubsets U).glued
hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑(ConcreteCategory.hom ((ofOpenSubsets U).ι i)) ⁻¹' s)
⊢ ∀ x ∈ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s,
    ∃ t ⊆ ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U)) '' s, IsOpen[inst✝] t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y =
    𝟙 (pullback (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)))

Tactic:
apply pullback.hom_ext <;> simp_rw [Category.id_comp, Category.assoc]
  · apply glued_cover_cocycle_fst
  · apply glued_cover_cocycle_snd

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g =
    pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g

Tactic:
← cancel_mono (𝒰.f i)

Goal state after:
case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ ((t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ pullback.fst (𝒰.f i ≫ f) g) ≫ 𝒰.f i =
    (pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ pullback.fst (𝒰.f i ≫ f) g) ≫ 𝒰.f i
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
← cancel_mono (𝒰.f i)

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ (t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)) ≫ 𝒰.f i =
    pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) ≫ 𝒰.f i
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ Function.Injective ⇑(fromGlued 𝒰)

Tactic:
by
  intro x y h
  obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
  obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y
  rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply] at h
  simp_rw [← Scheme.Hom.comp_base] at h
  rw [ι_fromGlued, ι_fromGlued] at h
  let e :=
    (TopCat.pullbackConeIsLimit _ _).conePointUniqueUpToIso
      (isLimitOfHasPullbackOfPreservesLimit Scheme.forgetToTop (𝒰.f i) (𝒰.f j))
  rw [𝒰.gluedCover.ι_eq_iff]
  use e.hom ⟨⟨x, y⟩, h⟩
  constructor
  · erw [← ConcreteCategory.comp_apply e.hom,
      IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.left]
    rfl
  · erw [← ConcreteCategory.comp_apply e.hom, pullbackSymmetry_hom_comp_fst,
      IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
⊢ IsOpen (⇑(fromGlued 𝒰) '' U)

Tactic:
rw [isOpen_iff_forall_mem_open]

Goal state after:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
⊢ ∀ x ∈ ⇑(fromGlued 𝒰) '' U, ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd

Tactic:
simp_rw [(Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ (((pullbackSymmetry s.fst (𝒰.f b)).hom ≫ pullback.map (𝒰.f b) s.fst (𝒰.f b ≫ f) g (𝟙 (𝒰.X b)) s.snd f ⋯ ⋯) ≫
        (gluing 𝒰 f g).ι b) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case inv_hom_id.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.fst (𝒰.f i ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
· simp_rw [Category.assoc, pullback.lift_fst, pullback.lift_snd, Category.id_comp]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i : 𝒰.I₀
⊢ (pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯ ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    𝟙 (pullback (𝒰.f i ≫ f) g) ≫ pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
⊢ P (pullback.fst f g)

Tactic:
by
      rw [P.iff_of_zeroHypercover_target (S.affineCover.pullback₁ f)]
      intro i
      let e : pullback (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) ≅
          _ := by
        refine pullbackSymmetry _ _ ≪≫ pullbackRightPullbackFstIso f g _ ≪≫ ?_ ≪≫
          (pullbackRightPullbackFstIso (S.affineCover.f i) g
            (pullback.snd f (S.affineCover.f i))).symm
        exact asIso
          (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simpa using! pullback.condition) (by simp))
      have : e.hom ≫ pullback.fst _ _ =
          pullback.snd (pullback.fst f g) ((S.affineCover.pullback₁ f).f i) := by
        simp [e]
      rw [← this, P.cancel_left_of_respectsIso]
      apply HasAffineProperty.pullback_fst_of_right hP'
      let := isLocal_affineProperty P
      rw [← pullbackSymmetry_hom_comp_snd, Q.cancel_left_of_respectsIso]
      apply of_isPullback (.of_hasPullback _ _) H

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
⊢ ∀ (i : (a : ↑s) × ↑(t a)),
    P
      ((algebraMap S
            ((fun x ↦
                match x with
                | ⟨a, b⟩ => Localization.Away ↑b)
              i)).comp
        f)

Tactic:
· intro ⟨a, b⟩
    rw [IsScalarTower.algebraMap_eq S (Localization.Away a.val) (Localization.Away b.val)]
    apply ht _ _ b.property

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
x : R
⊢ (algebraMap T (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))) (g (f x)) =
    (Localization.awayMap g' ↑a) ((algebraMap S (Localization.Away ↑a)) (f x))

Tactic:
change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
x : R
⊢ (algebraMap T (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))) (g (f x)) =
    (Localization.awayMap g' ↑a) ((algebraMap S (Localization.Away ↑a)) (f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: X✝ Y✝ Z✝ : Scheme
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x))

Tactic:
exact (f.stalkMap_surjective x).comp (g.stalkMap_surjective (f x))

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

Goal state before:
pp: X : TopCat
F : TopCat.Presheaf CommRingCat X
U₁ U₂ U₃ U₄ U₅ U₆ U₇ : Opens ↑X
n₁ n₂ : ℕ
y₁ : ↑(F.obj (op U₁))
y₂ : ↑(F.obj (op U₂))
f : ↑(F.obj (op (U₁ ⊔ U₂)))
x : ↑(F.obj (op U₃))
h₄₁ : U₄ ≤ U₁
h₄₂ : U₄ ≤ U₂
h₅₁ : U₅ ≤ U₁
h₅₃ : U₅ ≤ U₃
h₆₂ : U₆ ≤ U₂
h₆₃ : U₆ ≤ U₃
h₇₄ : U₇ ≤ U₄
h₇₅ : U₇ ≤ U₅
h₇₆ : U₇ ≤ U₆
e₁ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
e₂ :
  (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₂ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) f ^ n₁ * (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) y₂

Tactic:
rw [e₁, e₂, mul_left_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
e : I ≤ J
inst✝¹ : J.IsPrime
inst✝ : J.FiniteHeight
e' : J.height ≤ I.height
⊢ J ∈ I.minimalPrimes

Tactic:
obtain ⟨p, h₁, h₂⟩ := Ideal.exists_minimalPrimes_le e
  convert! h₁
  refine (eq_of_le_of_not_lt h₂ fun h₃ ↦ ?_).symm
  have := h₁.isPrime
  have := finiteHeight_of_le h₂ IsPrime.ne_top'
  exact lt_irrefl _ ((height_strict_mono_of_isPrime h₃).trans_le
    (e'.trans <| height_mono h₁.le))

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I < M
⊢ I.IsMaximal

pp: case inr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I = M
⊢ I.IsMaximal

Tactic:
· have h1 := Ideal.height_strict_mono_of_isPrime hM'
    have h2 := e ▸ M.height_le_ringKrullDim_of_ne_top hM.ne_top
    simp [← not_lt, h1] at h2

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : I.IsPrime
inst✝ : FiniteRingKrullDim R
e : ↑I.height = ringKrullDim R
h : I ≠ ⊤
M : Ideal R
hM : M.IsMaximal
hM'✝ : I ≤ M
hM' : I = M
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
h : I = ⊤
⊢ ↑(⨆ (_ : I ≠ ⊤), I.height) ≤ ringKrullDim R

Tactic:
simp [h, ringKrullDim_nonneg_of_nontrivial]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x ⋯)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑V) x ⋯)) (I.ideal V)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U) x hxU)) (I.ideal V) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)

Tactic:
simp only [homOfLE_leOfHom, TopCat.Presheaf.germ_res', this]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
j : ↥↑V
⊢ Submodule.restrictScalars (↑Γ(X, ↑V))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal (U (i j)))) ≤
    Submodule.restrictScalars (↑Γ(X, ↑V)) (J.ideal ⟨X.basicOpen (rU j), ⋯⟩)

Tactic:
← J.map_ideal (V := (U _)) (X.basicOpen_le _)

Goal state after:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
j : ↥↑V
⊢ Submodule.restrictScalars (↑Γ(X, ↑V))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal (U (i j)))) ≤
    Submodule.restrictScalars (↑Γ(X, ↑V))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (J.ideal (U (i j))))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
⊢ I * (J ⊔ K) = I * J ⊔ I * K

Tactic:
ext U : 2

Goal state after:
X : Scheme
I J K : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
⊢ (I ⊔ J) * K = I * K ⊔ J * K

Tactic:
ext U : 2

Goal state after:
X : Scheme
I J K : X.IdealSheafData
U : ↑X.affineOpens
⊢ ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

Tactic:
ext U : 2

Goal state after:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I ⊓ J).radical = I.radical ⊓ J.radical

Tactic:
ext U : 2

Goal state after:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
ext U : 2

Goal state after:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I * J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ vanishingIdeal I.support = I.radical

Tactic:
ext U : 2

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ (vanishingIdeal I.support).ideal U = I.radical.ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : ↑Z.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (g.app ↑U)) ≤
    Ideal.comap (CommRingCat.Hom.hom (g.app ↑U)) (RingHom.ker (CommRingCat.Hom.hom (app f (g ⁻¹ᵁ ↑U))))

Tactic:
exact Ideal.ker_le_comap _

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

Goal state before:
pp: case refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : ↑X.affineOpens
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
i : ↑↑s'
⊢ IsCompact (↑↑V ∩ ↑(X.basicOpen ↑i))

Tactic:
rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
    exact (V.2.basicOpen _).isCompact

Goal state after:
Module: Mathlib.RingTheory.RingHom.FiniteType

Goal state before:
pp: ⊢ IsStableUnderBaseChange @FiniteType

Tactic:
by
  apply IsStableUnderBaseChange.mk
  · exact finiteType_respectsIso
  · introv h
    rw [finiteType_algebraMap] at h
    apply finiteType_algebraMap.mpr
    infer_instance

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
⊢ (Hom.ker f).comap (Hom.coborderRange f).ι = Hom.ker (Hom.liftCoborder f)

Tactic:
ext U : 2

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsImmersion f
inst✝ : QuasiCompact f
U : ↑(↑(Hom.coborderRange f)).affineOpens
⊢ ((Hom.ker f).comap (Hom.coborderRange f).ι).ideal U = (Hom.ker (Hom.liftCoborder f)).ideal U
Module: Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ C ∈ image (BasicConstructibleSetData.map f) s, C.toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet

Tactic:
set_biUnion_finset_image

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
s : ConstructibleSetData R
⊢ ⋃ y ∈ s, (BasicConstructibleSetData.map f y).toSet = comap f ⁻¹' ⋃ C ∈ s, C.toSet