mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * 0 + 1) = e₁ - e₂

pp: case succ
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n✝ : ℕ
a✝ : (e₁ - e₂) ^ (2 * n✝ + 1) = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * (n✝ + 1) + 1) = e₁ - e₂

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * 0 + 1) = e₁ - e₂

case succ
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
n✝ : ℕ
a✝ : (e₁ - e₂) ^ (2 * n✝ + 1) = e₁ - e₂
⊢ (e₁ - e₂) ^ (2 * (n✝ + 1) + 1) = e₁ - e₂
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case zero
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ (f ^ 0) v = μ ^ 0 • v

pp: case succ
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
n✝ : ℕ
a✝ : (f ^ n✝) v = μ ^ n✝ • v
⊢ (f ^ (n✝ + 1)) v = μ ^ (n✝ + 1) • v

Tactic:
<;>

Goal state after:
case zero
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ (f ^ 0) v = μ ^ 0 • v

case succ
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
v : M
hv : f.HasUnifEigenvector μ 1 v
n✝ : ℕ
a✝ : (f ^ n✝) v = μ ^ n✝ • v
⊢ (f ^ (n✝ + 1)) v = μ ^ (n✝ + 1) • v
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he.«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ IsIdempotentElem (o ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case he.«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ IsIdempotentElem (o ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case he.«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ IsIdempotentElem (o ((fun i ↦ i) ⟨0, ⋯⟩))

case he.«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ IsIdempotentElem (o ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.LinearAlgebra.Matrix.Ideal

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

Tactic:
· 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.RingTheory.Idempotents

Goal state before:
pp: case he₁.«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) * (1 - o j) = 0

pp: case he₁.«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) * (1 - o j) = 0

Tactic:
<;>

Goal state after:
case he₁.«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) * (1 - o j) = 0

case he₁.«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
j : Fin 2
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) * (1 - o j) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he₁.«0».«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

pp: case he₁.«0».«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

pp: case he₁.«1».«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

pp: case he₁.«1».«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

Tactic:
<;>

Goal state after:
case he₁.«0».«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

case he₁.«0».«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) = 0

case he₁.«1».«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨0, ⋯⟩)) = 0

case he₁.«1».«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) * (1 - o ((fun i ↦ i) ⟨1, ⋯⟩)) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case he₁.«0».«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : True
⊢ (1 - o 0) * (1 - o 1) = 0

pp: case he₁.«1».«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : True
⊢ (1 - o 1) * (1 - o 0) = 0

Tactic:
<;>

Goal state after:
case he₁.«0».«1»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : True
⊢ (1 - o 0) * (1 - o 1) = 0

case he₁.«1».«0»
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
hij : True
⊢ (1 - o 1) * (1 - o 0) = 0
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: case e'_1
ι : 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 ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := ⋯
κ : ι → Type u_3 := ⋯
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := ⋯
x✝ : ι
⊢ x✝ ∈ s ↔ N x✝ ≠ ⊥

pp: case e'_8.h.e'_2
ι : 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 ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := ⋯
κ : ι → Type u_3 := ⋯
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := ⋯
e_1✝ : ↥s = { i // N i ≠ ⊥ }
a✝¹ : ↥s
a'✝ : { i // N i ≠ ⊥ }
a✝ : a✝¹ ≍ a'✝
x✝ : ι
⊢ x✝ ∈ s ↔ N x✝ ≠ ⊥

Tactic:
<;>

Goal state after:
case e'_1
ι : 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 ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := ⋯
κ : ι → Type u_3 := ⋯
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := ⋯
x✝ : ι
⊢ x✝ ∈ s ↔ N x✝ ≠ ⊥

case e'_8.h.e'_2
ι : 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 ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := ⋯
κ : ι → Type u_3 := ⋯
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := ⋯
e_1✝ : ↥s = { i // N i ≠ ⊥ }
a✝¹ : ↥s
a'✝ : { i // N i ≠ ⊥ }
a✝ : a✝¹ ≍ a'✝
x✝ : ι
⊢ x✝ ∈ s ↔ N x✝ ≠ ⊥
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
h : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ) h)

Tactic:
apply isNilpotent_restrict_of_le (q := f.genEigenspace μ (maxUnifEigenspaceIndex f μ))
    _ (isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ))

Goal state after:
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
h : MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
⊢ f.maxGenEigenspace μ ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)
Module: Mathlib.Algebra.DualNumber

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

pp: case h2
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ snd (ε * x) = snd (x * ε)

Tactic:
<;>

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

case h2
R : Type u_1
inst✝ : Semiring R
x : R[ε]
⊢ snd (ε * x) = snd (x * ε)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
⊢ Algebra R R'

Tactic:
letI := f.toAlgebra
    exact Algebra.compHom _ (algebraMap R R[ε])

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (traceAux R b.reindexFinsetRange) f = (traceAux R b) f

Tactic:
traceAux_eq R b b.reindexFinsetRange

Goal state after:
R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (traceAux R b.reindexFinsetRange) f = (traceAux R b.reindexFinsetRange) f
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
A : Matrix ι ι R
b : Basis ι R M
⊢ (trace R M) ((Matrix.toLin b b) A) = A.trace

Tactic:
simp [trace_eq_matrix_trace R b]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case hl
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
x✝¹ : Dual R M
x✝ : M
⊢ ((AlgebraTensorModule.curry
          (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ ↑e) ∘ₗ inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) ∘ₗ ↑e) ∘ₗ inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝

pp: case hr
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
x✝¹ : Dual R N
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ ↑e) ∘ₗ inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) ∘ₗ ↑e) ∘ₗ inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝

Tactic:
<;>

Goal state after:
case hl
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
x✝¹ : Dual R M
x✝ : M
⊢ ((AlgebraTensorModule.curry
          (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ ↑e) ∘ₗ inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) ∘ₗ ↑e) ∘ₗ inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝

case hr
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
x✝¹ : Dual R N
x✝ : N
⊢ ((AlgebraTensorModule.curry
          (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ ↑e) ∘ₗ inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (((id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) ∘ₗ ↑e) ∘ₗ inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)))
        x✝¹)
      x✝
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

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

Tactic:
refine iSup₂_mono fun μ _ ↦ ?_

Goal state after:
case refine_2
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
μ : R
x✝ : μ ∈ s
⊢ Submodule.map (g ^ l) ((f.genEigenspace μ) k) ≤ (f.genEigenspace μ) k
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 μ₂)
⊢ MapsTo ⇑(LinearMap.restrict f hf) ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁)
    ↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂)

Tactic:
intro x hx
  simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
    LinearMap.restrict_sub _, Module.End.pow_restrict _, LinearMap.restrict_apply,
    Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢
  exact h hx

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
h : reduce [] = head✝ :: tail✝ ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
h : reduce [] = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p

case cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
L3 : List (α × Bool)
x✝¹ : α
x✝ : Bool
head✝ : α × Bool
tail✝ : List (α × Bool)
h : reduce [] = head✝ :: tail✝ ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: L3
⊢ p
Module: Mathlib.GroupTheory.FreeGroup.Reduce

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

pp: 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

Tactic:
<;>

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.Algebra.Free

Goal state before:
pp: case intro
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝ f : α →ₙ* β
x : AssocQuotient α
c d e : α
⊢ f (c * d * e) = f (c * (d * e))

pp: case left
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝¹ f✝ : α →ₙ* β
x : AssocQuotient α
c d e f : α
⊢ f✝ (c * (d * e * f)) = f✝ (c * (d * (e * f)))

Tactic:
<;>

Goal state after:
case intro
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝ f : α →ₙ* β
x : AssocQuotient α
c d e : α
⊢ f (c * d * e) = f (c * (d * e))

case left
α : Type u
inst✝¹ : Mul α
β : Type v
inst✝ : Semigroup β
f✝¹ f✝ : α →ₙ* β
x : AssocQuotient α
c d e f : α
⊢ f✝ (c * (d * e * f)) = f✝ (c * (d * (e * f)))
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
hd : α × Bool
tail : List (α × Bool)
r : reduce L1 = hd :: tail
⊢ List.rec [(x, b)] (fun head tail tail_ih ↦ if x = head.1 ∧ b = !head.2 then tail else (x, b) :: head :: tail)
        (hd :: tail) =
      L2 ++ (x', b') :: (x', !b') :: L3 →
    p

Tactic:
obtain ⟨y, c⟩ := hd
      dsimp only
      split_ifs with h <;> intro H
      · rw [H] at r
        exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
      rcases L2 with (_ | ⟨a, L2⟩)
      · injections; subst_vars
        simp at h
      · refine @reduce.not _ L1 L2 L3 x' b' ?_
        rw [List.cons_append] at H
        injection H with _ H
        rw [r, H]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ x * y = mk (x.toWord ++ y.toWord)

Tactic:
← FreeGroup.mul_mk,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ x * y = mk x.toWord * mk y.toWord
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inl
α : Type u
h✝ : IsEmpty α
⊢ #(FreeRing α) = max #α ℵ₀

pp: case inr
α : Type u
h✝ : Nonempty α
⊢ #(FreeRing α) = max #α ℵ₀

Tactic:
<;>

Goal state after:
case inl
α : Type u
h✝ : IsEmpty α
⊢ #(FreeRing α) = max #α ℵ₀

case inr
α : Type u
h✝ : Nonempty α
⊢ #(FreeRing α) = max #α ℵ₀
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inl
α : Type u
h✝ : IsEmpty α
⊢ #(FreeCommRing α) = max #α ℵ₀

pp: case inr
α : Type u
h✝ : Nonempty α
⊢ #(FreeCommRing α) = max #α ℵ₀

Tactic:
<;>

Goal state after:
case inl
α : Type u
h✝ : IsEmpty α
⊢ #(FreeCommRing α) = max #α ℵ₀

case inr
α : Type u
h✝ : Nonempty α
⊢ #(FreeCommRing α) = max #α ℵ₀