mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ c₂ : PullbackCone f g
a : c₁ ⟶ c₂
⊢ ∀ (j : Discrete WalkingPair),
    Over.homMk a.hom ⋯ ≫ (BinaryFan.mk (Over.homMk c₂.fst ⋯) (Over.homMk c₂.snd ⋯)).π.app j =
      (BinaryFan.mk (Over.homMk c₁.fst ⋯) (Over.homMk c₁.snd ⋯)).π.app j

Tactic:
rintro (_ | _) <;> cat_disch

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 : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m : s.pt ⟶ (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ m ≫ c.pt.hom = (pullbackConeEquivBinaryFan.functor.obj s).pt.hom

Tactic:
simp [← hm₁, dsimp% c.fst.w]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk ⊤ (𝟙 X) ⋯
⊢ a.left = Y.hom

Tactic:
rw [← Over.w a]

Goal state after:
T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Over ⊤ X
a : Y ⟶ Over.mk ⊤ (𝟙 X) ⋯
⊢ a.left = a.left ≫ (Over.mk ⊤ (𝟙 X) ⋯).hom
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₁ c₂ : PushoutCocone f g
a : c₁ ⟶ c₂
⊢ ∀ (j : Discrete WalkingPair),
    (BinaryCofan.mk (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯)).ι.app j ≫ Under.homMk a.hom ⋯ =
      (BinaryCofan.mk (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)).ι.app j

Tactic:
rintro (_ | _) <;> cat_disch

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring A
f : R →+* A
p q : ℕ
inst✝¹ : CharP R p
inst✝ : CharP A q
⊢ ↑p = 0

Tactic:
rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro U V k
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Under Q Z) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hg ⋙ map Q hf).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro U V k
    ext
    simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
by
  cases CharP.exists R with
  | intro p p_charP =>
    by_cases h : p = 0
    · rw [h] at p_charP
      have h0 : CharZero R := CharP.charP_to_charZero R
      exact split_equalCharZero_mixedCharZero R h_equal h_mixed
    · exact h_pos p h p_charP

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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ∃ k k_1, (z * k_1 + ↑↑k) • p = z • r

Tactic:
← h

Goal state after:
case mp
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ ∃ k_1 k_2, (z * k_2 + ↑↑k_1) • p = k • p
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:
rw [← natCast_zsmul ψ, ← natCast_zsmul θ,
    zmultiples_zsmul_eq_zsmul_iff (Int.natCast_ne_zero.mpr hz), Int.cast_natCast]

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

Goal state before:
pp: case some
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = get? ⟨f, al⟩ 0 :: f.tail

Tactic:
exact (Stream'.eta f).symm

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

Goal state before:
pp: case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ ((Corec.f f (some b)).fst :: corec' (Corec.f f) (Corec.f f (some b)).snd).tail = corec' (Corec.f f) (some b')

Tactic:
Stream'.tail_cons

Goal state after:
case some
α : Type u
β : Type v
f : β → Option (α × β)
b : β
a : α
b' : β
h : f b = some (a, b')
⊢ corec' (Corec.f f) (Corec.f f (some b)).snd = corec' (Corec.f f) (some b')
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ⟨f, al⟩.val 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ f = Stream'.cons (⟨f, al⟩.val 0) f.tail

Tactic:
exact (Stream'.eta f).symm

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

Goal state before:
pp: case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ (Stream'.cons (Corec.f f (Sum.inr b)).fst (Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd)).tail =
    Stream'.corec' (Corec.f f) (Sum.inr b')

Tactic:
Stream'.tail_cons

Goal state after:
case inr
α : Type u
β : Type v
f : β → α ⊕ β
b b' : β
h : f b = Sum.inr b'
⊢ Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).snd = Stream'.corec' (Corec.f f) (Sum.inr b')
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a b : α
s : Seq α
⊢ a = b ∨ a ∈ s → a ∈ cons b s

Tactic:
rintro (rfl | m)

Goal state after:
case inl
α : Type u
a : α
s : Seq α
⊢ a ∈ cons a s

case inr
α : Type u
a b : α
s : Seq α
m : a ∈ s
⊢ a ∈ cons b s
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ (x ++ₛ a).get (x.length + n) = a.get n

Tactic:
by
  induction x <;> simp [Nat.succ_add, *, cons_append_stream]

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

Goal state before:
pp: α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = s.val n
⊢ (s.val n).isSome = true

Tactic:
← h

Goal state after:
α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : some a = s.val n
⊢ (some a).isSome = true
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ a ∈ s

Tactic:
← h

Goal state after:
α : Type u
s : Computation α
h✝ : s.Terminates
a : α
h : s.get = a
⊢ s.get ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a b : α
m n : ℕ
h1 : s.Results a m
h2 : s.Results b n
this✝ this : s.Terminates
⊢ m = n

Tactic:
rw [← h1.length, h2.length]

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

Goal state before:
pp: α : Type u
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ map id ⟨f, al⟩ = ⟨f, al⟩

Tactic:
apply Subtype.ext; simp only [map, comp_apply, id_eq]
    have e : @Option.rec α (fun _ => Option α) none some = id := by ext ⟨⟩ <;> rfl
    have h : ((fun x : Option α => x) = id) := rfl
    simp [e, h, Stream'.map_id]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ (s.bind f).bind g = s.bind fun x ↦ (f x).bind g

Tactic:
apply
    eq_of_bisim fun c₁ c₂ =>
      c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x : α => bind (f x) g
  · intro c₁ c₂ h
    match c₁, c₂, h with
    | _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
    | _, _, Or.inr ⟨s, rfl, rfl⟩ =>
      induction s using recOn with
      | pure s =>
        simp only [BisimO, ret_bind]; generalize f s = fs
        induction fs using recOn with
        | pure t => rw [ret_bind]; rcases destruct (g t) with b | cb <;> simp
        | think => simp
      | think s => simpa [BisimO] using Or.inr ⟨s, rfl, rfl⟩
  · exact Or.inr ⟨s, rfl, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1 : s✝.think.Results a m✝
m' : ℕ
h : s✝.Results a m' ∧ m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + m✝)

Tactic:
obtain ⟨h1, e⟩ := h

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
s✝ : Computation α
h3 : ∀ {m : ℕ}, s✝.Results a m → (s✝.bind f).Results b (n + m)
m✝ : ℕ
h1✝ : s✝.think.Results a m✝
m' : ℕ
h1 : s✝.Results a m'
e : m✝ = m' + 1
⊢ (s✝.bind f).think.Results b (n + m✝)
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) (Polynomial.map (f' i₁ i h1) p₁ + Polynomial.map (f' i₂ i h2) p₂) =
    q₁ + q₂

Tactic:
rw [Polynomial.map_add, map_map, map_map, ← ih₁, ← ih₂]

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ +
      Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ =
    Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) s'.destruct s.destruct

Tactic:
← h

Goal state after:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ ↦ (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) s'.destruct s.destruct

Tactic:
← h

Goal state after:
α : Type u
c s' s : Computation α
h : (s <|> empty α) = s'
⊢ BisimO (fun c₁ c₂ ↦ (c₂ <|> empty α) = c₁) (s <|> empty α).destruct s.destruct
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
h : c₁ ~ c₂
⊢ c₁.Terminates ↔ c₂.Terminates

Tactic:
simp only [terminates_iff, exists_congr h]

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0
⊢ ∀ (a : DirectLimit G f), (lift G f P g Hg) a = 0 → a = 0

Tactic:
intro z

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0
z : DirectLimit G f
⊢ (lift G f P g Hg) z = 0 → z = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = Int.fract v + ↑⌊v⌋

Tactic:
Int.fract_add_floor

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = v
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
h : x = 0
⊢ (Ring.DirectLimit.of G f i) 0 = 0

Tactic:
(Ring.DirectLimit.of _ _ _).map_zero

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
h : x = 0
⊢ 0 = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts) →
      ∃ conts, (of v).contsAux n = Pair.map Rat.cast conts

Tactic:
clear n
      let g := of v
      intro n IH
      rcases n with (_ | _ | n)
      -- n = 0
      · suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]
        use Pair.mk 1 0
        simp
      -- n = 1
      · suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [contsAux]
        use Pair.mk ⌊v⌋ 1
        simp [g]
      -- 2 ≤ n
      · obtain ⟨pred_conts, pred_conts_eq⟩ := IH (n + 1) <| lt_add_one (n + 1)
        -- invoke the IH
        rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n
        -- option.none
        · use pred_conts
          have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
            contsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
          simp only [g, this, pred_conts_eq]
        -- option.some
        · -- invoke the IH a second time
          obtain ⟨ppred_conts, ppred_conts_eq⟩ :=
            IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1
          obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K) :=
            of_partNum_eq_one_and_exists_int_partDen_eq s_ppred_nth_eq
          -- finally, unfold the recurrence to obtain the required rational value.
          simp only [g, a_eq_one, b_eq_z,
            contsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
          use nextConts 1 (z : ℚ) ppred_conts pred_conts
          cases ppred_conts; cases pred_conts
          simp [nextConts, nextNum, nextDen]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = ↑Aₙ
Bₙ : ℚ
nth_den_eq : (of v).dens n = ↑Bₙ
⊢ (of v).convs n = ↑(Aₙ / Bₙ)

Tactic:
simp [nth_num_eq, nth_den_eq, conv_eq_num_div_den]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (n + 1) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(n + 1)

Tactic:
intro ifp_succ_n stream_succ_nth_eq

Goal state after:
case succ
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
ifp_succ_n : IntFractPair ℚ
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(n + 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 = 1
a✝ : Nontrivial R
⊢ P.toPoly.leadingCoeff = 1

Tactic:
leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero),

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
a✝ : Nontrivial R
⊢ P.b = 1
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
· exact Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∈ s
⊢ e i * ∑ j ∈ s, e j = e i

Tactic:
classical
  simp [Finset.mul_sum, he.mul_eq, h]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
i : I
s : Finset I
h : i ∉ s
⊢ e i * ∑ j ∈ s, e j = 0

Tactic:
classical
  simp [Finset.mul_sum, he.mul_eq, h]

Goal state after:
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →ₗ[K] W := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
this : ∀ (A : End K V) (x : V), T (A x) = (f A) (T x)
w : W
⊢ ∃ a, T a = w

Tactic:
obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz
    exact ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _)

Goal state after:
case succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
e' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n : ℕ
⊢ (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂

Tactic:
induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this : Module.Finite R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
have := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝ : Module.Finite R M
this : Free R M
⊢ (trace R N) (e.conj f) = (trace R M) f
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * (x⁻¹ * x)

Tactic:
inv_mul_cancel₀ hx0

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * 1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Prop
L2 L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = L2 ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

Tactic:
by cases L2 <;> injections

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: case inl
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝ : Subsingleton R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

pp: case inr
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝ : Nontrivial R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
· exact (cardinalMk_eq_one R X).trans_le (le_max_of_le_right one_le_aleph0)

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
X : Type v
h✝ : Nontrivial R
⊢ #(FreeAlgebra R X) ≤ max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
q : ℚ
⊢ ↑(normSq ↑q) = ↑q ^ 2

Tactic:
rw [← coe_ratCast, normSq_coe, coe_pow]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
x : R
⊢ Δ_[1] (fun r ↦ r ^ j) x = (∑ i ∈ range j, j.choose i • fun r ↦ r ^ i) x

Tactic:
simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
x : R
⊢ Δ_[1] (fun r ↦ r ^ (n + 1)) x = (∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i) x

Tactic:
simp [nsmul_eq_mul, fwdDiff, add_pow, sum_range_succ, mul_comm]

Goal state after: