mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hxy
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := ⋯
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (Function.update c.val j (c.val j %ₘ c.val i) j).degree < (c.val j).degree

Tactic:
simpa using

Goal state after:
case hxy
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (c.val j %ₘ c.val i).degree < (c.val j).degree
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := ⋯
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound

Tactic:
have deg_bound₂ : c'.degBound < c.degBound := by
          dsimp [InductionObj.degBound, c']
          apply Finset.sum_lt_sum ?_ ⟨j, Finset.mem_univ _, ?_⟩
          · intro k _
            rw [update_apply]
            split_ifs with hkj
            · subst hkj; gcongr; exact (degree_modByMonic_le _ hi).trans hle
            · rfl
          · gcongr; simpa using (degree_modByMonic_lt _ hi).trans_le hle

Goal state after:
case neg
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
hij : coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ
hi' : ¬c.val i = 1
deg_bound₂ : c'.degBound < c.degBound
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ g₁ ≫ g i₁ ≫ φ i₁ = g₂ ≫ g i₂ ≫ φ i₂

Tactic:
simpa using

Goal state after:
C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ g₁ ≫ g i₁ ≫ φ i₁ = g₂ ≫ g i₂ ≫ φ i₂
Module: Mathlib.CategoryTheory.EffectiveEpi.Comp

Goal state before:
pp: C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ (g₁ ≫ g i₁) ≫ f i₁ = (g₂ ≫ g i₂) ≫ f i₂

Tactic:
simpa using

Goal state after:
C✝ : Type u_1
inst✝³ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝² : Category.{v_2, u_2} C
I : Type u_3
Z Y : I → C
X : C
g : (i : I) → Z i ⟶ Y i
f : (i : I) → Y i ⟶ X
inst✝¹ : EffectiveEpiFamily Z fun i ↦ g i ≫ f i
inst✝ : ∀ (i : I), Epi (g i)
W : C
φ : (a : I) → Y a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : I) (g₁ : Z ⟶ Y a₁) (g₂ : Z ⟶ Y a₂), g₁ ≫ f a₁ = g₂ ≫ f a₂ → g₁ ≫ φ a₁ = g₂ ≫ φ a₂
T : C
i₁ i₂ : I
g₁ : T ⟶ Z i₁
g₂ : T ⟶ Z i₂
eq : g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
⊢ g₁ ≫ g i₁ ≫ f i₁ = g₂ ≫ g i₂ ≫ f i₂
Module: Mathlib.CategoryTheory.EffectiveEpi.Preserves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ g₁ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₁ = g₂ ≫ (fun a ↦ e.unit.app (X a) ≫ e.inverse.map (ε a)) a₂

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
e : C ≌ D
B : C
α : Type u_3
X : α → C
π : (a : α) → X a ⟶ B
W : D
ε : (a : α) → e.functor.obj (X a) ⟶ W
h :
  ∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
    g₁ ≫ e.functor.map (π a₁) = g₂ ≫ e.functor.map (π a₂) → g₁ ≫ ε a₁ = g₂ ≫ ε a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
this : True → e.functor.map g₁ ≫ ε a₁ = e.functor.map g₂ ≫ ε a₂
⊢ g₁ ≫ e.unit.app (X a₁) ≫ e.inverse.map (ε a₁) = g₂ ≫ e.unit.app (X a₂) ≫ e.inverse.map (ε a₂)
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : l = j
e : c.val j = 0
⊢ c.val i = 0

Tactic:
simpa using

Goal state after:
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : l = j
e : c.val j = 0
⊢ c.val i = 0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case h
I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
o : I := ⋯
k : I
hik : k ⟶ IsCofiltered.min i j
heq : D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b
⊢ D.map (hik ≫ IsCofiltered.minToLeft i j) ≫ a = D.map (hik ≫ IsCofiltered.minToRight i j) ≫ b

Tactic:
simpa using

Goal state after:
case h
I : Type u
inst✝⁴ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝³ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝² : LocallyOfFiniteType f
inst✝¹ : IsCofiltered I
inst✝ : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
a : D.obj i ⟶ X
ha : t.app i = a ≫ f
j : I
b : D.obj j ⟶ X
hb : t.app j = b ≫ f
hab : c.π.app i ≫ a = c.π.app j ≫ b
o : I := IsCofiltered.min i j
k : I
hik : k ⟶ IsCofiltered.min i j
heq : D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b
⊢ D.map hik ≫ D.map (IsCofiltered.minToLeft i j) ≫ a = D.map hik ≫ D.map (IsCofiltered.minToRight i j) ≫ b
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 : I), IsAffine (D.obj i)
i : I
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
this : ∀ (i : Iᵒᵖ), IsAffine (Opposite.unop (D.op.obj i))
j : Iᵒᵖ
f : Opposite.op i ⟶ j
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) s =
    (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) 0
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) s = 0

Tactic:
simpa using

Goal state after:
I : Type u
inst✝² : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝¹ : IsCofiltered I
inst✝ : ∀ (i : I), IsAffine (D.obj i)
i : I
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
this : ∀ (i : Iᵒᵖ), IsAffine (Opposite.unop (D.op.obj i))
j : Iᵒᵖ
f : Opposite.op i ⟶ j
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) s =
    (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) 0
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f.unop))) s = 0
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
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i))))) s) =
    0
⊢ Over.Hom.left f = j.hom

Tactic:
simpa using

Goal state after:
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
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagram D i U).map f)))
      ((ConcreteCategory.hom (Scheme.Hom.appTop ((opensDiagramι D i U).app (Over.mk (𝟙 i))))) s) =
    0
⊢ Over.Hom.left f = j.hom
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ 0 ≤ numBound k₂ D₂ 0

Tactic:
simpa using

Goal state after:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ k₁ ≤ k₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.polynomial.Monic

Tactic:
simpa using

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly.Monic
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

Tactic:
by
  rw [nonsingular_iff', equation_iff_variableChange, equation_zero, ← neg_ne_zero, or_comm,
    nonsingular_zero, variableChange_a₃, variableChange_a₄, inv_one, Units.val_one]
  simp only [variableChange_def]
  congr! 3 <;> ring1

Goal state after:
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 : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  (ConcreteCategory.hom
        (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0
⊢ Over.Hom.left f = j.hom

Tactic:
simpa using

Goal state after:
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 : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
j : Over i
f : j ⟶ Over.mk (𝟙 i)
hf :
  (ConcreteCategory.hom
        (Scheme.Hom.appTop (Scheme.Hom.resLE (D.map (Over.Hom.left f)) (D.map (𝟙 i) ⁻¹ᵁ U) (D.map j.hom ⁻¹ᵁ U) ⋯)))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0
⊢ Over.Hom.left f = j.hom
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := Finsupp.toMultiset (Finsupp.comapDomain Fin.succ (Multiset.toFinsupp d) ⋯)
⊢ 1 ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝ : CommRing R
n✝ n : ℕ
IH :
  ∀ {M : Submodule ℤ R},
    1 ∈ M →
      ∀ (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)),
        (∀ C ∈ S, C.n ≤ k) →
          (∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) →
            ∃ T,
              comap MvPolynomial.C '' S.toSet = T.toSet ∧
                ∀ C ∈ T,
                  C.n ≤ numBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
                    ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S, ∀ (j : Fin C.n), C.g j ∈ coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k * (1 + Multiset.count 0 d)
B : Multiset (Fin n) := Finsupp.toMultiset (Finsupp.comapDomain Fin.succ (Multiset.toFinsupp d) ⋯)
⊢ 1 ∈ M
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
⊢ y₁ = y₂ ∨ y₁ = W.negY x₂ y₂

Tactic:
by
  rw [equation_iff] at h₁ h₂
  rw [← sub_eq_zero, ← sub_eq_zero (a := y₁), ← mul_eq_zero, negY]
  linear_combination (norm := (rw [hx]; ring1)) h₁ - h₂

Goal state after:
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 : (D.obj i).Opens
hU : IsCompact ↑U
s t : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) t

Tactic:
simpa using

Goal state after:
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 : (D.obj i).Opens
hU : IsCompact ↑U
s t : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) t
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) s = (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) t
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
⊢ IsAffineOpen ((D.map j.hom ⁻¹ᵁ U).ι ''ᵁ ⊤)

Tactic:
simpa using

Goal state after:
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)
s : ↑Γ(c.pt, ⊤)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
this✝ : CompactSpace ↥c.pt
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : IsAffineOpen U
hxU : (c.π.app i) x ∈ ↑U
this : ∀ (j : Over i), IsAffine ((opensDiagram D i U).obj j)
j : Over i
t : ↑Γ((opensDiagram D i U).obj j, ⊤)
hj :
  (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app j))) t =
    (s |_ ⋯.functor.obj (Opposite.unop (Opposite.op ⊤))) ⋯
⊢ IsAffineOpen (D.map j.hom ⁻¹ᵁ U)