mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s')
⊢ s = cons a s'

Tactic:
obtain ⟨f, al⟩ := s
    injections _ h1 h2
    rw [← h2]
    apply Subtype.ext
    dsimp [tail, cons]
    rw [h1] at f0
    rw [← f0]
    exact (Stream'.eta f).symm

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

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
a : α
s' : Seq α
H : s.destruct = some (a, s')
⊢ motive s

Tactic:
destruct_eq_cons H

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
a : α
s' : Seq α
H : s.destruct = some (a, s')
⊢ motive (Seq.cons a s')
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ (iterate f a).tail = iterate f (f a)

Tactic:
ext n

Goal state after:
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).tail.get n = (iterate f (f a)).get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).get (n + 1) = (iterate f (f a)).get n

Tactic:
induction n with

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

Goal state before:
pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
⊢ s.val n = (pure a).val n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
f : α → α
a : α
n : ℕ
⊢ iterate f (f a) n = map f (iterate f a) n

Tactic:
induction n with

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

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
⊢ s = nil

Tactic:
ext n

Goal state after:
case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ s.get? n = some a✝ ↔ nil.get? n = some a✝
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
⊢ a = b

Tactic:
ext n

Goal state after:
α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
n : ℕ
⊢ a.get n = b.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
xs : Stream' α
⊢ (take n xs).dropLast = take (n - 1) xs

Tactic:
by
  cases n with
  | zero => simp
  | succ n => rw [take_succ', List.dropLast_concat, Nat.add_one_sub_one]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
n : ℕ
⊢ C ((pure a).thinkN n)

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁ = s₂

Tactic:
ext n

Goal state after:
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ s₁.get n = s₂.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
⊢ s₁.get n = s₂.get n

Tactic:
induction n with

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

Goal state before:
pp: case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none) → s.get? n = none

pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none

Tactic:
· rintro ⟨_, k, hkn, hk⟩
    exact le_stable s hkn hk

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m ≤ n, s.get? m = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
n k : ℕ
s : Seq α
⊢ (take (k + 1) s)[n]? = if n < k + 1 then s.get? n else none

Tactic:
take

Goal state after:
α : Type u
n k : ℕ
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take k r)[n]? =
    if n < k + 1 then s.get? n else none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (take (m + 1) s).length ≤ m + 1

Tactic:
take

Goal state after:
case succ
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
⊢ (match s.destruct with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ ↑(s.toList h) = s

Tactic:
ext n

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a✝ : α
⊢ (↑(s.toList h)).get? n = some a✝ ↔ s.get? n = some a✝
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n : ℕ
hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)
⊢ (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
    ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0

Tactic:
induction n with

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

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

Tactic:
by
  by_cases h : (s.map f).Terminates <;> have h' := h <;> rw [terminates_map_iff] at h'
  · rw [length'_of_terminates h, length'_of_terminates h', length_map h]
  · rw [length'_of_not_terminates h, length'_of_not_terminates h']

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ((IntFractPair.stream v n).bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    IntFractPair.stream v n = none ∨ ∃ ifp, IntFractPair.stream v n = some ifp ∧ ifp.fr = 0

Tactic:
cases IntFractPair.stream v n

Goal state after:
case none
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (none.bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    none = none ∨ ∃ ifp, none = some ifp ∧ ifp.fr = 0

case some
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
val✝ : IntFractPair K
⊢ ((some val✝).bind fun ap_n ↦ if ap_n.fr = 0 then none else some (IntFractPair.of ap_n.fr⁻¹)) = none ↔
    some val✝ = none ∨ ∃ ifp, some val✝ = some ifp ∧ ifp.fr = 0
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
n : ℕ
⊢ IntFractPair.stream (↑a) (n + 1) = none

Tactic:
induction n with

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : Int.fract v ≠ 0
n : ℕ
⊢ IntFractPair.stream v (n + 1) = IntFractPair.stream (Int.fract v)⁻¹ n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ nil.drop n = nil

Tactic:
induction n with

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

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
n : ℕ
⊢ (of ↑a).s.get? n = none

Tactic:
induction n with

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

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
n✝ : ℕ
a✝ : (of ↑a).convs' n✝ = ↑a
⊢ (of ↑a).convs' (n✝ + 1) = ↑a

Tactic:
rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]
    exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _

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

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ (of ↑a).convs' n = ↑a

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
n : ℕ
⊢ motive (s.drop n)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (fib n).Coprime (fib (n + 1))

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ (s.drop i).get? (k + 1)
hj : j = i + k + 1
⊢ R x y

Tactic:
have := all_coind_drop_motive motive base (fun hd tl ih ↦ (step hd tl ih).right) i

Goal state after:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ (s.drop i).get? (k + 1)
hj : j = i + k + 1
this : motive (s.drop i)
⊢ R x y
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
⊢ ∀ {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

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
h : Pairwise R s
n : ℕ
⊢ Pairwise R (s.drop n)

Tactic:
induction n with

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

Goal state before:
pp: α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
n : ℕ
hb : b.drop n ≠ nil
⊢ motive (a.drop n) (b.drop n)

Tactic:
induction n with

Goal state after:
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
nth_stream_eq_none : IntFractPair.stream v n = none
⊢ v = (of v).convs (n - 1)

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib (n + 1) = ∑ k ∈ Finset.range n, fib k + 1

Tactic:
induction n with

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n

Tactic:
induction n with

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s

Tactic:
ext n

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
a✝ : Pair K
⊢ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n = some a✝ ↔ (of v).s.get? n = some a✝
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

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

Tactic:
induction n with

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
ifp_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
this : ↑⌊ifp_n.fr⁻¹⌋ ≤ ifp_n.fr⁻¹
⊢ ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹

Tactic:
obtain ⟨_, ifp_n_fr⟩ := ifp_n
    have : ifp_n_fr ≠ 0 := by
      intro h
      simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
    have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
      simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
    rwa [← this]

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
c : ContFract K
⊢ (↑↑c).convs = (↑↑c).convs'

Tactic:
ext n

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
c : ContFract K
n : ℕ
⊢ (↑↑c).convs.get n = Stream'.get (↑↑c).convs' n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
⊢ (fun P ↦ ⟨P.toPoly, ⋯⟩) ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f) =
    f

Tactic:
ext n

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
⊢ (↑((fun P ↦ ⟨P.toPoly, ⋯⟩)
            ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f))).coeff
      n =
    (↑f).coeff n
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
g : GenContFract K := of v
⊢ 0 ≤ ((of v).contsAux n).b

Tactic:
induction n with

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ map φ P = { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }

Tactic:
apply_fun toPoly

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (map φ P).toPoly =
    { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }.toPoly

case inj
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ Function.Injective toPoly
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ y * x = 0 ∧ x + y = 1

Tactic:
simp [iff_ortho_complete, Pairwise, Fin.forall_fin_two, and_assoc]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: 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 : ℕ
e : Fin n → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin n), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
induction n with

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
⊢ x * (1 - x) = 0 ∧ (1 - x) * x = 0 ↔ IsIdempotentElem x

Tactic:
simp [mul_sub, sub_mul, IsIdempotentElem, sub_eq_zero, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case h.inr
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
i j : n
qj : q ≠ j
⊢ (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid

Tactic:
simp [N, qj, sum_apply, mul_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case a
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) n ≤
    ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) (finrank K V)

Tactic:
change (f.genEigenspace μ) n ≤ (f.genEigenspace μ) (finrank K V)
    rw [genEigenspace_nat, genEigenspace_nat]
    apply ker_pow_le_ker_pow_finrank

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
this : Algebra R R' := compHom R' (algebraMap R R[ε])
⊢ f = g

Tactic:
let f' : R[ε] →ₐ[R] R' :=
    { toRingHom := f
      commutes' _ := rfl }

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
this : Algebra R R' := compHom R' (algebraMap R R[ε])
f' : R[ε] →ₐ[R] R' := { toRingHom := f, commutes' := ⋯ }
⊢ f = g
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)

Goal state after:
case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

case neg
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquiv R M M).symm

Tactic:
rw [dualTensorHomEquiv_eq_dualTensorHomEquivOfBasis (Module.Free.chooseBasis R M)]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis (Free.chooseBasis R M)).symm
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
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
⊢ IsNilpotent ((trace R M) f)

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ IsNilpotent ((trace R M) f)

case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ IsNilpotent ((trace R M) f)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α × Bool
⊢ reduce (List.replicate n x) = List.replicate n x

Tactic:
induction n with

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀

Tactic:
· rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(FreeGroup α) = max #α ℵ₀

Tactic:
classical
  apply le_antisymm
  · apply (mk_le_of_injective (FreeGroup.toWord_injective (α := α))).trans_eq
    simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]
    obtain hα | hα := lt_or_ge #α ℵ₀
    · simp only [hα.le, max_eq_right, max_eq_right_iff]
      exact (mul_lt_aleph0 hα natCast_lt_aleph0).le
    · rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα
  · apply max_le
    · exact mk_le_of_injective FreeGroup.of_injective
    · simp

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : M₂
⊢ ∃ a, i₃ a = g₂ (i₂ y)

Tactic:
exact ⟨f₂ y, congr($hc₂ y).symm⟩

Goal state after:
Module: Mathlib.Algebra.FiveLemma

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_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : M₂
⊢ ∃ a, i₃ a = g₂ (i₂ y)

Tactic:
exact ⟨f₂ y, congr($hc₂ y).symm⟩

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (∑ i ∈ insert a✝ s✝, f i).den ∣ (insert a✝ s✝).lcm fun i ↦ (f i).den

Tactic:
rw [Finset.sum_insert has, Finset.lcm_insert]
    exact (Rat.add_den_dvd_lcm _ _).trans (lcm_dvd_lcm dvd_rfl ih)

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case re
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).re = (s • t • x).re

Tactic:
exact smul_assoc _ _ _

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case imI
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ ((s • t) • x).imI = (s • t • x).imI

Tactic:
exact smul_assoc _ _ _

Goal state after: