mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom ((stalkFunctor C x).map α)) ((ConcreteCategory.hom (F.germ U₁ x hxU₁)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map α)) ((ConcreteCategory.hom (F.germ U₂ x hxU₂)) t)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t

Tactic:
rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply] at hst

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
hU₂ : U₂ ∈ B
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (α.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (α.app (op U₂))) t)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
⊢ s = t

Tactic:
choose V m i₁ i₂ heq using fun x : U => F.presheaf.germ_eq x.1 x.2 x.2 s t (h x.1 x.2)

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.obj.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
⊢ s = t
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Semiring R
inst✝⁵ : Module R M
inst✝⁴ : TopologicalSpace M
inst✝³ : TopologicalSpace R
inst✝² : SeparableSpace R
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
s : Set M
hs : IsSeparable s
n : ℕ
⊢ IsSeparable {f | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s}

Tactic:
apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ IsInvertible 0 ↔ Subsingleton M ∧ Subsingleton M₂

Tactic:
refine ⟨fun ⟨e, he⟩ ↦ ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂

case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (c.ι.app i₀)

Tactic:
simp only [← IsColimit.comp_coconePointUniqueUpToIso_inv hc h.isColimitCocone i₀,
    cocone_ι_app, coconeιApp_eq_id, id_comp]

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (hc.coconePointUniqueUpToIso h.isColimitCocone).inv
Module: Mathlib.Algebra.Category.Ring.LinearAlgebra

Goal state before:
pp: A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
⊢ Nontrivial ↑D

Tactic:
let : Field A := hA.toField

Goal state after:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
⊢ Nontrivial ↑D
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
⊢ Cocone F

Tactic:
let x (a : A) : j₀ ⟶ IsFiltered.max j₀ c.pt := (F.obj a).hom ≫ c.ι.app a ≫
      IsFiltered.rightToMax j₀ c.pt

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
this : IsFiltered J
c : Cocone (F ⋙ Under.forget j₀) := cocone (F ⋙ Under.forget j₀) hA
x : A → (j₀ ⟶ IsFiltered.max j₀ c.pt) := fun a ↦ (F.obj a).hom ≫ c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt
⊢ Cocone F
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ ((toSpanSingleton R N (s • x)).compLeft ι) i j = ((RingHom.id S) s • (toSpanSingleton R N x).compLeft ι) i j

Tactic:
dsimp only [coe_comp, coe_single, Function.comp_apply, compLeft_apply, toSpanSingleton_apply,
      RingHom.id_apply, smul_apply, Pi.smul_apply]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ i j • s • x = (s • (toSpanSingleton R N x).compLeft ι) i j
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ z₁ = i₂ (f₁ d + y₂)
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂

Tactic:
map_add,

Goal state after:
R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : g₁ z₁ = i₂ (f₁ d) + i₂ y₂
hd : f₁ d = y₁ - y₂
⊢ π₁ z₁ = π₁ z₂
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePullbacks C
⊢ HasFiniteLimits (Over B)

Tactic:
by
  have := ConstructProducts.over_finiteProducts_of_finiteWidePullbacks (B := B)
  have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
  apply hasFiniteLimits_of_hasEqualizers_and_finite_products

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.left }).hom
    ((pair (Under.mk f) (Under.mk g)).obj { as := WalkingPair.right }).hom
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ m = Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s))

Tactic:
change PushoutCocone f g at s

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m : (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).right ⟶ s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ m = Under.Hom.right (hc.desc (pushoutCoconeEquivBinaryCofan.functor.obj s))
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = p * (ringChar R * r)
hr : q = ringChar R * r
⊢ False

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = p * ringChar R * r
hr : q = ringChar R * r
⊢ False
Module: Mathlib.Algebra.CharP.CharAndCard

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : u * (↑p * r) = 0
⊢ False

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : u * ↑p * r = 0
⊢ False
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ¬ringChar R ∣ t

Tactic:
← ringChar.spec,

Goal state after:
R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ¬↑t = 0
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
hp : Nat.Prime p
n : ℕ
⊢ IsUnit ↑(-↑n) ↔ ¬↑p ∣ -↑n

Tactic:
simp [CharP.isUnit_natCast_iff hp, Int.dvd_neg, Int.ofNat_dvd]

Goal state after:
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
⊢ IsPrimePow q

Tactic:
have q_eq_a_mul_rn : q = r ^ n * a := by rw [Nat.mul_div_cancel' (Nat.ordProj_dvd q r)]

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = r ^ n * a
⊢ IsPrimePow q
Module: Mathlib.Algebra.CharP.Pi

Goal state before:
pp: ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
⊢ ↑x = 0

Tactic:
rw [← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x, h, map_zero]

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
⊢ x⁻¹ ∈ S

Tactic:
obtain ⟨y, hy⟩ := hS.mul_inv_cancel (show (⟨x, hx⟩ : S) ≠ 0 from Subtype.coe_ne_coe.1 hx0)

Goal state after:
case neg
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : ⟨x, hx⟩ * y = 1
⊢ x⁻¹ ∈ S
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ IsUnit ↑↑n

Tactic:
rw [← Ideal.span_singleton_eq_top]
  -- So by contrapositive, we should show the quotient does not have characteristic zero.
  apply not_imp_comm.mp (h.elim (Ideal.span {↑n}))
  intro h_char_zero
  -- In particular, the image of `n` in the quotient should be nonzero.
  apply h_char_zero.cast_injective.ne n.ne_zero
  -- But `n` generates the ideal, so its image is clearly zero.
  rw [← map_natCast (Ideal.Quotient.mk _), Nat.cast_zero, Ideal.Quotient.eq_zero_iff_mem]
  exact Ideal.subset_span (Set.mem_singleton _)

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
x : α
s : Seq α
h h' : (cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
rw [terminates_cons_iff] at h'

Goal state after:
case pos
α : Type u
x : α
s : Seq α
h : (cons x s).Terminates
h' : s.Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
x : α
s : Seq α
h h' : ¬(cons x s).Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
rw [terminates_cons_iff] at h'

Goal state after:
case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ ((empty α).think <|> s) = (empty α <|> s)

Tactic:
← think_empty

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (empty α <|> s.think) = s'
⊢ (empty α <|> s) = (empty α <|> s)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> (empty α).think) = (s <|> empty α)

Tactic:
← think_empty

Goal state after:
case think
α : Type u
c s' s : Computation α
h : (s.think <|> empty α) = s'
⊢ (s <|> empty α) = (s <|> empty α)
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
⊢ v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
set pconts := g.contsAux (n + 1) with pconts_eq

Goal state after:
case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) pconts ifp_n.fr
pconts_eq : pconts = g.contsAux (n + 1)
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ 1 ≤ { b := ⌊ifp_n.fr⁻¹⌋, fr := fract ifp_n.fr⁻¹ }.b

Tactic:
le_floor,

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ ↑1 ≤ ifp_n.fr⁻¹
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
set pconts := g.contsAux (n + 1) with pconts_eq

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ ∀ ⦃b : K⦄, g.partDens.get? n = some b → b ≠ 0

Tactic:
intro _ nth_partDen_eq

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
b✝ : K
nth_partDen_eq : g.partDens.get? n = some b✝
⊢ b✝ ≠ 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0

Tactic:
← mul_assoc,

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * (1 - e₂) * e' = 0