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

Goal state before:
pp: case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
⊢ ExpChar R p

Tactic:
have := f.charP H p; exact .prime hp

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
⊢ s.Results a n

Tactic:
let ⟨n', r, e⟩ := of_results_think h
    injection e with h'; rwa [h']

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

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b

Tactic:
rw [al e]; exact h

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

Goal state before:
pp: α : 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

Tactic:
cases h : destruct s with
    | none =>
      simp [destruct_eq_none h]
    | some a =>
      match a with
      | (x, r) =>
        rw [destruct_eq_cons h]
        match n with
        | 0 => simp
        | n + 1 => simp [List.getElem?_cons_succ, getElem?_take]

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

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
⊢ x ∈ take n s

Tactic:
obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn

Goal state after:
case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈ take n s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case pure
α : Type u
β : Type v
f : α → β
s✝ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) ((pure s).bind (pure ∘ f)).destruct
    (map f (pure s)).destruct

Tactic:
| pure s =>

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

Goal state before:
pp: case pure
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g)
    (((pure s).bind f).bind g).destruct ((pure s).bind fun x ↦ (f x).bind g).destruct

Tactic:
| pure s =>

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

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)

Tactic:
by
  rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]

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

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

Tactic:
| pure s =>

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

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

Tactic:
| pure s =>

Goal state after:
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
inst✝ : IsStrictOrderedRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ (of ↑a).s.get? (n + 1) = (of (fract ↑a)⁻¹).s.get? n

Tactic:
rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int,
      Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Monoid α
inst✝⁴ : Monoid β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a b : α
c d : β
hab : a ∣ b
hcd : c ∣ d
⊢ a • c ∣ b • d

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hab, hcd
  exact ⟨x • y, mul_smul_mul_comm a x c y⟩

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

Goal state before:
pp: n : ℕ
⊢ n.fastFib = fib n

Tactic:
rw [fastFib, fastFibAux_eq]

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

Goal state before:
pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
· -- 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: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ conts, (of v).conts n = Pair.map Rat.cast conts

Tactic:
by
  rw [nth_cont_eq_succ_nth_contAux]; exact exists_gcf_pair_rat_eq_of_nth_contsAux v <| n + 1

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
v : K
n : ℕ
⊢ ∃ q, (of v).convs n = ↑q

Tactic:
rcases exists_rat_eq_nth_num v n with ⟨Aₙ, nth_num_eq⟩

Goal state after:
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ₙ
⊢ ∃ q, (of v).convs n = ↑q
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
m : ℕ
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1

Tactic:
clear m

Goal state after:
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : DivisionRing K
⊢ ∀ (n_1 : ℕ),
    (∀ m < n_1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) →
      n_1 ≤ n → g.contsAux n_1 = (g.squashGCF n).contsAux n_1
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_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)

Tactic:
suffices ifp_succ_n.fr.num + 1 ≤ (IntFractPair.of q).fr.num - n by
      rw [Int.natCast_succ, sub_add_eq_sub_sub]
      solve_by_elim [le_sub_right_of_add_le]

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 + 1 ≤ (IntFractPair.of q).fr.num - ↑n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.d = Q.d

Tactic:
by rw [← coeff_eq_d, h, coeff_eq_d]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
⊢ ∃! e'_1, IsIdempotentElem e'_1 ∧ f e'_1 = f e'

Tactic:
exact ⟨e', ⟨he₂, rfl⟩, fun x ⟨hx, hx'⟩ ↦
    eq_of_isNilpotent_sub_of_isIdempotentElem hx he₂
      (h _ (by rw [RingHom.mem_ker, map_sub, hx', sub_self]))⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
⊢ ∀ c ∈ Finset.univ, ∑ j, single c j (M c j) ∈ (matrix n I).jacobson

Tactic:
intro i _

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∑ j, single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
⊢ ↑(equivMatrix.symm I) = {x | ∃ N ∈ I, N i j = x}

Tactic:
ext r

Goal state after:
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
⊢ r ∈ ↑(equivMatrix.symm I) ↔ r ∈ {x | ∃ N ∈ I, N i j = x}
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ I ≤ J → matrix n I ≤ matrix n J

Tactic:
intro IJ M MI i j
      exact IJ <| MI i j

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
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
calc f.genEigenspace μ k
      ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
    _ ≤ f.genEigenspace μ (finrank K V) := by
      rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
      exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

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
⊢ f.eigenspace μ = (f - μ • 1).ker

Tactic:
by
  rw [eigenspace, genEigenspace_one]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
⊢ e i * ↑(r j) * e i = 0

Tactic:
have ⟨r', eq⟩ := (r j).2

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
r' : R
eq : (fun x ↦ e j * x * e j) r' = ↑(r j)
⊢ e i * ↑(r j) * e i = 0
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
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) }
x y : A
⊢ (↑fe).1 x * (↑fe).2 * ((↑fe).1 y * (↑fe).2) = 0

Tactic:
(fe.prop.2 _).mul_mul_mul_comm,

Goal state after:
R : Type u_1
A✝ : Type u_2
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) }
x y : A
⊢ (↑fe).1 x * (↑fe).1 y * ((↑fe).2 * (↑fe).2) = 0
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
⊢ ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
intro μ₁ s

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
s : Finset R
⊢ μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case refine_1
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ Commute f (g ^ l)

Tactic:
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

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

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) (y + z) ∈ ↑(s.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
rw [SetLike.mem_coe, map_add, hl, zero_add]

Goal state after:
case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
μ : R
x✝ : μ ∈ s
u : M
hu : u ∈ ↑((f.genEigenspace μ) k)
⊢ Commute f (g ^ l)

Tactic:
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ ((LinearMap.restrict f hfp - μ • 1) ^ l).ker = Submodule.comap p.subtype ((f - μ • 1) ^ l).ker

Tactic:
← LinearMap.restrict_smul_one μ,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ ((LinearMap.restrict f hfp - LinearMap.restrict (μ • 1) ⋯) ^ l).ker = Submodule.comap p.subtype ((f - μ • 1) ^ l).ker
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✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
have hμ : g = algebraMap R _ μ + n := eq_add_of_sub_eq' rfl

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
rw [Finset.mem_antidiagonal] at hij

Goal state after:
case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
Module: Mathlib.Algebra.Field.Action.ConjAct

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
⊢ ∀ (a : ConjAct K) (x y : K), a • (x + y) = a • x + a • y

Tactic:
by simp [smul_def, mul_add, add_mul]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
x : N₂
a : M₂
hy : i₃ (f₂ a) = g₂ x
o : M₁
hb : g₁ (i₁ o) = x / i₂ a
⊢ g₁ (i₁ o) = i₂ (f₁ o)

Tactic:
simpa using DFunLike.congr_fun hc₁ o

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
head_eq✝ : (x, b) = a
H : (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3
⊢ reduce L1 = L2 ++ (x', b') :: (x', !b') :: L3

Tactic:
rw [r, H]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case coe
α : Type u_1
a : FreeSemigroup α
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑a) = ↑a

Tactic:
induction a with simp_all

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
⊢ a ∣ b

Tactic:
have hy : IsIntegral R y := by
    refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩
    simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]
    replace hx := congr_arg (algebraMap R K) hx
    rw [map_pow] at hx
    simp [hx, ha]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
⊢ a ∣ b
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t

Tactic:
← coe_subset

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Tactic:
← coe_subset

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ ↑s ⊆ ↑(a • t) ↔ ↑(a⁻¹ • s) ⊆ ↑t
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #ℍ[R,c₁,c₂,c₃] = #R

Tactic:
rw [mk_quaternionAlgebra, pow_four]

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

Goal state before:
pp: case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ (-1) ^ (k + 1) * a * b = (-1) ^ (k + 1) * (a * b)

Tactic:
rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
    simp only [neg_mul, ih]

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

Goal state before:
pp: case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ (φ h - 1) ^ n * (φ (x + h) - φ x) = (φ h - 1) ^ n * (φ h * φ x - 1 * φ x)

Tactic:
← AddChar.map_add_eq_mul,

Goal state after:
case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ (φ h - 1) ^ n * (φ (x + h) - φ x) = (φ h - 1) ^ n * (φ (h + x) - 1 * φ x)
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x✝¹ x✝ : M
hxy : x✝¹ * x✝ ∈ InfSet.sInf f
⊢ x✝¹ ∈ InfSet.sInf f ∧ x✝ ∈ InfSet.sInf f

Tactic:
by
  simp_rw [mem_sInf] at hxy ⊢
  exact ⟨fun s hs ↦ (hf s hs <| hxy s hs).1, fun s hs ↦ (hf s hs <| hxy s hs).2⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
⊢ ∃ y, x✝ * y✝ * y ∈ s

Tactic:
| mul _ _ _ _ ih₁ ih₂ =>

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Center

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
⊢ 0 * ↑↑u = ↑↑u * 0

pp: case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
hr : r ≠ 0
⊢ r * ↑↑u = ↑↑u * r

Tactic:
· rw [mul_zero, zero_mul]

Goal state after:
case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
u : ↥(center G₀ˣ)
r : G₀
hr : r ≠ 0
⊢ r * ↑↑u = ↑↑u * r