mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: 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
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
⊢ f x⁻¹ ∈ S

Tactic:
map_inv₀ f x

Goal state after:
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
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L'
x : L
hx : x ∈ (Subalgebra.comap f S.toSubalgebra).carrier
⊢ (f x)⁻¹ ∈ S
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s : Seq α
m n : ℕ
h : m ≤ n
⊢ s.get? m = none → s.get? n = none

Tactic:
obtain ⟨f, al⟩ := s
  induction h with | refl => exact id | step _ IH => exact fun h2 ↦ al (IH h2)

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ ((Corec.f f o).fst :: corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = none →
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none

Tactic:
exact IH (Corec.f f o).2

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.cons (Corec.f f o).fst (Stream'.corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = some a' →
    Stream'.cons (Corec.f f (Corec.f f o).snd).fst (Stream'.corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd)
        (n + 1) =
      some a'

Tactic:
exact IH (Corec.f f o).2

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

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

Tactic:
inits_tail,

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ (s : Stream' α), s.inits.get n = take n.succ s
s : Stream' α
⊢ (initsCore [s.head, s.tail.head] s.tail.tail).get n = s.head :: (initsCore [s.tail.head] s.tail.tail).get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ zip appendStream' s.inits s.tails = const s

Tactic:
ext
  simp

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

Goal state before:
pp: α : Type u
x : α
k : ℕ
ih : ∀ {s : Seq α} {n : ℕ}, k < n → s.get? k = some x → x ∈ take n s
s : Seq α
h_get : s.get? (k + 1) = some x
l : ℕ
h_mn : k + 1 < k + 1 + l + 1
y : α
hy : s.get? 0 = some y
⊢ k < k + 1 + l

Tactic:
lia

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

Goal state before:
pp: case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
rw [convs'Aux] at this

Goal state after:
case succ.some
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this✝ : s.tail.TerminatedAt n
this :
  (match s.tail.head with
    | none => 0
    | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
    convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
⊢ b = b'

Tactic:
rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩

Goal state after:
α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b = b'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case e'_3
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ k + 1 + m = k + (m + 1)

Tactic:
lia

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

Goal state before:
pp: case e'_3.coe
α : Type u
n : ℕ
x : α
s : Seq α
m : ℕ
⊢ m + 1 - (n + 1) = m - n

Tactic:
lia

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
m n : ℕ
h : m < n
i : ℕ
⊢ n + i ≠ m

Tactic:
lia

Goal state after:
Module: Mathlib.Data.Nat.DvdSequence

Goal state before:
pp: f : ℕ → ℕ
hf : IsStrongDvdSequence f
a b : ℕ
hab : a ∣ b
⊢ f a ∣ f b

Tactic:
simpa [gcd_eq_left hab, gcd_eq_left_iff_dvd] using hf a b

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
n : ℕ
hx : x ∈ (Seq.cons hd tl).get? (n + 1)
h_ij : n + 1 < k + 1
⊢ n < k

Tactic:
lia

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
i j : ℕ
h_ij : i < j
⊢ i + 1 < j + 1

Tactic:
lia

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
n : ℕ
hx : some x = tl.get? n
⊢ 0 < n + 1

Tactic:
lia

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

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i : ℕ
x : α
hx : x ∈ s.get? i
k : ℕ
ih : ∀ y ∈ s.get? (i + k + 1), R x y
y : α
hy : y ∈ s.get? (i + (k + 1) + 1)
⊢ i + k + 1 ≤ i + (k + 1) + 1

Tactic:
lia

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

Goal state before:
pp: case pos
α : 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
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
⊢ b.length' ≤ a.length'

Tactic:
simp only [length'_of_terminates ha, length'_le_iff]

Goal state after:
case pos
α : 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
this : ∀ (n : ℕ), b.drop n ≠ nil → motive (a.drop n) (b.drop n)
ha : a.Terminates
⊢ b.TerminatedAt (a.length ha)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos.cons.coe
α : 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
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : ¬cons b_hd b_tl = nil
a_hd : α
a_tl : Seq α
right✝ : motive a_tl b_tl
u : ℕ
ha' : 0 = u + 1
⊢ False

Tactic:
lia

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

Goal state before:
pp: case some
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - ↑n
this✝¹ : fract_q_num - ↑n = -1
this✝ : 0 ≤ ifp.fr
this : 0 ≤ ifp.fr.num
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
lia

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

Goal state before:
pp: case h₂
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 : ℕ := ⋯
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := ⋯
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := ⋯
nB : K := ⋯
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ 1 ≤ 2

Tactic:
lia

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

Goal state before:
pp: case succ.inl
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
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ g.convs n = g.convs' n

Tactic:
IH _

Goal state after:
case succ.inl
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
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ g.convs' n = g.convs' n

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
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
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
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
⊢ ¬n + 2 ≤ 1

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ 0 * X ^ 3 + C P.b * X ^ 2 + C P.c * X + C P.d = C P.b * X ^ 2 + C P.c * X + C P.d

Tactic:
zero_mul,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ 0 + C P.b * X ^ 2 + C P.c * X + C P.d = C P.b * X ^ 2 + C P.c * X + 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
⊢ 0 * X ^ 2 + C P.c * X + C P.d = C P.c * X + C P.d

Tactic:
zero_mul,

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ 0 + C P.c * X + C P.d = C P.c * X + 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
⊢ 0 * X + C P.d = C P.d

Tactic:
zero_mul,

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
⊢ 0 + C P.d = C P.d
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.inl
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
terminated : g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

pp: case succ.inr
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
· -- terminating case
      rcases n with - | n
      · simp
      · have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
        simp only [g, this, IH]

Goal state after:
case succ.inr
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b
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)
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
have n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1) := by
      rcases n with - | n'
      · simp
      · have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
        have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
        exact Or.inr this

Goal state after:
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)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
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)
⊢ pA * B - pB * A = (-1) ^ (n' + 1)

Tactic:
simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n

Goal state after:
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
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)
n_eq_zero_or_not_terminatedAt_pred_n : ¬g.TerminatedAt (n' + 1 - 1)
⊢ pA * B - pB * A = (-1) ^ (n' + 1)
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}
⊢ ((P.a ≠ 0 ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
and_iff_right ha,

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}
⊢ (x ≠ y ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
he : OrthogonalIdempotents e
i j : I
⊢ e i * e j = if i = j then e i else 0

Tactic:
split
  · simp [*, (he.idem j).eq]
  · exact he.ortho ‹_›

Goal state after:
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:
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: 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 : ℕ
hn : (e₁ - e₂) ^ n = 0
this : 0 * 0 * (e₁ - e₂) = e₁ - e₂
⊢ e₁ = e₂

Tactic:
zero_mul,

Goal state after:
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 : ℕ
hn : (e₁ - e₂) ^ n = 0
this : 0 * (e₁ - e₂) = e₁ - e₂
⊢ 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 : ℕ
hn : (e₁ - e₂) ^ n = 0
this : 0 * (e₁ - e₂) = e₁ - e₂
⊢ e₁ = e₂

Tactic:
zero_mul,

Goal state after:
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 : ℕ
hn : (e₁ - e₂) ^ n = 0
this : 0 = e₁ - e₂
⊢ 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 : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ = e₂

Tactic:
have : (e₁ - e₂) ^ 3 = (e₁ - e₂) := by
    simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]
    simp only [← mul_assoc, he₂.eq]
    abel
  obtain ⟨n, hn⟩ := H
  have : (e₁ - e₂) ^ (2 * n + 1) = (e₁ - e₂) := by
    clear hn; induction n <;> simp [mul_add, add_assoc, pow_add _ (2 * _) 3, ← pow_succ, *]
  rwa [pow_succ, two_mul, pow_add, hn, zero_mul, zero_mul, eq_comm, sub_eq_zero] at this

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ k = i + (k - i)

Tactic:
lia

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

Goal state before:
pp: case e'_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ ⨆ l, ((f - μ • 1) ^ l).ker = ⨆ x, ⨆ l, ⨆ (_ : ↑l ≤ WithTop.coeOrderHom.toOrderHom x), ((f - μ • 1) ^ l).ker

Tactic:
rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]

Goal state after:
case e'_2
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ sSup (range fun l ↦ ((f - μ • 1) ^ l).ker) = sSup (range fun x ↦ ((f - μ • 1) ^ (↑x).2).ker)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ Commute ε x

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace = ((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace

Tactic:
LinearMap.toMatrix_comp _ b,

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace =
    ((toMatrix b c) (f ∘ₗ id) * (toMatrix c b) id).trace
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
⊢ (↑fe).1 a + 0 * (↑fe).2 = (↑fe).1 a

Tactic:
zero_mul,

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) }
a : A
⊢ (↑fe).1 a + 0 = (↑fe).1 a
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
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (((llcomp R M N M).compr₂ (trace R M)) g) f = (((llcomp R N M N).flip.compr₂ (trace R N)) g) f
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Tactic:
simp only [llcomp_apply', compr₂_apply, flip_apply] at h

Goal state after:
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
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case hk
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
⊢ finrank K V ≤ finrank K V + finrank K V

Tactic:
lia

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
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
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
· rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
    rintro ⟨s, ⟨b⟩⟩
    exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

Goal state after: