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

Goal state before:
pp: case nil.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
⊢ R nil nil → BisimO R nil.destruct nil.destruct → nil.head = nil.head ∧ R nil.tail nil.tail

Tactic:
intro r _

Goal state after:
case nil.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head ∧ R nil.tail nil.tail
Module: Mathlib.Data.Stream.Init

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

Tactic:
rw [tail_iterate]

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

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

Tactic:
rw [iterate]

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = f (iterate f a n)
⊢ f (iterate f (f a) n) = f (f (iterate f a n))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a ∈ s

Tactic:
rw [p h]

Goal state after:
α : Type u
s : Computation α
a : α
p : s ~> a
a' : α
h : a' ∈ s
⊢ a' ∈ s
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this : s.Terminates
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
have := results_of_terminates' _ (of_think_mem h.mem)

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this✝ : s.Terminates
this : s.Results a s.length
⊢ ∃ m, s.Results a m ∧ n = m + 1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ s.think = (pure a).thinkN (n + 1)

Tactic:
IH (results_think_iff.1 h)

Goal state after:
case succ.think
α : Type u
a : α
n : ℕ
IH : ∀ {s : Computation α}, s.Results a n → s = (pure a).thinkN n
s : Computation α
h : s.think.Results a (n + 1)
⊢ ((pure a).thinkN n).think = (pure a).thinkN (n + 1)
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
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1)) p₁ +
      Polynomial.map ((of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2)) p₂ =
    Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ + Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂

Tactic:
congr 2

Goal state after:
case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₁ i h1) = of G (fun i j h ↦ ⇑(f' i j h)) i₁

case e_a.e_f
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
q : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
q₁ q₂ : (DirectLimit G fun i j h ↦ ⇑(f' i j h))[X]
x✝¹ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₁
x✝ : ∃ i p, Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i) p = q₂
i₁ : ι
p₁ : (G i₁)[X]
ih₁ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₁) p₁ = q₁
i₂ : ι
p₂ : (G i₂)[X]
ih₂ : Polynomial.map (of G (fun i j h ↦ ⇑(f' i j h)) i₂) p₂ = q₂
i : ι
h1 : i₁ ≤ i
h2 : i₂ ≤ i
⊢ (of G (fun i j h ↦ ⇑(f' i j h)) i).comp (f' i₂ i h2) = of G (fun i j h ↦ ⇑(f' i j h)) i₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s : Stream' α
⊢ ↑([] ++ₛ s) = (↑[]).append ↑s

Tactic:
simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

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

Goal state before:
pp: case cons
α : Type u
s : Stream' α
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(tail✝ ++ₛ s) = (↑tail✝).append ↑s
⊢ ↑(head✝ :: tail✝ ++ₛ s) = (↑(head✝ :: tail✝)).append ↑s

Tactic:
simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
s_nth_eq : (of v).s.get? n = some { a := 1, b := ↑ifp.b }
⊢ ∃ ifp_1, IntFractPair.stream v (n + 1) = some ifp_1 ∧ ↑ifp_1.b = { a := 1, b := ↑ifp.b }.b

Tactic:
simp_all only [Option.some.injEq, exists_eq_left']

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

Goal state before:
pp: α : Type u
β : Type v
init : β
f : β → α → β
⊢ nil.fold init f = cons init nil

Tactic:
unfold fold

Goal state after:
α : Type u
β : Type v
init : β
f : β → α → β
⊢ (have f := fun x ↦
      match x with
      | (acc, x) =>
        match x.destruct with
        | none => none
        | some (x, s) => some (f acc x, f acc x, s);
    cons init (corec f (init, nil))) =
    cons init nil
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ (cons x s).fold init f = cons init (s.fold (f init x) f)

Tactic:
unfold fold

Goal state after:
α : Type u
β : Type v
init : β
f : β → α → β
x : α
s : Seq α
⊢ (have f := fun x ↦
      match x with
      | (acc, x) =>
        match x.destruct with
        | none => none
        | some (x, s) => some (f acc x, f acc x, s);
    cons init (corec f (init, cons x s))) =
    cons init
      (have f_1 := fun x ↦
        match x with
        | (acc, x) =>
          match x.destruct with
          | none => none
          | some (x, s) => some (f acc x, f acc x, s);
      cons (f init x) (corec f_1 (f init x, s)))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
S : Seq (Seq1 α)
⊢ ∃ s S_1,
    Seq.map f S.join = s.append (Seq.map f S_1.join) ∧ (Seq.map (map f) S).join = s.append (Seq.map (map f) S_1).join

Tactic:
· simpa using ⟨nil, S, by simp, by simp⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq1 α
f : α → Seq1 β
g : β → Seq1 γ
⊢ (s.bind f).bind g = s.bind fun x ↦ (f x).bind g

Tactic:
by
  obtain ⟨a, s⟩ := s
  simp only [bind, map_pair, map_join]
  rw [← map_comp]
  simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]
  rw [map_comp _ join]
  generalize Seq.map (map g ∘ f) s = SS
  rcases map g (f a) with ⟨⟨a, s⟩, S⟩
  induction s using recOn with | nil => ?_ | cons x s_1 => ?_ <;>
  induction S using recOn with | nil => simp | cons x_1 s_2 => ?_
  · obtain ⟨x, t⟩ := x_1
    cases t <;> simp
  · obtain ⟨y, t⟩ := x_1; simp

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : Cubic R
⊢ P.toPoly = 0 ↔ P = 0

Tactic:
rw [← zero, toPoly_injective]

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

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

Tactic:
by
  induction n generalizing g with
  | zero => simp
  | succ n IH =>
    let g' := squashGCF g n
    -- first replace the rhs with the squashed computation
    suffices g.convs (n + 1) = g'.convs' n by
      rwa [succ_nth_conv'_eq_squashGCF_nth_conv']
    rcases Decidable.em (TerminatedAt g n) with terminatedAt_n | not_terminatedAt_n
    · have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminatedAt_n
      rw [convs_stable_of_terminated n.le_succ terminatedAt_n, g'_eq_g, IH _]
      intro _ _ m_lt_n s_mth_eq
      exact s_pos (Nat.lt_succ_of_lt m_lt_n) s_mth_eq
    · suffices g.convs (n + 1) = g'.convs n by
        -- invoke the IH for the squashed gcf
        rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            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
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
      -- now the result follows from the fact that the convergents coincide at the squashed position
      -- as established in `succ_nth_conv_eq_squashGCF_nth_conv`.
      have : ∀ ⦃b⦄, g.partDens.get? n = some b → b ≠ 0 := by
        intro _ nth_partDen_eq
        grind [exists_s_b_of_partDen nth_partDen_eq]
      exact succ_nth_conv_eq_squashGCF_nth_conv @this

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

Goal state before:
pp: case succ.inl.succ
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 + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
        simp only [g, this, IH]

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
x : A
y : M
⊢ (basisAux A b) (a • x ⊗ₜ[R] y) = a • (basisAux A b) (x ⊗ₜ[R] y)

Tactic:
simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc]

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

Goal state before:
pp: case right
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ ↑ifp_succ_n.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b

Tactic:
have : (ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹ :=
      IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv stream_nth_eq succ_nth_stream_eq

Goal state after:
case right
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹
⊢ ↑ifp_succ_n.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
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
inst✝ : Nonempty n
I J : Ideal R
eq : matrix n I = matrix n J
x : R
⊢ x ∈ I ↔ x ∈ J

Tactic:
have : (∀ _ _, x ∈ I) ↔ (∀ _ _, x ∈ J) := congr((Matrix.of fun _ _ => x) ∈ $eq)

Goal state after:
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matrix n I = matrix n J
x : R
this : (∀ (x_1 x_2 : n), x ∈ I) ↔ ∀ (x_1 x_2 : n), x ∈ J
⊢ x ∈ I ↔ x ∈ J
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag ⟨i, k⟩ = 0 ⟨i, k⟩

Tactic:
simp only [Matrix.diag_apply, Pi.zero_apply, toMatrix_apply, IsInternal.collectedBasis_coe]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
κ : ι → Type u_4
inst✝¹ : (i : ι) → Fintype (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
s : Finset ι
h : IsInternal fun i ↦ N ↑i
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i)
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : ∀ i ∉ s, N i = ⊥
i : ↥s
k : κ ↑i
⊢ ((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0
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
⊢ ∑ i_1, e i * ↑(r i_1) * e i = ↑(r i)

Tactic:
rw [Finset.sum_eq_single i _ (by simp at ·)]

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 : I
⊢ e i * ↑(r i) * e i = ↑(r i)

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
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
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : IsNilpotent (μ₁ - μ₂)
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False

Tactic:
isNilpotent_iff_eq_zero,

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
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : μ₁ - μ₂ = 0
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ (trace R M) 1 = ↑(finrank R M)

Tactic:
rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(Fintype.card (Free.ChooseBasisIndex R M))
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
s : Finset N
b : Basis (↥s) R N
⊢ False

Tactic:
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:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: 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 : f.IsPrimitive
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
⊢ ¬(algebraMap R K) g.leadingCoeff = 0

Tactic:
obtain ⟨h, rfl⟩ := hg_div

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
h : R[X]
hf_lC : (algebraMap R K) (g * h).leadingCoeff ≠ 0
hf_prim : (g * h).IsPrimitive
hfmodP : map (algebraMap R K) (g * h) = C ((algebraMap R K) (g * h).leadingCoeff) * map (algebraMap R K) q ^ p
⊢ ¬(algebraMap R K) g.leadingCoeff = 0
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]

Tactic:
by
  apply (equivProd c₁ c₂ c₃).injective.addCommGroup <;> intros <;> rfl

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R ≃+* S
h : IsIntegrallyClosed R
⊢ IsIntegrallyClosed S

Tactic:
by
  let _ : Algebra S R := f.symm.toRingHom.toAlgebra
  let f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv fun _ ↦ rfl
  let g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f
  refine (isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)
  rcases (isIntegrallyClosed_iff _).mp h ((isIntegral_algEquiv g).mpr hx).tower_top with ⟨z, hz⟩
  exact ⟨f.symm z, (IsFractionRing.algEquivOfAlgEquiv_algebraMap f.symm z).symm.trans <|
    (AlgEquiv.symm_apply_eq g).mpr hz⟩

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : SMul M α
inst✝⁶ : SMul M β
inst✝⁵ : SMul N α
inst✝⁴ : SMul N β
a✝ : M
b : α
c : β
x✝ : α ⊕ β
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : SMul Mᵐᵒᵖ β
inst✝¹ : IsCentralScalar M α
inst✝ : IsCentralScalar M β
a : M
x : α ⊕ β
⊢ MulOpposite.op a • x = a • x

Tactic:
by
    cases x
    exacts [congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]

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

Goal state before:
pp: case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    map (algebraMap R (FractionRing (R ⧸ P))) (C f.leadingCoeff) *
      map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree

Tactic:
← Polynomial.map_pow,

Goal state after:
case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    map (algebraMap R (FractionRing (R ⧸ P))) (C f.leadingCoeff) *
      map (algebraMap R (FractionRing (R ⧸ P))) (X ^ f.natDegree)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ 0 ∈ P

Tactic:
exact P.zero_mem

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

Goal state before:
pp: case inl
M : Type u_1
inst✝ : Semigroup M
s : Set M
x y : M
hy : y ∈ s
⊢ x • y ∈ s ∪ univ * s

Tactic:
exact .inr <| mul_mem_mul (mem_univ _) hy

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
← natCard_inv t

Goal state after:
G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : M ≤ N
⊢ N ≤ M

Tactic:
rw [SetLike.le_def] at h ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
M : Submonoid G
hMp : M.IsMulPointed
hMs : M.IsMulSpanning
N : Submonoid G
hN : N.IsMulPointed
h : ∀ ⦃x : G⦄, x ∈ M → x ∈ N
⊢ ∀ ⦃x : G⦄, x ∈ N → x ∈ M