mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a + b).num * (↑b.den * ↑a.den) = ↑((a + b).num * ↑a.den * ↑b.den)

pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑((a + b).num * ↑a.den * ↑b.den) = (↑a.num * ↑b.den + ↑b.num * ↑a.den) * ↑(a + b).den

Tactic:
· simp_rw [Int.cast_mul, Int.cast_natCast]
        ring

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑((a + b).num * ↑a.den * ↑b.den) = (↑a.num * ↑b.den + ↑b.num * ↑a.den) * ↑(a + b).den
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • a✝¹ - z • a✝ ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - (a✝ + ↑k • (p / ↑z)) ∈ AddSubgroup.zmultiples p

Tactic:
← smul_sub,

Goal state after:
case h.h
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
z : ℤ
hz : z ≠ 0
a✝¹ a✝ : R
⊢ z • (a✝¹ - a✝) ∈ AddSubgroup.zmultiples p ↔ ∃ k, a✝¹ - (a✝ + ↑k • (p / ↑z)) ∈ AddSubgroup.zmultiples p
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ (y :: t).get 0 = y

Tactic:
get_zero_cons

Goal state after:
α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ y = y
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s

Tactic:
· right
    rw [get_succ, tail_cons] at h
    exact ⟨n', h⟩

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

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

Tactic:
rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]

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

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 : Seq β
⊢ ∀ ⦃s₂ : Seq β⦄,
    (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1 s₂ → BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s₂.destruct

Tactic:
s2

Goal state after:
α : Type u
β : Type v
s : Seq α
f g : Seq α → Seq β
H : ∀ (s : Seq α), BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct
s1 s2 : Seq β
⊢ (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1 s2 → BisimO (fun s1 s2 ↦ ∃ s, s1 = f s ∧ s2 = g s) s1.destruct s2.destruct
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑(cons b s') (k + 1)
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')

Tactic:
rw [h_eq] at e

Goal state after:
case succ.cons
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') k.succ = ↑s' k
⊢ C (cons b s')
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ m ≤ n, ¬s.get? m = none

Tactic:
intro hn _ _ k hkn hk
    exact hn <| le_stable s hkn hk

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

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partNums.get? n = none ↔ g.s.get? n = none

Tactic:
cases s_nth_eq : g.s.get? n

Goal state after:
case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partNums.get? n = none ↔ none = none

case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partNums.get? n = none ↔ some val✝ = none
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partDens.get? n = none ↔ g.s.get? n = none

Tactic:
cases s_nth_eq : g.s.get? n

Goal state after:
case none
α : Type u_1
g : GenContFract α
n : ℕ
s_nth_eq : g.s.get? n = none
⊢ g.partDens.get? n = none ↔ none = none

case some
α : Type u_1
g : GenContFract α
n : ℕ
val✝ : Pair α
s_nth_eq : g.s.get? n = some val✝
⊢ g.partDens.get? n = none ↔ some val✝ = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 : Seq α
⊢ ∀ ⦃s₂ : Seq α⦄,
    (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1 s₂ →
      BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1.destruct
        s₂.destruct

Tactic:
s2

Goal state after:
α : Type u
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
⊢ (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1 s2 →
    BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)) s1.destruct
      s2.destruct
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
h : fract ↑a = 0
⊢ ↑a = ↑⌊↑a⌋ + 1 / ↑0

Tactic:
cast_zero,

Goal state after:
case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
n : ℕ
inst✝ : IsStrictOrderedRing K
a : ℤ
h : fract ↑a = 0
⊢ ↑a = ↑⌊↑a⌋ + 1 / 0
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
f : α → α
s : Seq α
n m : ℕ
h_if : m = n
⊢ Option.map f (s.get? n) = Option.map f (s.get? m)

Tactic:
simp [h_if]

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

Goal state before:
pp: case succ.cons
α : Type u
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → motive tl
m : ℕ
x✝ : α
s✝ : Seq α
ih : motive (cons x✝ s✝)
⊢ motive (cons x✝ s✝).tail

Tactic:
· exact step _ _ ih

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

Goal state before:
pp: case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = (s.set n x).get? m
h_nm : n ≠ m
⊢ p y

Tactic:
rw [get?_set_of_ne _ _ h_nm.symm] at hy

Goal state after:
case inr
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
m : ℕ
hy : some y = s.get? m
h_nm : n ≠ m
⊢ p y
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
⊢ (Ring.DirectLimit.of G f i) x * (Ring.DirectLimit.of G f i) x⁻¹ = 1

Tactic:
by
      rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]

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

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
⊢ v = (of v).convs (n + 1 - 1)

Tactic:
change v = g.convs n

Goal state after:
case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
g : GenContFract K := of v
⊢ v = g.convs n
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

Tactic:
cases g_s_head_eq : g.s.get? 0

Goal state after:
case zero.none
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
g_s_head_eq : g.s.get? 0 = none
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

case zero.some
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
val✝ : Pair K
g_s_head_eq : g.s.get? 0 = some val✝
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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

Tactic:
have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this✝ : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : g.s.get? m = some gp_m
this : 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b
ot : g'.s.get? m = some { a := gp_m.a, b := gp_m.b + gp_succ_m.a / gp_succ_m.b }
⊢ 0 < gp'.a ∧ 0 < gp'.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
g : GenContFract K := of v
not_terminated : ¬g.partDens.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
obtain ⟨b, nth_partDen_eq⟩ : ∃ b, g.partDens.get? n = some b :=
      Option.ne_none_iff_exists'.mp not_terminated

Goal state after:
case 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
not_terminated : ¬g.partDens.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
⊢ (of v).dens n ≤ (of v).dens (n + 1)
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
x✝ x y : A ⊗[R] M
hx : (basisAux A b) (a • x) = a • (basisAux A b) x
hy : (basisAux A b) (a • y) = a • (basisAux A b) y
⊢ (basisAux A b) (a • (x + y)) = a • (basisAux A b) (x + y)

Tactic:
simp [hx, hy]

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
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ ∃ e'_1, IsIdempotentElem e'_1 ∧ f e'_1 = f e' ∧ e'_1 * e₂ = 0 ∧ e₂ * e'_1 = 0

Tactic:
refine ⟨(1 - e₂) * e', ?_, ?_, ?_, ?_⟩

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

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 - e₂) * e') = f e'

case refine_3
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 - e₂) * e' * e₂ = 0

case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0
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:
by
  induction n with
  | zero => refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩
  | succ n IH =>
    obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _)
    have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i
    obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ :=
      exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _
      h₁.isIdempotentElem_sum
      (by simp [Finset.mul_sum, h₂', he.mul_eq, eq_comm])
      (by simp [Finset.sum_mul, h₂', he.mul_eq])
    refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩
    obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
⊢ ∃ a,
    (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) a =
      (Ideal.quotientInfToPiQuotient fun i ↦ Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x)

Tactic:
exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩

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

Goal state before:
pp: case inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')

Tactic:
obtain hj | rfl := ne_or_eq j j'

Goal state after:
case inr.inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
hj : j ≠ j'
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')

case inr.inr
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
⊢ c (Matrix.single i j x i j) (Matrix.single i j y i j)
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
x : M
⊢ x ∈ ((f - μ • 1) ^ 0).ker ↔ x = 0

Tactic:
pow_zero,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ LinearMap.ker 1 ↔ x = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Tactic:
· rintro ⟨x, rfl⟩ i hi
    have : k = i + (k - i) := by lia
    rw [this, pow_add]
    exact ⟨_, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ r * e = r

Tactic:
← hc.comm

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ e * r = r
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
⊢ (∃ x ∈ I, e ∣ x - r) → (1 - e) * r ∈ I

Tactic:
intro ⟨s, hs, t, hrst⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
s : R
hs : s ∈ I
t : R
hrst : s - r = e * t
⊢ (1 - e) * r ∈ I
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: 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)
s : Finset M
b : Basis (↥s) R M
⊢ ((toMatrix b b) (f * g)).trace = ((toMatrix b b) (g * f)).trace

Tactic:
LinearMap.toMatrix_mul

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)
s : Finset M
b : Basis (↥s) R M
⊢ ((toMatrix b b) f * (toMatrix b b) g).trace = ((toMatrix b b) g * (toMatrix b b) f).trace
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
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ↑x ∈ g.maxGenEigenspace μ₁
⊢ f ↑x ∈ g.maxGenEigenspace μ₂

Tactic:
exact h hx

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

Goal state before:
pp: 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
⊢ ((f - (algebraMap K (End K V)) μ) ^ finrank K V * (f - (algebraMap K (End K V)) μ) ^ finrank K V).ker =
    (f.genEigenspace μ) ↑(finrank K V + finrank K V)

Tactic:
simp_rw [← pow_add, genEigenspace_nat]

Goal state after:
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
⊢ LinearMap.ker ((f - (algebraMap K (End K V)) μ) ^ (finrank K V + finrank K V)) =
    ((f - μ • 1) ^ (finrank K V + finrank K V)).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • f - t • μ • 1) ^ l) m = 0

Tactic:
← smul_sub,

Goal state after:
case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ ((t • (f - μ • 1)) ^ l) m = 0
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)
  swap
  · rw [LinearMap.trace, dif_neg H]
    exact IsNilpotent.zero
  obtain ⟨s, ⟨b⟩⟩ := H
  classical
  rw [trace_eq_matrix_trace R b]
  apply Matrix.isNilpotent_trace_of_isNilpotent
  simpa

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ 1 * a = a

Tactic:
← mul_inv_cancel a,

Goal state after:
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * a⁻¹ * a = a
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red L (reduce L)

Tactic:
induction L with
  | nil => constructor
  | cons hd1 tl1 ih =>
    dsimp
    revert ih
    generalize htl : reduce tl1 = TL
    intro ih
    cases TL with
    | nil => exact Red.cons_cons ih
    | cons hd2 tl2 =>
      dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ 0 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g

Tactic:
pow_zero,

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * 1 + r
hr : map (algebraMap R K) r = 0
hm : m = 0
⊢ IsUnit g
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
⊢ f.coeff n ∈ 𝓟

Tactic:
rcases ne_iff_lt_or_gt.1 hn with h₁ | h₂
  · exact hf.mem h₁
  · rw [coeff_eq_zero_of_natDegree_lt h₂]
    exact Ideal.zero_mem _

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = univ * s

Tactic:
by
  rw [coe_closure, union_eq_right]
  exact fun x hx => ⟨1, mem_univ 1, x, hx, by simp⟩

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

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
⊢ ↑(n ^ 0) = ↑n ^ 0

Tactic:
pow_zero,

Goal state after:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
⊢ ↑1 = ↑n ^ 0
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑s⁻¹ = #↑s

Tactic:
rw [← image_inv_eq_inv, Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn]

Goal state after: