mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : MvPolynomial (Fin n) ↑R →ₐ[↑R] ↑S
h₁ : Function.Surjective ⇑π
h₂ : (ker π.toRingHom).FG
⊢ iP ≫ CommRingCat.ofHom ↑π = f

Tactic:
ext1

Goal state after:
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
f : R ⟶ S
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hg : ∀ (i : J), f ≫ g = α.app i ≫ c.ι.app i
hc' : IsColimit ((forget CommRingCat).mapCocone c)
this : Algebra ↑R ↑S := ⋯
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : MvPolynomial (Fin n) ↑R →ₐ[↑R] ↑S
h₁ : Function.Surjective ⇑π
h₂ : (ker π.toRingHom).FG
⊢ CommRingCat.Hom.hom (iP ≫ CommRingCat.ofHom ↑π) = CommRingCat.Hom.hom f
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_1
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := CommRingCat.of (MvPolynomial (Fin n) ↑R)
iP : R ⟶ P := CommRingCat.ofHom MvPolynomial.C
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom (iP ≫ π)).toAlgebra
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
⊢ π ≫ g =
    CommRingCat.ofHom
        (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x_1 ↦
          (ConcreteCategory.hom (F.map (hi x_1))) (x x_1)) ≫
      c.ι.app i

Tactic:
ext1

Goal state after:
case refine_1
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
F : J ⥤ CommRingCat
α : (Functor.const J).obj R ⟶ F
S : CommRingCat
c : Cocone F
hc : IsColimit c
inst✝ : PreservesColimit F (forget CommRingCat)
g : S ⟶ c.pt
hc' : IsColimit ((forget CommRingCat).mapCocone c)
n : ℕ
P : CommRingCat := ⋯
iP : R ⟶ P := ⋯
π : P ⟶ S
hg : ∀ (i : J), (iP ≫ π) ≫ g = α.app i ≫ c.ι.app i
this : Algebra ↑R ↑S := ⋯
hn : ∃ f, Function.Surjective ⇑f ∧ (ker f.toRingHom).FG
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
s : Finset ↑P
hs : Ideal.span ↑s = ker (CommRingCat.Hom.hom π)
j : Fin n → J
x : (i : Fin n) → (fun X ↦ X) ((F ⋙ forget CommRingCat).obj (j i))
h :
  ∀ (i : Fin n),
    (ConcreteCategory.hom (((forget CommRingCat).mapCocone c).ι.app (j i))) (x i) =
      (ConcreteCategory.hom (π ≫ g)) (MvPolynomial.X i)
i : J
hi : (a : Fin n) → j a ⟶ i
⊢ CommRingCat.Hom.hom (π ≫ g) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (MvPolynomial.eval₂Hom (CommRingCat.Hom.hom (α.app i)) fun x_1 ↦
            (ConcreteCategory.hom (F.map (hi x_1))) (x x_1)) ≫
        c.ι.app i)
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
N₃ : Type u_7
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₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[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₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
⊢ σ (ι₃ x) - f₁ y ∈ Set.range ⇑ι₂

Tactic:
by
      rw [← hι₂, map_sub, ← H₂, ← hy, sub_eq_zero]; exact congr($h₁ y)

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 : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ m = Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯

Tactic:
ext1

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m = Over.Hom.left (Over.homMk (hc.lift (pullbackConeEquivBinaryFan.inverse.obj s)) ⋯)
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 : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ m = Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯

Tactic:
ext1

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 : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ Under.Hom.right m =
    Under.Hom.right (Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: 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)
⊢ IsPrimePow q

Tactic:
let r := ringChar K

Goal state after:
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
⊢ IsPrimePow q
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: 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
⊢ IsPrimePow q

Tactic:
let n := q.factorization r

Goal state after:
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
⊢ IsPrimePow q
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul.tmul.tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ e₄'.symm ((r ⊗ₜ[R] s • x ⊗ₜ[R] z) ⊗ₜ[S] y) = r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)

Tactic:
ext1

Goal state after:
case tmul.tmul.tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := ⋯
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A := ⋯
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) := ⋯
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) := ⋯
y : ↥(RingHom.ker (algebraMap S T))
x : A
z : S
r : A
s : S
⊢ ↑(e₄'.symm ((r ⊗ₜ[R] s • x ⊗ₜ[R] z) ⊗ₜ[S] y)) = ↑(r ⊗ₜ[R] s • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y))
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
r' x : A ⊗[R] S
y : ↥(RingHom.ker (algebraMap S T))
⊢ e₄'.symm (r' • x ⊗ₜ[S] y) = r' • e₄'.symm (x ⊗ₜ[S] y)

Tactic:
induction x with
        | zero => simp only [zero_tmul, smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, add_tmul, LinearEquiv.map_add, *]
        | tmul x z =>
        induction r' with
        | zero => simp only [zero_smul, LinearEquiv.map_zero]
        | add x y _ _ => simp only [add_smul, LinearEquiv.map_add, *]
        | tmul r s =>
        rw [smul_tmul']
        ext1
        dsimp [e₄', ePp, φ]
        change ((r * x) ⊗ₜ[R] ((s * z) * y.1)) = (r ⊗ₜ[R] s) * (x ⊗ₜ[R] (z * y.1))
        rw [Algebra.TensorProduct.tmul_mul_tmul, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)

Tactic:
RingHom.ker_eq_comap_bot

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)

Tactic:
rw [CharP.quotient_iff, RingHom.ker_eq_comap_bot]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ (∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
← natCast_zsmul ψ,

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ ↑n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ (cons a ⟨f, al⟩).destruct = some (a, ⟨f, al⟩)

Tactic:
by
    unfold cons destruct Functor.map
    apply congr_arg fun s => some (a, s)
    apply Subtype.ext; dsimp [tail]

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail

Tactic:
unfold interleave corecOn

Goal state after:
α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x ↦
          match x with
          | (s₁, snd) => s₁.head)
        (fun x ↦
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      (fun x ↦
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mp
α : Type u
x : α
s : Seq α
n : ℕ
h : (cons x s).TerminatedAt n
⊢ s.Terminates

pp: case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates

Tactic:
· exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩

Goal state after:
case mpr
α : Type u
x : α
s : Seq α
n : ℕ
h : s.TerminatedAt n
⊢ (cons x s).Terminates
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = (initsCore (a :: l) s).get (n + 1)

Tactic:
inits_core_eq (a :: l) s

Goal state after:
case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ (initsCore (a :: (l ++ [s.head])) s.tail).get n = ((a :: l) :: initsCore (a :: l ++ [s.head]) s.tail).get (n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
simp only [think_bind, results_think_iff] at h

Goal state after:
case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.bind f).Results b n
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Computation α
m : a ∈ s
⊢ f a ∈ map f s

Tactic:
by
  rw [← bind_pure]; apply mem_bind m; apply ret_mem

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

Goal state before:
pp: case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ (map f s).length' = s.length'

Tactic:
length'_of_not_terminates h,

Goal state after:
case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ ⊤ = s.length'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ LiftRelAux (Function.swap R) (Function.swap C) (Sum.inl b) ca.destruct ↔ ∃ a, a ∈ ca ∧ R a b

Tactic:
LiftRelAux.ret_left

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
b : β
ca : Computation α
⊢ (∃ b_1, b_1 ∈ ca ∧ Function.swap R b b_1) ↔ ∃ a, a ∈ ca ∧ R a b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
⊢ zipWith f s nil = nil

Tactic:
ext1

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
n✝ : ℕ
⊢ (zipWith f s nil).get? n✝ = nil.get? n✝
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ n.fastFibAux.1 = fib n

Tactic:
fastFibAux_eq

Goal state after:
n : ℕ
⊢ (fib n, fib (n + 1)).1 = fib n
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
⊢ n ≥ N → |v - (of v).convs n| < ε

Tactic:
n_ge_N

Goal state after:
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
⊢ |v - (of v).convs n| < ε
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly = C P.d

Tactic:
of_b_eq_zero ha hb,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ C P.c * X + C P.d = C P.d
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.leadingCoeff = P.c

Tactic:
of_b_eq_zero ha hb,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ (C P.c * X + C P.d).leadingCoeff = P.c
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.degree = 1

Tactic:
of_b_eq_zero ha hb,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ (C P.c * X + C P.d).degree = 1
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.natDegree = 1

Tactic:
of_b_eq_zero ha hb,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ (C P.c * X + C P.d).natDegree = 1
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : ↑ifp_succ_n.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
⊢ gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b

Tactic:
← ifp_succ_n_b_eq_gp_b

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : ↑ifp_succ_n.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
⊢ ↑ifp_succ_n.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ x * y = 0 ∧ y * x = 0 ∧ x + y = 1 ↔ x * y = 0 ∧ x + y = 1

Tactic:
and_left_comm,

Goal state after:
R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ y * x = 0 ∧ x * y = 0 ∧ x + y = 1 ↔ x * y = 0 ∧ x + y = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ IsIdempotentElem (1 - (1 - x ^ n) ^ n)

Tactic:
by
  have : (x - x ^ 2) ^ n ∣ (1 - (1 - x ^ n) ^ n) - (1 - (1 - x ^ n) ^ n) ^ 2 := by
    conv_rhs => rw [pow_two, ← mul_one_sub, sub_sub_cancel]
    nth_rw 1 3 [← one_pow n]
    rw [← (Commute.one_left x).mul_geom_sum₂, ← (Commute.one_left (1 - x ^ n)).mul_geom_sum₂]
    simp only [sub_sub_cancel, one_pow, one_mul]
    rw [Commute.mul_pow, Commute.mul_mul_mul_comm, ← Commute.mul_pow, mul_one_sub, ← pow_two]
    · exact ⟨_, rfl⟩
    · simp
    · refine .pow_right (.sub_right (.one_right _) (.sum_left _ _ _ fun _ _ ↦ .pow_left ?_ _)) _
      simp
    · exact .sub_left (.one_left _) (.sum_right _ _ _ fun _ _ ↦ .pow_right rfl _)
  rwa [hx, zero_dvd_iff, sub_eq_zero, eq_comm, pow_two] at this

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_2
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
⊢ (f 1 - f e₂) * f e' = f e'

Tactic:
map_one,

Goal state after:
case refine_2
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
⊢ (1 - f e₂) * f e' = f e'