mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
⊢ Function.Bijective ⇑ibc.toDualBaseChangeAux

Tactic:
let b := Free.chooseBasis R V

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
V : Type u_2
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
W : Type u_3
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module R W
A : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A W
inst✝² : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst✝¹ : Free R V
inst✝ : Module.Finite R V
b : Basis (Free.ChooseBasisIndex R V) R V := Free.chooseBasis R V
⊢ Function.Bijective ⇑ibc.toDualBaseChangeAux
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
    (affineCombination k univ s.points) w ∈ ⇑(homothety (s.points i) x) '' (s.faceOpposite i).closedInterior

Tactic:
Set.mem_image

Goal state after:
case pos
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Field k
inst✝⁵ : LinearOrder k
inst✝⁴ : IsOrderedRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
x : k
hx : x ∈ Set.Icc 0 1
hxpos : 0 < x
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hp : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
⊢ (∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1) ∧ w i = 1 - x ↔
    ∃ x_1 ∈ (s.faceOpposite i).closedInterior, (homothety (s.points i) x) x_1 = (affineCombination k univ s.points) w
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
x : V
⊢ ↑e x = x + f x • v

Tactic:
he,

Goal state after:
case h
R : Type u_1
V : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
e✝ e : V ≃ₗ[R] V
f : Dual R V
v : V
he : ↑e = LinearMap.transvection f v
x : V
⊢ (LinearMap.transvection f v) x = x + f x • v
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case hle
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
this : finrank K (V ⧸ ker f) = 1
x : V
⊢ x ∈ (↑e).fixedSubmodule → x ∈ ker f

Tactic:
mem_ker,

Goal state after:
case hle
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
this : finrank K (V ⧸ ker f) = 1
x : V
⊢ x ∈ (↑e).fixedSubmodule → f x = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case h.left
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
hfv : f v = 0
x : V
hx : x ∈ ker f
⊢ f x = 0

Tactic:
LinearMap.mem_ker

Goal state after:
case h.left
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
hfv : f v = 0
x : V
hx : f x = 0
⊢ f x = 0
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
⊢ e w - w ∈ (↑e).fixedSubmodule.mkQ.ker

Tactic:
LinearMap.mem_ker

Goal state after:
case neg
V : Type u_2
inst✝³ : AddCommGroup V
K : Type u_3
inst✝² : DivisionRing K
inst✝¹ : Module K V
inst✝ : Module.Finite K V
e : V ≃ₗ[K] V
x✝ : e ∈ dilatransvections K V ∧ e.fixedReduce = 1
he : finrank K (V ⧸ (↑e).fixedSubmodule) ≤ 1
he' : e.fixedReduce = 1
he_one : ¬e = 1
hefixed_ne_top : (↑e).fixedSubmodule ≠ ⊤
w : V
hw : w ∉ (↑e).fixedSubmodule
f : Dual K V
hfw : f w ≠ 0
hf : map f (↑e).fixedSubmodule = ⊥
hf' : (↑e).fixedSubmodule = ker f
eq_top : (↑e).fixedSubmodule ⊔ K ∙ w = ⊤
v : V := (f w)⁻¹ • (e w - w)
⊢ (↑e).fixedSubmodule.mkQ (e w - w) = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: c : CliffordAlgebra Q
⊢ toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))

Tactic:
simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]

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

Goal state before:
pp: ⊢ (algebraMap ℝ (CliffordAlgebra Q)) (Q 1) = -1

Tactic:
Q_apply,

Goal state after:
⊢ (algebraMap ℝ (CliffordAlgebra Q)) (-(1 * 1)) = -1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) (1, 0)) = c₁ • 1 + 0 • (ι (Q c₁ c₂)) (1, 0)

Tactic:
Q_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((1, 0).1 * (1, 0).1) + c₂ * ((1, 0).2 * (1, 0).2)) =
    c₁ • 1 + 0 • (ι (Q c₁ c₂)) (1, 0)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) ((Q c₁ c₂) (0, 1)) = c₂ • 1

Tactic:
Q_apply,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
⊢ (algebraMap R (CliffordAlgebra (Q c₁ c₂))) (c₁ * ((0, 1).1 * (0, 1).1) + c₂ * ((0, 1).2 * (0, 1).2)) = c₂ • 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

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
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ (CliffordAlgebra.ι Q) m₁ * ((CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₃) =
    Q m₂ • ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₃)

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
m₁ m₂ m₃ : M
⊢ (CliffordAlgebra.ι Q) m₁ * ((CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₂ * (CliffordAlgebra.ι Q) m₃) =
    (algebraMap R (CliffordAlgebra Q)) (Q m₂) * ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₃)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Even

Goal state before:
pp: case fst
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ (f.bilin m) m * a = Q m • a

Tactic:
Algebra.smul_def,

Goal state after:
case fst
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
f : EvenHom Q A
m : M
a : A
g : M →ₗ[R] A
hg : g ∈ S f
⊢ (f.bilin m) m * a = (algebraMap R A) (Q m) * a
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Inversion

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
inst✝ : Invertible (Q m)
⊢ ⅟(Q m) • (algebraMap R (CliffordAlgebra Q)) (Q m) = 1

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
m : M
inst✝ : Invertible (Q m)
⊢ (algebraMap R (CliffordAlgebra Q)) ⅟(Q m) * (algebraMap R (CliffordAlgebra Q)) (Q m) = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        ((ι Q) m₂.1 * (ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2 * (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      (Q' Q) m₂ • ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2)

Tactic:
Algebra.smul_def,

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
f : M × R →ₗ[R] M × R →ₗ[R] CliffordAlgebra Q :=
  ((Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ
        (ι Q ∘ₗ LinearMap.fst R M R + Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)).compl₂
    (ι Q ∘ₗ LinearMap.fst R M R - Algebra.linearMap R (CliffordAlgebra Q) ∘ₗ LinearMap.snd R M R)
f_apply :
  ∀ (x y : M × R),
    (f x) y =
      ((ι Q) x.1 + (algebraMap R (CliffordAlgebra Q)) x.2) * ((ι Q) y.1 - (algebraMap R (CliffordAlgebra Q)) y.2)
hc : ∀ (r : R) (x : CliffordAlgebra Q), Commute ((algebraMap R (CliffordAlgebra Q)) r) x
hm :
  ∀ (m : M × R),
    (ι Q) m.1 * (ι Q) m.1 - (algebraMap R (CliffordAlgebra Q)) m.2 * (algebraMap R (CliffordAlgebra Q)) m.2 =
      (algebraMap R (CliffordAlgebra Q)) ((Q' Q) m)
m₁ m₂ m₃ : M × R
⊢ ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
        ((ι Q) m₂.1 * (ι Q) m₂.1 - (algebraMap R (CliffordAlgebra Q)) m₂.2 * (algebraMap R (CliffordAlgebra Q)) m₂.2) *
      ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2) =
    ((ι Q) m₁.1 + (algebraMap R (CliffordAlgebra Q)) m₁.2) *
      ((algebraMap R (CliffordAlgebra Q)) ((Q' Q) m₂) * ((ι Q) m₃.1 - (algebraMap R (CliffordAlgebra Q)) m₃.2))
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: case e_a
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (2 • (j₁ * i₂) + (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))

Tactic:
two_nsmul,

Goal state after:
case e_a
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (j₁ * i₂ + j₁ * i₂ + (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))
Module: Mathlib.LinearAlgebra.Dimension.Torsion.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommGroup M
⊢ AddSubgroup.toIntSubmodule (AddCommGroup.torsion M) = torsion ℤ M

Tactic:
by
    rw [← Submodule.torsion_int, Submodule.toAddSubgroup_toIntSubmodule]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝¹ : ℕ
x✝ : Fin i✝¹ → M
i✝ : ℕ
⊢ ((((toDirectSum.comp ofDirectSum).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i ↦ ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝ =
    ((((AlgHom.id R (⨁ (n : ℕ), ⨂[R]^n M)).toLinearMap ∘ₗ DirectSum.lof R ℕ (fun i ↦ ⨂[R]^i M) i✝¹).compMultilinearMap
          (PiTensorProduct.tprod R))
        x✝)
      i✝

Tactic:
simp [DirectSum.lof_eq_of, -tprod_apply, toDirectSum_tensorPower_tprod]

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

Goal state before:
pp: case e'_3
ι : 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)
e : (ι → R) ≃+ M := ↑bM.equivFun.symm
he : e = ↑bM.equivFun.symm
e' : (ι → R) →+ M := ↑e
he' : Function.Surjective ⇑e'
e_2✝ : Pi.addCommGroup.toAddGroup = Pi.addGroup
⊢ N'.toAddSubgroup = AddSubgroup.map (↑e.symm) N.toAddSubgroup

Tactic:
he,

Goal state after:
case e'_3
ι : 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)
e : (ι → R) ≃+ M := ↑bM.equivFun.symm
he : e = ↑bM.equivFun.symm
e' : (ι → R) →+ M := ↑e
he' : Function.Surjective ⇑e'
e_2✝ : Pi.addCommGroup.toAddGroup = Pi.addGroup
⊢ N'.toAddSubgroup = AddSubgroup.map (↑(↑bM.equivFun.symm).symm) N.toAddSubgroup
Module: Mathlib.LinearAlgebra.FreeModule.Int

Goal state before:

Tactic:
∑ x : Fin n, _ =
            if i = f hj.choose then (h (f hj.choose)).choose * a hj.choose else 0 := by
              convert! Finset.sum_eq_single (M := R) hj.choose ?_ ?_
              · simp
              · rintro j - h
                have hinj := f.injective.ne h
                rw [hj.choose_spec] at hinj
                simp [hinj.symm]
              · simp
          _ = g i := by
              simp only [hj.choose_spec, ↓reduceIte]
              rw [mul_comm]
              conv_rhs =>
                rw [← hj.choose_spec, (h (f hj.choose)).choose_spec]
              simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte, Classical.choose_eq]
              congr!
              · exact hj.choose_spec.symm
              · simp [hj]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition

Goal state before:
pp: m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = (cert.L * A.submatrix (⇑cert.σ) id).rank

Tactic:
cert.L.rank_mul_eq_right_of_isLowerTriangular _ cert.L_lowerTriangular cert.L_diag_ne_zero

Goal state after:
m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = (A.submatrix (⇑cert.σ) id).rank
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
inst✝ : DecidableEq n
A : Matrix m n R
h : Nonempty n
i j : n
⊢ 1 i j = Pi.single i (↑1) j

Tactic:
by simp [one_apply, Pi.single_apply, eq_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Goal state before:
pp: case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
this : Unique { s // ⊤ = ⊥ }
⊢ card { s // ker 0 = ⊥ } = ∏ i, (q ^ n - q ^ ↑i)

Tactic:
ker_zero,

Goal state after:
case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
this : Unique { s // ⊤ = ⊥ }
⊢ card { s // ⊤ = ⊥ } = ∏ i, (q ^ n - q ^ ↑i)
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.transpose.det ≠ 0

Tactic:
exact det_ne_zero_of_sum_row_lt_diag (by simp_rw [Matrix.transpose_apply]; exact h)

Goal state after:
Module: Mathlib.RingTheory.PiTensorProduct

Goal state before:
pp: ι : Type u_1
R' : Type u_2
R : Type u_3
A : ι → Type u_4
inst✝⁶ : CommSemiring R'
inst✝⁵ : CommSemiring R
inst✝⁴ : (i : ι) → Semiring (A i)
inst✝³ : Algebra R' R
inst✝² : (i : ι) → Algebra R (A i)
inst✝¹ : (i : ι) → Algebra R' (A i)
inst✝ : ∀ (i : ι), IsScalarTower R' R (A i)
r : R'
x : ⨂[R] (i : ι), A i
⊢ { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := fun x ↦ x • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
by
    simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
    change mul _ _ = mul _ _
    rw [LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower, LinearMap.smul_apply]
    change r • (1 * x) = r • (x * 1)
    rw [mul_one, one_mul]

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
⊢ A ⊆ ↑B → span A ≤ B

Tactic:
intro h x hx
      induction hx with
      | of => apply h; assumption
      | mem_add => apply B.mem_add; assumption'

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝³ : Field F
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i₁ i₂ : ι
hij : i₁ ≠ i₂
g : Matrix.SpecialLinearGroup ι F := SpecialLinearGroup.transvection hij 1
⊢ Nontrivial (ProjectiveSpecialLinearGroup ι F)

Tactic:
refine ⟨⟨(QuotientGroup.mk g : Matrix.ProjectiveSpecialLinearGroup ι F),
    1, fun h ↦ one_ne_zero (α := F) ?_⟩⟩

Goal state after:
ι : Type u_1
F : Type u_2
inst✝³ : Field F
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : Nontrivial ι
i₁ i₂ : ι
hij : i₁ ≠ i₂
g : Matrix.SpecialLinearGroup ι F := SpecialLinearGroup.transvection hij 1
h : ↑g = 1
⊢ 1 = 0
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ a • D.rep = D.rep + (b.coord ⟨D.rep, hD_mem⟩) D.rep • (↑a - 1) • b ⟨D.rep, hD_mem⟩

Tactic:
Module.Basis.coord_apply

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ a • D.rep = D.rep + (b.repr D.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • b ⟨D.rep, hD_mem⟩
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
hQ : L.mapQ L (↑(toLin' A)) hcomap = LinearMap.id
hdet : 1 = c * LinearMap.det LinearMap.id * LinearMap.det LinearMap.id
⊢ A • v = v

Tactic:
LinearMap.det_id,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
hQ : L.mapQ L (↑(toLin' A)) hcomap = LinearMap.id
hdet : 1 = c * 1 * LinearMap.det LinearMap.id
⊢ A • v = v
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
hQ : L.mapQ L (↑(toLin' A)) hcomap = LinearMap.id
hdet : 1 = c * 1 * LinearMap.det LinearMap.id
⊢ A • v = v

Tactic:
LinearMap.det_id,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A : SpecialLinearGroup ι F
L : Submodule F (ι → F) := F ∙ v
hA : A ∈ lineStab L
c : F
hcv : ↑(toLin' A) v = c • v
hcomap : F ∙ v ≤ Submodule.comap (↑(toLin' A)) (F ∙ v)
hres : (↑(toLin' A)).restrict hcomap = c • LinearMap.id
hQ : L.mapQ L (↑(toLin' A)) hcomap = LinearMap.id
hdet : 1 = c * 1 * 1
⊢ A • v = v