mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ (summand a b σ) v + (summand a b (swap i j • σ)) v = 0

Tactic:
induction σ using Quotient.inductionOn'

Goal state after:
case h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
⊢ (summand a b (Quotient.mk'' a✝)) v + (summand a b (swap i j • Quotient.mk'' a✝)) v = 0
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
⊢ (Perm.sign a✝ • MultilinearMap.domDomCongr a✝ ((↑a).domCoprod ↑b)) v +
      (Perm.sign (swap i j * a✝) • MultilinearMap.domDomCongr (swap i j * a✝) ((↑a).domCoprod ↑b)) v =
    0

Tactic:
Perm.sign_mul,

Goal state after:
case h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
a✝ : Perm (ιa ⊕ ιb)
⊢ (Perm.sign a✝ • MultilinearMap.domDomCongr a✝ ((↑a).domCoprod ↑b)) v +
      ((Perm.sign (swap i j) * Perm.sign a✝) • MultilinearMap.domDomCongr (swap i j * a✝) ((↑a).domCoprod ↑b)) v =
    0
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p : P
⊢ (∃ y ∈ s, (1 - r) • (c -ᵥ ↑h.some) +ᵥ y = p) → ∃ y ∈ s, r • (y -ᵥ c) +ᵥ c = p

Tactic:
intro ⟨x, hmem, heq⟩

Goal state after:
case inr.mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : (1 - r) • (c -ᵥ ↑h.some) +ᵥ x = p
⊢ ∃ y ∈ s, r • (y -ᵥ c) +ᵥ c = p
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case inr.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p : P
⊢ (∃ y ∈ s, r • (y -ᵥ c) +ᵥ c = p) → ∃ y ∈ s, (1 - r) • (c -ᵥ ↑h.some) +ᵥ y = p

Tactic:
intro ⟨x, hmem, heq⟩

Goal state after:
case inr.mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : CommRing k
inst✝² : AddCommGroup V
inst✝¹ : AddTorsor V P
inst✝ : Module k V
s : AffineSubspace k P
c : P
r : k
hr : IsUnit r
t : k
ht : r * t = 1
h✝ : (↑s).Nonempty
h : Nonempty ↥s
p x : P
hmem : x ∈ s
heq : r • (x -ᵥ c) +ᵥ c = p
⊢ ∃ y ∈ s, (1 - r) • (c -ᵥ ↑h.some) +ᵥ y = p
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_1.e_f
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m₁ m₂ : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
σ : Perm.ModSumCongr ιa ιb
⊢ (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑(m₁ + m₂)).domCoprod ↑n)) ⋯) x✝ =
    (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m₁).domCoprod ↑n)) ⋯) x✝ +
      (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m₂).domCoprod ↑n)) ⋯) x✝

Tactic:
induction σ using Quotient.inductionOn'

Goal state after:
case refine_1.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m₁ m₂ : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑(m₁ + m₂)).domCoprod ↑n)) ⋯) x✝ =
    ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m₁).domCoprod ↑n)) ⋯) x✝ +
      ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m₂).domCoprod ↑n)) ⋯) x✝
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_2.e_f
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
σ : Perm.ModSumCongr ιa ιb
⊢ (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑(c • m)).domCoprod ↑n)) ⋯) x✝ =
    c • (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n)) ⋯) x✝

Tactic:
induction σ using Quotient.inductionOn'

Goal state after:
case refine_2.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑(c • m)).domCoprod ↑n)) ⋯) x✝ =
    c • ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n)) ⋯) x✝
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_3.e_f
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
σ : Perm.ModSumCongr ιa ιb
⊢ (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑(n₁ + n₂))) ⋯) x✝ =
    (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n₁)) ⋯) x✝ +
      (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n₂)) ⋯) x✝

Tactic:
induction σ using Quotient.inductionOn'

Goal state after:
case refine_3.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑(n₁ + n₂))) ⋯) x✝ =
    ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n₁)) ⋯) x✝ +
      ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n₂)) ⋯) x✝
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: case refine_4.e_f
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
σ : Perm.ModSumCongr ιa ιb
⊢ (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑(c • n))) ⋯) x✝ =
    c • (Quotient.liftOn' σ (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n)) ⋯) x✝

Tactic:
induction σ using Quotient.inductionOn'

Goal state after:
case refine_4.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x✝ : ιa ⊕ ιb → Mᵢ
a✝ : Perm (ιa ⊕ ιb)
⊢ ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑(c • n))) ⋯) x✝ =
    c • ((Quotient.mk'' a✝).liftOn' (fun σ ↦ Perm.sign σ • MultilinearMap.domDomCongr σ ((↑m).domCoprod ↑n)) ⋯) x✝
Module: Mathlib.LinearAlgebra.Alternating.DomCoprod

Goal state before:
pp: ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ alternatization (a.domCoprod b) = (alternatization a).domCoprod (alternatization b)

Tactic:
apply coe_multilinearMap_injective

Goal state after:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x ↦ Mᵢ) N₁
b : MultilinearMap R' (fun x ↦ Mᵢ) N₂
⊢ ↑(alternatization (a.domCoprod b)) = ↑((alternatization a).domCoprod (alternatization b))
Module: Mathlib.LinearAlgebra.Center

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := Classical.ofNonempty
x : V
⊢ ((b.repr x).sum fun a b_1 ↦ f (b_1 • b a)) = (b.repr x).sum fun a b_1 ↦ ⟨(b.coord i) (f (b i)), ⋯⟩ • b_1 • b a

Tactic:
apply sum_congr

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_3
inst✝ : Nontrivial ι
b : Basis ι R V
f : V →ₗ[R] V
hV : Nontrivial V
h_allEq : ∀ (i j : ι), (b.coord i) (f (b i)) = (b.coord j) (f (b j))
hcomm : ∀ (i : ι) (r : R), r • f (b i) = (b.coord i) (f (b i)) • r • b i
i : ι := ⋯
x : V
⊢ ∀ x_1 ∈ (b.repr x).support, f ((b.repr x) x_1 • b x_1) = ⟨(b.coord i) (f (b i)), ⋯⟩ • (b.repr x) x_1 • b x_1
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case «0»
R : Type u_3
V : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid V
inst✝³ : Module R V
inst✝² : Free R V
inst✝¹ : Module.Finite R V
inst✝ : StrongRankCondition R
f : Dual R V
v : V
hfv : f v = 0
h : finrank R V = 0
h1 : 0 ≤ 1
⊢ transvection f v = id

Tactic:
have : Subsingleton V := (finrank_eq_zero_iff_of_free R V).mp h
    simp [Subsingleton.eq_zero v]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: c : ℂ
⊢ toComplex (ofComplex ((starRingEnd ℂ) c)) = (starRingEnd ℂ) (toComplex (ofComplex c))

Tactic:
toComplex_ofComplex,

Goal state after:
c : ℂ
⊢ (starRingEnd ℂ) c = (starRingEnd ℂ) (toComplex (ofComplex c))
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (v Q) m * e0 Q = -(e0 Q * (v Q) m)

Tactic:
exact (neg_e0_mul_v _ m).symm

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ pinGroup Q ∧ star x ∈ even Q

Tactic:
refine ⟨pinGroup.star_mem hx₁, ?_⟩

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ even Q
⊢ star x ∈ even Q
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯
⊢ star x ∈ (evenOdd Q 0).toSubalgebra ⋯ ⋯

Tactic:
simp only [Submodule.mem_toSubalgebra] at hx₂ ⊢

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx₁ : x ∈ pinGroup Q
hx₂ : x ∈ evenOdd Q 0
⊢ star x ∈ evenOdd Q 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ (ι R) m ∈ ⋀[R]^1 M

Tactic:
simpa only [pow_one] using LinearMap.mem_range_self _ m

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m✝ m'✝ : ExteriorAlgebra R M
hm : m✝ ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)
hm' : m'✝ ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)
⊢ m✝ + m'✝ ∈ Submodule.span R (Set.range fun x ↦ (ιMulti R x.fst) x.snd)

Tactic:
| add _ _ hm hm' =>

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

Goal state before:
pp: I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ringCon R A = (ringCon' R A).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm

Tactic:
rw [ringCon', ringCon, rel']

Goal state after:
I : Type u
inst✝⁵ : DecidableEq I
i : I
R : Type v
inst✝⁴ : CommSemiring R
A : I → Type w
inst✝³ : (i : I) → Semiring (A i)
inst✝² : (i : I) → Algebra R (A i)
B : Type w'
inst✝¹ : Semiring B
inst✝ : Algebra R B
maps : {i : I} → A i →ₐ[R] B
⊢ ringConGen (rel R A) = (ringConGen (rel R A on ⇑ofDirectSum)).comap (powerAlgebraEquivFreeTensorAlgebra R A).symm
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
x : ⨁ (i : I), A i
⊢ ↑((ι R) x) = (ι' R A) x

Tactic:
aesop (add simp [ι', mkAlgHom])

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Fintype ι
inst✝ : Module R M
N : Submodule R M
bM : Basis ι R M
bN : Basis (Fin n) R ↥N
f : Fin n ↪ ι
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
N' : Submodule R (ι → R) := Submodule.map (↑bM.equivFun) N
hN' : N' = Submodule.map (↑bM.equivFun) N
bN' : Basis (Fin n) R ↥N' := bN.map (bM.equivFun.submoduleMap N)
snf' : ∀ (i : Fin n), ↑(bN' i) = Pi.single (f i) (a i)
hNN' : N.toAddSubgroup.index = N'.toAddSubgroup.index
g : ι → R
h : ∃ c, g = ∑ x, c x • Pi.single (f x) (a x)
⊢ ∀ (i : ι), (if h : ∃ j, f j = i then a h.choose else 0) ∣ g i

Tactic:
rcases h with ⟨c, rfl⟩
      intro i
      simp only [Finset.sum_apply, Pi.smul_apply, Pi.single_apply]
      split_ifs with h
      · convert! dvd_mul_left (a h.choose) (c h.choose)
        calc ∑ x : Fin n, _ = c h.choose * if i = f h.choose then a h.choose else 0 := by
              refine Finset.sum_eq_single h.choose ?_ (by simp)
              rintro j - hj
              have hinj := f.injective.ne hj
              rw [h.choose_spec] at hinj
              simp [hinj.symm]
          _ = c h.choose * a h.choose := by simp [h.choose_spec]
      · convert! dvd_refl (0 : R)
        convert! Finset.sum_const_zero with j
        rw [not_exists] at h
        specialize h j
        rw [eq_comm] at h
        simp [h]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ Aᵀ.IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
constructor <;> apply IsTotallyUnimodular.transpose

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case pos
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    (-1) ^ (↑i + ↑x) * ↑s * (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

pp: m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1,
      (-1) ^ (↑i + ↑x_1) * Pi.single (g x) (↑s) (g x_1) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
y : Fin (k + 1)
hxy : y ≠ x
⊢ (-1) ^ (↑i + ↑y) * Pi.single (g x) (↑s) (g y) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove y.succAbove).det =
    0

Tactic:
· rw [hAB]
            change _ ∈ MonoidHom.mrange SignType.castHom.toMonoidHom
            refine mul_mem (mul_mem ?_ (Set.mem_range_self s)) ?_
            · apply pow_mem
              exact ⟨-1, by simp⟩
            · exact ih _ _
                (hf.comp Fin.succAbove_right_injective)
                (hg.comp Fin.succAbove_right_injective)

Goal state after:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
s : SignType
x : Fin (k + 1)
hj' : B j = Pi.single (g x) ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x_1,
      (-1) ^ (↑i + ↑x_1) * Pi.single (g x) (↑s) (g x_1) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x_1.succAbove).det
y : Fin (k + 1)
hxy : y ≠ x
⊢ (-1) ^ (↑i + ↑y) * Pi.single (g x) (↑s) (g y) *
      (((A.fromRows B).submatrix f g).submatrix i.succAbove y.succAbove).det =
    0
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
inst✝¹ : Fintype m
inst✝ : DecidableEq m
a : ℕ
⊢ (↑a).num = ↑a

Tactic:
by
  simpa [← diagonal_natCast] using num_map_natCast (a : Matrix m m ℕ)

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ Commute (star A) A

Tactic:
rw [commute_iff_eq, star_eq_conjTranspose, hA.conjTranspose_mul, hA.mul_conjTranspose]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : (f * f).ofConv = f.ofConv
⊢ IsSelfAdjoint f

Tactic:
← Matrix.ext_iff,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : ∀ (i : m) (j : n), (f * f).ofConv i j = f.ofConv i j
⊢ IsSelfAdjoint f
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
κ : ι → Type u_4
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : Finite ι
b : (i : ι) → Basis (κ i) R (M i)
p : (i : ι) → κ i
this : Fintype ι
⊢ (piTensorProduct b) p = ⨂ₜ[R] (i : ι), (b i) (p i)

Tactic:
classical
  refine (Basis.piTensorProduct b).ext_elem (fun q ↦ ?_)
  simp [Finsupp.single_apply, Fintype.prod_ite_zero, ← funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f

Tactic:
· convert! Dependent.mk _ _ h
    · simp only [mk_rep, Function.comp_apply]
    · exact fun i => rep_nonzero (f i)

Goal state after: