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

Goal state before:
pp: case e'_2.e'_4
α : Type u
β : Type v
α' : Type u'
s₁ : Seq α
s₂ : Seq β
f : α → α'
⊢ s₂ = map id s₂

Tactic:
simp

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

Goal state before:
pp: case e'_2.e'_3
α : Type u
β : Type v
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f : β → β'
⊢ s₁ = map id s₁

Tactic:
simp

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
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = Int.fract v + ↑⌊v⌋

Tactic:
rw [Int.fract_add_floor]

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

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g₁ : (i : ι) → G i →+* G' i
g₂ : (i : ι) → G' i →+* G'' i
hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝

Tactic:
simp

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
  | zero => simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]
  | succ =>
    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.Data.Seq.Basic

Goal state before:
pp: case e_s
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ (match (init, cons x s).2.destruct with
    | none => none
    | some (x_1, s_1) => some (f (init, cons x s).1 x_1, f (init, cons x s).1 x_1, s_1)) =
    some (f init x, f init x, s)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
this : motive nil
⊢ ∀ (x : α), nil.head = some x → p x

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u
s : Seq α
p : α → Prop
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl
n : ℕ
hd : α
tl : Seq α
this : motive (cons hd tl)
⊢ ∀ (x : α), (cons hd tl).head = some x → p x

Tactic:
simp [(step hd tl this).left]

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

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 0 ↔ m < 0

Tactic:
simp

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

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
⊢ fib m < fib 1 ↔ m < 1

Tactic:
simp

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

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ n + 2 ∈ Set.Ici 2

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ (fib 0).Coprime (fib (0 + 1))

Tactic:
simp

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

Goal state before:
pp: case zero
m : ℕ
⊢ fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (0 + 1)

Tactic:
simp

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

Goal state before:
pp: case h_hd
α : Type u
R : α → α → Prop
hd : α
⊢ ∀ x ∈ nil, R hd x

Tactic:
simp

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

Goal state before:
pp: case h_tl
α : Type u
R : α → α → Prop
hd : α
⊢ Pairwise R nil

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)

Tactic:
simp

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

Goal state before:
pp: case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
R : α → α → Prop
h : Pairwise R nil
⊢ Pairwise R nil.tail

Tactic:
simp

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

Goal state before:
pp: case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → true = true)

Tactic:
simp

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

Goal state before:
pp: case inl
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)

Tactic:
simp

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

Goal state before:
pp: m n : ℕ
⊢ (fib m).gcd (fib (n + 0 * m)) = (fib m).gcd (fib n)

Tactic:
simp

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

Goal state before:
pp: case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = (fib 0).gcd (fib n✝)

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a : β
⊢ join ((a, nil), nil) = (a, nil)

Tactic:
simp

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

Goal state before:
pp: case cons
α : Type u
β : Type v
a✝ : α
f : α → Seq1 β
a x✝ : β
s✝ : Seq β
⊢ join ((a, Seq.cons x✝ s✝), nil) = (a, Seq.cons x✝ s✝)

Tactic:
simp

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

Goal state before:
pp: case bisim.nil.nil
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    (nil.append (Seq.map f nil.join)).destruct (nil.append (Seq.map (map f) nil).join).destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ Seq.map f S.join = nil.append (Seq.map f S.join)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ (Seq.map (map f) S).join = nil.append (Seq.map (map f) S).join

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ map f (join ((a, s), S)) = (map (map f) ((a, s), S)).join

Tactic:
by cases s <;> simp [map]

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

Goal state before:
pp: case bisim.nil.nil
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (nil.append nil.join.join).destruct (nil.append (Seq.map join nil).join).destruct

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ fib (0 + 1) = ∑ k ∈ Finset.range 0, fib k + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ Seq.cons x (s.append (S.join.append SS.join.join)) = (Seq.cons x (s.append S.join)).append SS.join.join

Tactic:
simp

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

Goal state before:
pp: α : Type u
SS✝ SS : Seq (Seq1 (Seq1 α))
S : Seq (Seq1 α)
x✝ x : α
s : Seq α
⊢ Seq.cons x (s.append (S.join.append (Seq.map join SS).join)) =
    (Seq.cons x (s.append S.join)).append (Seq.map join SS).join

Tactic:
simp

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

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

Tactic:
simp [Finset.range_add_one]

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

Goal state before:
pp: α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ SS.join.join = nil.append SS.join.join

Tactic:
simp

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

Goal state before:
pp: α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ (Seq.map join SS).join = nil.append (Seq.map join SS).join

Tactic:
simp

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

Goal state before:
pp: case nil.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
⊢ (join (((a, nil), nil), SS)).join = join (join ((a, nil), nil), Seq.map join SS)

Tactic:
simp

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

Goal state before:
pp: case cons.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), nil), SS)).join = join (join ((a, Seq.cons x s_1), nil), Seq.map join SS)

Tactic:
simp

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

Goal state before:
pp: case nil.cons.nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x : γ
⊢ (join (((a, nil), Seq.cons (x, nil) s_2), SS)).join = join (join ((a, nil), Seq.cons (x, nil) s_2), Seq.map join SS)

Tactic:
simp

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

Goal state before:
pp: case nil.cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
s_2 : Seq (Seq1 γ)
x x✝ : γ
s✝ : Seq γ
⊢ (join (((a, nil), Seq.cons (x, Seq.cons x✝ s✝) s_2), SS)).join =
    join (join ((a, nil), Seq.cons (x, Seq.cons x✝ s✝) s_2), Seq.map join SS)

Tactic:
simp

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

Goal state before:
pp: case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
s_2 : Seq (Seq1 γ)
y : γ
t : Seq γ
⊢ (join (((a, Seq.cons x s_1), Seq.cons (y, t) s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons (y, t) s_2), Seq.map join SS)

Tactic:
simp

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

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := ⋯
IH : ∀ m < 0, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ { a := 1, b := 0 } = Pair.map Rat.cast { a := 1, b := 0 }

Tactic:
simp

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

Goal state before:
pp: case some.succ
K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
| succ m IH =>

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

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

Tactic:
cases n with
  | zero =>
    cases g_s_head_eq : g.s.get? 0 <;>
      simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]
  | succ =>
    simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
      squashGCF]

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'.map (Option.map (mapFr Rat.cast)) (IntFractPair.stream q) = IntFractPair.stream v

Tactic:
funext n; exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n

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

Goal state before:
pp: case zero
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < 0 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ g.convs 0 = g.convs' 0

Tactic:
simp

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

Goal state before:
pp: case succ.zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 + 1 - 2)
⊢ ↑(fib (0 + 1)) ≤ ((of v).contsAux (0 + 1)).b

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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 }
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

Tactic:
obtain hn | hn := le_or_gt n 3

Goal state after:
case inl
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 : ℕ
hn : n ≤ 3
⊢ (↑((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

case inr
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 : ℕ
hn : 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
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
let g := of v
  rcases Decidable.em <| g.partDens.TerminatedAt n with terminated | not_terminated
  · have : g.TerminatedAt n :=
      terminatedAt_iff_partDen_none.2 (by rwa [Stream'.Seq.TerminatedAt] at terminated)
    have : g.dens (n + 1) = g.dens n :=
      dens_stable_of_terminated n.le_succ this
    rw [this]
  · obtain ⟨b, nth_partDen_eq⟩ : ∃ b, g.partDens.get? n = some b :=
      Option.ne_none_iff_exists'.mp not_terminated
    have : 1 ≤ b := of_one_le_get?_partDen nth_partDen_eq
    calc
      g.dens n ≤ b * g.dens n := by
        simpa using mul_le_mul_of_nonneg_right this zero_le_of_den
      _ ≤ g.dens (n + 1) := le_of_succ_get?_den nth_partDen_eq

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

Goal state before:
pp: case zero
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
stream_nth_eq : IntFractPair.stream v 0 = some ifp
conts : Pair K := g.contsAux (0 + 1)
pred_conts : Pair K := g.contsAux 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)
⊢ 0 = 0 ∨ ¬g.TerminatedAt (0 - 1)

Tactic:
simp

Goal state after:
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 : A ⊗[R] M
⊢ (basisAux A b) (a • 0) = a • (basisAux A b) 0

Tactic:
simp

Goal state after:
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
i : ι
⊢ a • (basis A b) i = a ⊗ₜ[R] b i

Tactic:
simpa using basis_repr_symm_apply b a i

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

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

Tactic:
simp

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

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

Tactic:
by simp [T, this, hd]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.range n
⊢ Commute (1 - x ^ n) x

Tactic:
simp

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 : S
he : e ∈ f.range
he' : IsIdempotentElem e
⊢ e * f 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
l : List ι
f : ι → M
⊢ ↑(List.map f l).prod = (List.map (fun i ↦ ↑(f i)) l).prod

Tactic:
induction l with simp [*]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
⊢ M • N ∈ I.matrix.carrier

Tactic:
by
    intro i j
    rw [smul_eq_mul, mul_apply]
    apply sum_mem
    intro k _
    apply I.mul_mem_left _ (hN k j)

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝ : Matrix n n R
⊢ x✝ ∈ matrix n ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

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
i : n
a✝ : i ∈ Finset.univ
⊢ ∀ c ∈ Finset.univ, single i c (M i c) ∈ (matrix n I).jacobson

Tactic:
intro j

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 : n
⊢ j ∈ Finset.univ → single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case empty
R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
⊢ ∏ i ∈ ∅, (1 - e i) = 1 - ∑ i ∈ ∅, e i

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype n
x✝⁴ x✝³ : Matrix n n R
x✝² : ⊤ x✝⁴ x✝³
x✝¹ x✝ : n
⊢ ⊤ (x✝⁴ x✝¹ x✝) (x✝³ x✝¹ x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
s : Finset I
⊢ (∏ i ∈ ∅, (1 - e i)) * x = x

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents fun x ↦ 1 - e x
⊢ ∀ (x : I), 1 - (1 - e x) = e x

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
x y : R
h : c.ofMatrix x y
⊢ (fun x ↦ x i j) (single i j x) = x ∧ (fun x ↦ x i j) (single i j y) = y

Tactic:
simp

Goal state after:
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
r : R
h : r ∈ ↑(equivMatrix.symm I)
⊢ single i j r i j = r

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Ring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
x✝ : Matrix n n R
⊢ x✝ ∈ asIdeal (matrix n I) ↔ x✝ ∈ Ideal.matrix n (asIdeal I)

Tactic:
simp

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
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i j : I
h : some i ≠ some j
⊢ f (e' i * e' j) = 0

Tactic:
simp [he', he.1.2 (by simpa using h)]

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
n : ℕ∞
k : ℕ
ih : ∀ ⦃x : M⦄, ↑k ≤ n → ((f - μ • 1) ^ k) x = 0 → ((f - μ • 1) ^ k) (f x) = 0
x : M
hk : ↑(k + 1) ≤ n
hx : ((f - μ • 1) ^ k) ((f - μ • 1) x) = 0
⊢ ↑k ≤ ↑(k + 1)

Tactic:
simp

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
x✝ : M
⊢ x✝ ∈ f.maxGenEigenspace μ ↔ x✝ ∈ (f - μ • 1).maxGenEigenspace 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : NonUnitalSemiring R
idem : IsIdempotentElem e
⊢ (fun x ↦ e * x * e) e = e

Tactic:
by simp_rw [idem.eq]

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 : I
⊢ ∀ b ∈ Finset.univ, b ≠ i → e i * ↑(r b) * e i = 0

Tactic:
intro j

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
⊢ j ∈ Finset.univ → j ≠ i → e i * ↑(r j) * e i = 0
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: case h1
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ fst (ε * x) = fst (x * ε)

Tactic:
simp

Goal state after: