mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.LinearAlgebra

Goal state before:
pp: A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
e : D ≅ of (↑B ⊗[↑A] ↑C) := h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit ↑A ↑B ↑C)
⊢ Nontrivial ↑D

Tactic:
let e' : D ≃ B ⊗[A] C := e.commRingCatIsoToRingEquiv.toEquiv

Goal state after:
A B C D : CommRingCat
hA : IsField ↑A
f : A ⟶ B
g : A ⟶ C
inl : B ⟶ D
inr : C ⟶ D
inst✝¹ : Nontrivial ↑B
inst✝ : Nontrivial ↑C
h : IsPushout f g inl inr
this : Field ↑A := hA.toField
algInst✝¹ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝ : Algebra ↑A ↑C := (Hom.hom g).toAlgebra
e : D ≅ of (↑B ⊗[↑A] ↑C) := h.isColimit.coconePointUniqueUpToIso (pushoutCoconeIsColimit ↑A ↑B ↑C)
e' : ↑D ≃ ↑B ⊗[↑A] ↑C := e.commRingCatIsoToRingEquiv.toEquiv
⊢ Nontrivial ↑D
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Over Q X) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro U V k

Goal state after:
case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Over Q X
k : U ⟶ V
⊢ (map Q ⋯).map k = eqToHom ⋯ ≫ (map Q hf ⋙ map Q hg).map k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
⊢ autoParam
    (∀ (X_1 Y_1 : P.Under Q Z) (f_1 : X_1 ⟶ Y_1),
      (map Q ⋯).map f_1 = eqToHom ⋯ ≫ (map Q hg ⋙ map Q hf).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro U V k

Goal state after:
case h_map
T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
X Y Z : T
inst✝ : P.IsStableUnderComposition
f : X ⟶ Y
hf : P f
g : Y ⟶ Z
hg : P g
U V : P.Under Q Z
k : U ⟶ V
⊢ (map Q ⋯).map k = eqToHom ⋯ ≫ (map Q hg ⋙ map Q hf).map k ≫ eqToHom ⋯
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
p : ℕ
inst✝¹ : CharP R p
n : ℕ
inst✝ : Invertible ↑n
h : n.Coprime p
⊢ ⅟↑n = ↑(n.gcdA p)

Tactic:
let : Invertible (n : R) := invertibleOfCoprime h
  convert! (rfl : ⅟(n : R) = _)

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

Goal state before:
pp: case refl
α : Type u
m n : ℕ
f : Stream' (Option α)
al : f.IsSeq
⊢ get? ⟨f, al⟩ m = none → get? ⟨f, al⟩ m = none

Tactic:
| refl =>

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

Goal state before:
pp: α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ s'.tail.val = s'.val.tail

Tactic:
cases s'; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none

Tactic:
by_cases hi : i = n

Goal state after:
case pos
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : i = n
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none

case neg
α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
i : ℕ
hi : ¬i = n
⊢ Function.update (↑s) n (Option.map f (s.get? n)) i = none ↔ s.get? i = none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.odd
n : ℕ
h : (fun b ↦ a = b) (s.odd.get n)
⊢ (fun b ↦ s.odd.get n = b) (s.get (2 * n + 1))

Tactic:
get_odd

Goal state after:
α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.odd
n : ℕ
h : (fun b ↦ a = b) (s.odd.get n)
⊢ (fun b ↦ s.get (2 * n + 1) = b) (s.get (2 * n + 1))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refl
α : Type u
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ⟨f, al⟩.val m = some a → ⟨f, al⟩.val m = some a

Tactic:
| refl =>

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)

Tactic:
rw [get_succ]

Goal state after:
case succ
n✝ : ℕ
⊢ nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: case refl
K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s n = convs'Aux s n

Tactic:
| refl =>

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

Goal state before:
pp: α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a1 : a ∈ c₁
⊢ a ∈ c₂

Tactic:
let ⟨b, b2, ab⟩ := h1 a1

Goal state after:
α : Type u
c₁ c₂ : Computation α
x✝ : LiftRel (fun x1 x2 ↦ x1 = x2) c₁ c₂
a : α
h1 : ∀ {a : α}, a ∈ c₁ → ∃ b, b ∈ c₂ ∧ (fun x1 x2 ↦ x1 = x2) a b
h2 : ∀ {b : α}, b ∈ c₂ → ∃ a, a ∈ c₁ ∧ (fun x1 x2 ↦ x1 = x2) a b
a1 : a ∈ c₁
b : α
b2 : b ∈ c₂
ab : (fun x1 x2 ↦ x1 = x2) a b
⊢ a ∈ c₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
f : α → α
s : Seq α
n m : ℕ
⊢ (s.update n f).get? m = if m = n then Option.map f (s.get? m) else s.get? m

Tactic:
simp [update, Function.update]

Goal state after:
α : Type u
f : α → α
s : Seq α
n m : ℕ
⊢ (if m = n then Option.map f (s.get? n) else s.get? m) = if m = n then Option.map f (s.get? m) else s.get? m
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case refl
n : ℕ
⊢ 5 ≤ fib 5

Tactic:
| refl =>

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

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

Tactic:
map_comp _ join

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a : α
s : Seq α
⊢ (join (map g (f a), Seq.map (map g ∘ f) s)).join = join ((map g (f a)).join, Seq.map join (Seq.map (map g ∘ f) s))
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n

Tactic:
convs'_succ,

Goal state after:
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
⊢ ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs' n = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n
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:
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.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
⊢ |v - (of v).convs n| < ε

Tactic:
rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n

Goal state after:
case inl
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
terminatedAt_n : g.TerminatedAt n
⊢ |v - (of v).convs n| < ε

case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n

Goal state after:
case inl
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs 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.b = Q.b

Tactic:
← coeff_eq_b,

Goal state after:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.toPoly.coeff 2 = Q.b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
by
        rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n

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
m : M
⊢ (basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

Tactic:
by
  ext
  simp [basisAux, ← Algebra.commutes, Algebra.smul_def]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
| (baseChange A ((b'.linearMap b) ij)) ((basis A b') k)

Tactic:
simp only [basis_apply, baseChange_tmul]

Goal state after:
R : Type u_1
M : Type uM
ι : Type uι
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Fintype ι
ι' : Type u_3
N : Type u_4
inst✝⁵ : Fintype ι'
inst✝⁴ : DecidableEq ι'
inst✝³ : AddCommMonoid N
inst✝² : Module R N
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
| 1 ⊗ₜ[R] ((b'.linearMap b) ij) (b' k)
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)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
w : V
⊢ T (v w • x) = T (v w • y)

Tactic:
_root_.map_smul,

Goal state after:
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)
surj : Function.Surjective ⇑T
x y : V
hxy : T x = T y
w : V
⊢ v w • T x = v w • T y
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case zero
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 : Fin 0 → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin 0), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩

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
inst✝ : IsNoetherian R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) ⊤ = (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
by
  have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <|
    (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom
  convert! this using 1
  simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe,
    Function.comp_def]
  rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]
  congr 1
  aesop

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

Goal state before:
pp: case a
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ asIdeal (matrix n I).jacobson ≥ asIdeal (matrix n I.jacobson)

Tactic:
simp [asIdeal_jacobson, asIdeal_matrix, Ideal.matrix_jacobson_le]

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
      f.independent_maxGenEigenspace hf

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
⊢ (trace R M) (g ∘ₗ f) = 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
f : End R M
μ : R
n : ℕ∞
⊢ (f.genEigenspace μ) n ∈ f.invtSubmodule

Tactic:
by
  intro x hx
  simp only [Submodule.mem_comap, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
  obtain ⟨k, hk, hx⟩ := hx
  refine ⟨k, hk, ?_⟩
  induction k generalizing x
  case zero => simp_all
  case succ k ih =>
    rw [pow_succ, mul_apply] at hx ⊢
    simpa using ih (le_trans (by simp) hk) hx

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

Goal state before:
pp: case insert
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 : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ μ₁ ∉ insert μ₂ s → Disjoint ((f.genEigenspace μ₁) k) ((insert μ₂ s).sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
| insert μ₂ s _ ih =>

Goal state after:
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k) * -1

Tactic:
zpow_mul,

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = ((-1) ^ 2) ^ k * -1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case refl
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce L₁ = reduce L₁

Tactic:
| refl =>

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₂ : Function.Surjective ⇑i₂
hi₃ : Function.Injective ⇑i₃
hg₀ : Function.Injective ⇑g₁
⊢ Function.Surjective ⇑i₁

Tactic:
refine surjective_of_surjective_of_surjective_of_injective (0 : Unit →ₗ[R] M₁) f₁ f₂
    (0 : Unit →ₗ[R] N₁) g₁ g₂ 0 i₁ i₂ i₃ (by simp) hc₁ hc₂ hf₁ (fun y ↦ ?_) hg₁
    (fun | .unit => ⟨0, rfl⟩) hi₂ hi₃
  simp only [Set.mem_range, zero_apply, exists_const]
  exact ⟨fun h ↦ (hg₀ ((map_zero _).trans h.symm)), fun h ↦ h ▸ (map_zero _)⟩

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ↑r * x = x * ↑r

Tactic:
by
  ext <;> simp [mul_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
⊢ ↑(s • t • u) = ↑(t • s • u)

Tactic:
by simp_rw [coe_smul, smul_comm]

Goal state after:
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:
simp_rw [mem_sInf] at hxy ⊢

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
f : Set (Submonoid M)
hf : ∀ s ∈ f, s.MulSaturated
x✝¹ x✝ : M
hxy : ∀ p ∈ f, x✝¹ * x✝ ∈ p
⊢ (∀ p ∈ f, x✝¹ ∈ p) ∧ ∀ p ∈ f, x✝ ∈ p
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case h
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ ↑a✝ * ↑b✝ = ↑(a✝ * b✝)

Tactic:
Units.val_mul

Goal state after:
case h
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
y : A
hy : f y = ↑a✝
y' : A
hy' : f y' = ↑b✝
⊢ ↑a✝ * ↑b✝ = ↑a✝ * ↑b✝
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
let φ := ε.counitIso.symm.app X'

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_inj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')

Tactic:
Prod.mk_inj

Goal state after:
case i_inj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i' ∧ j = j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑⟨↑k + (i + 1), ⋯⟩ = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) (Fin.succAbove 0 k))

Tactic:
δ₀Iter_apply ..

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑⟨↑k + (i + 1), ⋯⟩ = ↑⟨↑(Fin.succAbove 0 k) + i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
⊢ X.σ₀Iter 0 ⋯ = 𝟙 (X _⦋n⦌)

Tactic:
by
  simp [σ₀Iter]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case a
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) y

Tactic:
exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ' ≫ δ i = δ i

Tactic:
eq_id_of_mono θ',

Goal state after:
case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ 𝟙 ⦋n⦌ ≫ δ i = δ i