mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (c.ι.app i ≫ hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)))

Tactic:
rw [hc.fac]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s).ι.app i))
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
⊢ h.cone ≅ c

Tactic:
by
    refine Cone.ext (asIso (c.π.app i₀)).symm (fun j ↦ ?_)
    let i := IsCofiltered.min i₀ j
    let α : i ⟶ i₀ := IsCofiltered.minToLeft _ _
    let β : i ⟶ j := IsCofiltered.minToRight _ _
    dsimp
    rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s) ≫ c.π.app i))

Tactic:
rw [hc.fac]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ Continuous ⇑(ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app i))
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j

Tactic:
let α : i₀ ⟶ i := IsFiltered.leftToMax _ _

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j

Tactic:
let α : i₀ ⟶ i := IsFiltered.leftToMax _ _

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ↑t ≠ 0

Tactic:
exact Invertible.ne_zero (t : R)

Goal state after:
Module: Mathlib.Algebra.CharP.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x - 0 ∈ I ↔ ↑x = 0

Tactic:
rw [sub_zero]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
inst✝¹ : Algebra L' L
inst✝ : IsScalarTower K L' L
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ restrictScalars K U ↔ x ∈ V

Tactic:
H,

Goal state after:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
inst✝¹ : Algebra L' L
inst✝ : IsScalarTower K L' L
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ restrictScalars K V ↔ x ∈ V
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ x = y

Tactic:
by rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero]

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
H : s.destruct = none
⊢ motive s

Tactic:
rw [destruct_eq_none H]
    apply nil

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

Goal state before:
pp: α : 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'
s s' : Seq α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ ↑s'.tail = (↑s').tail

Tactic:
cases s' using Subtype.recOn; rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ f a = b) ((map f s).get n)

Tactic:
by rw [get_map, h]

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

Goal state before:
pp: α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ zip f s₁ s₂ = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
← Stream'.eta (zip f s₁ s₂)

Goal state after:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ s₁ ⋈ s₂ = s₁.head :: s₂.head :: t

Tactic:
unfold interleave

Goal state after:
α : Type u
s₁ s₂ : Stream' α
t : Stream' α := s₁.tail ⋈ s₂.tail
⊢ (corecOn (s₁, s₂)
      (fun x ↦
        match x with
        | (s₁, snd) => s₁.head)
      fun x ↦
      match x with
      | (s₁, s₂) => (s₂, s₁.tail)) =
    s₁.head :: s₂.head :: t
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' ↦ (a', s.tail)) (↑s 0) = some (a, s.tail)

Tactic:
rw [← e]

Goal state after:
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ instFunctorOption.1 (fun a' ↦ (a', s.tail)) (some a) = some (a, s.tail)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
a✝ : Option.map f none = none
⊢ Option.map f (s (n + 1)) = none

Tactic:
rw [al e]
        assumption

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

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
h : n ≤ x.length
⊢ drop n (x ++ₛ a) = List.drop n x ++ₛ a

Tactic:
by
  obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le h
  ext k; rcases lt_or_ge k m with _ | hk
  · rw [get_drop, get_append_left, get_append_left, List.getElem_drop]; simpa [hm]
  · obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hk
    have hm' : m = (x.drop n).length := by simp [hm]
    simp_rw [get_drop, ← Nat.add_assoc, ← hm, get_append_right, hm', get_append_right]

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

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h✝ : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
revert s₁

Goal state after:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = ss → a ∈ s₁ ∨ a ∈ s₂
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✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)
i : ι
this : Nonempty ι
x✝¹ x✝ : G i
eq :
  (⇑(ringEquiv G f').toEquiv ∘ ⇑(of G (fun i j h ↦ ⇑(f' i j h)) i)) x✝¹ =
    (⇑(ringEquiv G f').toEquiv ∘ ⇑(of G (fun i j h ↦ ⇑(f' i j h)) i)) x✝
⊢ (fun x ↦ ⟦⟨i, x⟩⟧) x✝¹ = (fun x ↦ ⟦⟨i, x⟩⟧) x✝

Tactic:
simpa only [← ringEquiv_of]

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

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

Tactic:
let ppA := ppconts.a

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
x✝ : Option (IntFractPair ℚ)
stream_q_nth_eq : IntFractPair.stream q n = x✝
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
cases stream_q_nth_eq : IntFractPair.stream q n with

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

Goal state before:
pp: 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
this : g.squashGCF n = g
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
simp only [this, convs_stable_of_terminated n.le_succ terminatedAt_n]

Goal state after:
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.a = Q.a

Tactic:
rw [← coeff_eq_a, h, coeff_eq_a]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
J : Type u_4
inst✝ : Fintype J
i : J ≃ I
⊢ CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e

Tactic:
by
  simp only [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.equiv, Function.comp_apply,
    Fintype.sum_equiv i _ e (fun _ ↦ rfl)]

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : (i : ι) → AddCommMonoid (β i)
c : AddCon M
h : (i : ι) → β i →+ M
f : Π₀ (i : ι), β i
⊢ ↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i ↦ c.mk'.comp (h i)) f

Tactic:
by
  classical
  simp_rw [← AddCon.coe_mk', DFinsupp.sumAddHom_apply, map_dfinsuppSum]
  rfl

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
inst✝ : Nonempty n
I J : Ideal R
eq : matrix n I = matrix n J
⊢ I = J

Tactic:
by
    ext x
    have : (∀ _ _, x ∈ I) ↔ (∀ _ _, x ∈ J) := congr((Matrix.of fun _ _ => x) ∈ $eq)
    simpa only [forall_const] using this

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
hij : i ≠ j
⊢ 1 * (1 - e i) + e i * (1 - e j) = 1

Tactic:
simp [mul_sub, he.ortho hij]

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

Goal state before:
pp: 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
⊢ ⇑c.ofMatrix = Relation.Map (⇑c) (fun x ↦ x i j) fun x ↦ x i j

Tactic:
by
  ext x y
  constructor
  · intro h
    refine ⟨_,_, h i j, ?_⟩
    simp
  · rintro ⟨X, Y, h, rfl, rfl⟩ i' j'
    simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

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

Goal state before:
pp: case e'_2
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
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ ⨆ l, ((f - μ • 1) ^ l).ker = ⨆ x, ⨆ l, ⨆ (_ : ↑l ≤ WithTop.coeOrderHom.toOrderHom x), ((f - μ • 1) ^ l).ker

Tactic:
iSup_prod',

Goal state after:
case e'_2
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
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ ⨆ l, ((f - μ • 1) ^ l).ker = ⨆ x, ⨆ (_ : ↑x.2 ≤ WithTop.coeOrderHom.toOrderHom x.1), ((f - μ • 1) ^ x.2).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✝¹ : Free R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace R M

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective

Goal state after:
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
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h : Function.Surjective ⇑↑e
⊢ trace R (Dual R M) ∘ₗ Dual.transpose = trace 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
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  (dualTensorHomEquiv R M M).prodCongr (dualTensorHomEquiv R N N)
⊢ trace R (M × N) ∘ₗ prodMapLinear R M N M N R = id.coprod id ∘ₗ (trace R M).prodMap (trace R N)

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective

Goal state after:
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
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N) :=
  (dualTensorHomEquiv R M M).prodCongr (dualTensorHomEquiv R N N)
h : Function.Surjective ⇑↑e
⊢ trace R (M × N) ∘ₗ prodMapLinear R M N M N R = id.coprod id ∘ₗ (trace R M).prodMap (trace R N)
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
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R N
inst✝² : Module.Finite R N
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R P) (g ∘ₗ f ∘ₗ h) = (trace R N) (f ∘ₗ h ∘ₗ g)

Tactic:
rw [trace_comp_comm', comp_assoc]

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
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ∃ k, ((LinearMap.restrict g hg - μ₁ • 1) ^ k) x = 0
⊢ ∃ k, ((LinearMap.restrict g hg - μ₂ • 1) ^ k) ((LinearMap.restrict f hf) x) = 0

Tactic:
← LinearMap.restrict_smul_one _,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
f g : End R M
hf : MapsTo ⇑f ↑p ↑p
hg : MapsTo ⇑g ↑p ↑p
μ₁ μ₂ : R
h : MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)
x : ↥p
hx : ∃ k, ((LinearMap.restrict g hg - LinearMap.restrict (μ₁ • 1) ⋯) ^ k) x = 0
⊢ ∃ k, ((LinearMap.restrict g hg - LinearMap.restrict (μ₂ • 1) ⋯) ^ k) ((LinearMap.restrict f hf) x) = 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
μ t : R
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ ((t • f).genEigenspace (t * μ)) k

Tactic:
by
  intro m hm
  simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢
  peel hm with l hlk hl
  rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ DivisionRing α

Tactic:
let nnratCast := e.nnratCast

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : DivisionRing β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
⊢ DivisionRing α
Module: Mathlib.Algebra.Field.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
⊢ Field α

Tactic:
let nnratCast := e.nnratCast

Goal state after:
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : Field β
add_group_with_one : AddGroupWithOne α := e.addGroupWithOne
neg : Neg α := e.Neg
inv : Inv α := e.Inv
div : Div α := e.div
mul : Mul α := e.mul
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
nnratCast : NNRatCast α := e.nnratCast
⊢ Field α
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case cons.cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1) (if hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2 then tl2 else hd1 :: hd2 :: tl2)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2
⊢ Red (hd1 :: tl1) tl2

case neg
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
⊢ (if x = y ∧ b = !c then tail else (x, b) :: (y, c) :: tail) = L2 ++ (x', b') :: (x', !b') :: L3 → p

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : x = y ∧ b = !c
⊢ tail = L2 ++ (x', b') :: (x', !b') :: L3 → p

case neg
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L2 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
⊢ (x, b) :: (y, c) :: tail = L2 ++ (x', b') :: (x', !b') :: L3 → p
Module: Mathlib.GroupTheory.FreeGroup.Reduce

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

Tactic:
apply Red.reduce_left

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red w (invRev (reduce (invRev w)))
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.toWord = invRev x.toWord

Tactic:
rcases x with ⟨L⟩

Goal state after:
case mk
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ (Quot.mk Red.Step L)⁻¹.toWord = invRev (toWord (Quot.mk Red.Step L))
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ toFreeMonoid { head := x, tail := xs } = ofList (x :: xs)

Tactic:
suffices ∀ x : FreeMonoid α, (xs.map FreeMonoid.of).foldl (· * ·) x = x * ofList xs by
    simpa [← List.foldl_map, lift_mk_eq_foldl, toFreeMonoid, lift] using this (FreeMonoid.of x)
  induction xs with grind [ofList_nil, ofList_cons]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
x✝ : Fin 4 → R
⊢ (fun a ↦ ![a.re, a.imI, a.imJ, a.imK]) ((fun a ↦ { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }) x✝) = x✝

Tactic:
ext ⟨_, _ | _ | _ | _ | _ | ⟨⟩⟩ <;> rfl

Goal state after: