mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
v : m → R
h : ∀ (w : m → R), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ M.det * v i = 0

Tactic:
simpa using

Goal state after:
m : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m R
hM : M.det ∈ R⁰
v : m → R
h : ∀ (w : m → R), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ M.det * v i = 0
Module: Mathlib.LinearAlgebra.Matrix.Nondegenerate

Goal state before:
pp: ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, (∑ i, w i • A i x) • v x = 0
hv : w ᵥ* A = 0
w' : ι → R
⊢ w ⬝ᵥ A *ᵥ w' = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst✝⁴ : Fintype ι
inst✝³ : Finite κ
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : ∑ x, (∑ i, w i • A i x) • v x = 0
hv : w ᵥ* A = 0
w' : ι → R
⊢ w ᵥ* A ⬝ᵥ w' = 0
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hf : ↑↑x = 1
g : G
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ⟨f.toHomUnits g, ⋯⟩
⊢ f g = 1 g

Tactic:
simpa using

Goal state after:
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hf : ↑↑x = 1
g : G
n : ℕ
hn : (fun x_1 ↦ x ^ x_1) n = ⟨f.toHomUnits g, ⋯⟩
⊢ f g = 1
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: case calc_1.hx
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := ⋯
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ u ∈ Set.range ⇑f.toHomUnits

Tactic:
simpa using

Goal state after:
case calc_1.hx
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ ∃ y, f.toHomUnits y = u
Module: Mathlib.RingTheory.IntegralDomain

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) ↑(range (orderOf x))

Tactic:
simpa using

Goal state after:
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #{g | f.toHomUnits g = 1}
⊢ Set.InjOn (fun x_1 ↦ x ^ x_1) (Set.Iio (orderOf x))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
f : N ⟶ L
hx : addEquiv₀.symm f ∈ ((mk₀ g).precomp L ⋯).ker
⊢ addEquiv₀.symm f = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
L M N : C
g : M ⟶ N
hg : Epi g
f : N ⟶ L
hx : addEquiv₀.symm f ∈ ((mk₀ g).precomp L ⋯).ker
⊢ g ≫ f = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
⊢ Function.Injective ⇑(toLin' M)

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝² : Fintype n
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → M *ᵥ v ≠ 0
⊢ ∀ (v : n → K), M *ᵥ v = 0 → v = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : DecidableEq n
⊢ (∃ v, v ≠ 0 ∧ v ᵥ* M = 0) ↔ M.det = 0

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : DecidableEq n
⊢ (∃ v, v ≠ 0 ∧ Mᵀ *ᵥ v = 0) ↔ Mᵀ.det = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: n : Type u_1
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
M : Matrix n n A
inst✝ : Finite n
⊢ M.Nondegenerate ↔ M.SeparatingLeft

Tactic:
classical
  have := Fintype.ofFinite n
  rw [nondegenerate_iff_det_ne_zero, separatingLeft_iff_det_ne_zero]

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

Goal state before:
pp: n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ (-↑g).det = 1

Tactic:
simpa using

Goal state after:
n : Type u
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Fact (Even (Fintype.card n))
g : SpecialLinearGroup n R
⊢ (-↑g).det = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ det ![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]] = 1

Tactic:
simpa using

Goal state after:
R : Type v
inst✝ : CommRing R
A : SL(2, R)
⊢ ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0 = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ c = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
inst✝ : Field R
a b c d : R
h_det : a * d - b * c = 1
hg : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 = 0
⊢ c = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case refine_1
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
h : transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)
r : F
left✝ : r ^ Fintype.card ι = 1
hr : (scalar ι) r = ↑(transvection hij b)
⊢ b = 0

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
h : transvection hij b ∈ Subgroup.center (SpecialLinearGroup ι F)
r : F
left✝ : r ^ Fintype.card ι = 1
hr : (scalar ι) r = ↑(transvection hij b)
⊢ b = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 0 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (a • Pi.single 0 1) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 0 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (a • Pi.single 0 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: case «0»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) = (a⁻¹ • Pi.single 1 1) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: case «1»
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
⊢ (diag2 a ha • Pi.single 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) = (a⁻¹ • Pi.single 1 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.SpecialLinearGroup.smul_def, diag2_coe]

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

Goal state before:
pp: case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
hx : x = i₀
⊢ (∏ i with i ≠ i₀, fun k ↦ if k = i then D i else if k = i₀ then (D i)⁻¹ else 1) x = D x

Tactic:
simpa using

Goal state after:
case pos
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i₀ : ι
D : ι → F
hD : D i₀ = ∏ x with x ≠ i₀, (D x)⁻¹
x : ι
hx : x = i₀
⊢ (∏ x with ¬x = i₀, if i₀ = x then D x else (D x)⁻¹) = ∏ x with ¬x = i₀, (D x)⁻¹
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

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
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : { f // ∀ (m : M), f m * f m = (Algebra.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
x : M
⊢ ((s.val.comp ((lift Q) of)).toLinearMap ∘ₗ CliffordAlgebra.ι Q) x =
    ((AlgHom.id R (CliffordAlgebra Q)).toLinearMap ∘ₗ CliffordAlgebra.ι Q) x

Tactic:
simpa using

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
C : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)
mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)
add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)
a : CliffordAlgebra Q
s : Subalgebra R (CliffordAlgebra Q) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : { f // ∀ (m : M), f m * f m = (Algebra.algebraMap R ↥s) (Q m) } :=
  ⟨LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι, ⋯⟩
x : M
⊢ ↑((LinearMap.codRestrict (Subalgebra.toSubmodule s) (CliffordAlgebra.ι Q) ι) x) = (CliffordAlgebra.ι Q) x
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ (diagonal D).det = 1

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : SpecialLinearGroup ι F
L L' : List (TransvectionStruct ι F)
D : ι → F
hM : ↑M = (List.map TransvectionStruct.toMatrix L).prod * diagonal D * (List.map TransvectionStruct.toMatrix L').prod
⊢ ∏ i, D i = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: case nil
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
⊢ P (List.map TransvectionStruct.toSpecialLinearGroup []).prod

Tactic:
simpa using

Goal state after:
case nil
F : Type u_1
inst✝³ : Field F
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial ι
P : SpecialLinearGroup ι F → Prop
M : SpecialLinearGroup ι F
hdiag : ∀ (i j : ι) (hij : i ≠ j) {c : F} (hc : c ≠ 0), P (diag2n hij c hc)
htransvec : ∀ (i j : ι) (hij : i ≠ j) (a : F), P (transvection hij a)
hmul : ∀ (A B : SpecialLinearGroup ι F), P A → P B → P (A * B)
i₀ j₀ : ι
hij₀ : i₀ ≠ j₀
hP1 : P 1
hdiagonal : ∀ (D : ι → F) (hD : (diagonal D).det = 1), P ⟨diagonal D, hD⟩
⊢ P 1
Module: Mathlib.Algebra.GradedMonoid

Goal state before:
pp: ι : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ (List.map f (List.finRange n)).prod =
    mk ((List.finRange n).dProdIndex fun i ↦ (f i).fst) ((List.finRange n).dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)

Tactic:
GradedMonoid.list_prod_map_eq_dProd

Goal state after:
ι : Type u_1
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ mk ((List.finRange n).dProdIndex fun i ↦ (f i).fst) ((List.finRange n).dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd) =
    mk ((List.finRange n).dProdIndex fun i ↦ (f i).fst) ((List.finRange n).dProd (fun i ↦ (f i).fst) fun i ↦ (f i).snd)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: g : SL(2, ℤ)
⊢ ↑(T * g) 1 = ↑g 1

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
⊢ of ![![1, 1] ᵥ* ↑g, ![0, 1] ᵥ* ↑g] 1 = ↑g 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: g : SL(2, ℤ)
⊢ ↑(T⁻¹ * g) 1 = ↑g 1

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
⊢ of ![![1, -1] ᵥ* ↑g, ![0, 1] ᵥ* ↑g] 1 = ↑g 1
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this : AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃
⊢ a * b * c = a * (b * c)

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this : AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃
⊢ a * b * c = a * (b * c)
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i), (mulHom A) ((of A i) y) = (mulHom A).flip ((of A i) y)

Tactic:
intro ai ax

Goal state after:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ (mulHom A) ((of A ai) ax) = (mulHom A).flip ((of A ai) ax)
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : M.SeparatingLeft
⊢ ((Matrix.toLinearMap₂' R) M).SeparatingLeft

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : M.SeparatingLeft
⊢ ∀ (x : m → R), (∀ (y : n → R), x ⬝ᵥ M *ᵥ y = 0) → x = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : M.SeparatingRight
⊢ ((Matrix.toLinearMap₂' R) M).SeparatingRight

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : M.SeparatingRight
⊢ ∀ (y : n → R), (∀ (x : m → R), x ⬝ᵥ M *ᵥ y = 0) → y = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).SeparatingLeft ↔ M.det ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ M.SeparatingLeft ↔ ¬M.det = 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.det ≠ 0

Tactic:
simpa using

Goal state after:
R : Type u_1
n : Type u_11
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : IsDomain R
M : Matrix n n R
⊢ M.SeparatingRight ↔ ¬M.det = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case cons
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, head k = 0) ∧ ∀ a ∈ tail, ∀ k < m, a k = 0
⊢ (head * tail.prod) n = 0

Tactic:
refine mul_apply_eq_zero hl.1 (ih hl.2) ?_

Goal state after:
case cons
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, head k = 0) ∧ ∀ a ∈ tail, ∀ k < m, a k = 0
⊢ n < m + tail.length • m
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case cons
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, head k = 0) ∧ ∀ a ∈ tail, ∀ k < m, a k = 0
⊢ n < m + tail.length • m

Tactic:
simpa using

Goal state after:
case cons
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : SetLike.GradedMonoid A
inst✝ : CanonicallyOrderedAdd ι
m : ι
head : ⨁ (i : ι), ↥(A i)
tail : List (⨁ (i : ι), ↥(A i))
ih : (∀ x ∈ tail, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < tail.length • m → tail.prod n = 0
n : ι
hn : n < (tail.length + 1) • m
hl : (∀ k < m, head k = 0) ∧ ∀ a ∈ tail, ∀ k < m, a k = 0
⊢ n < tail.length • m + m
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < (Multiset.map Prod.snd s).sum
⊢ ∀ xn ∈ s.toList, ∀ k < xn.2, xn.1 k = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < (Multiset.map Prod.snd s).sum
⊢ ∀ (a : ⨁ (i : ι), ↥(A i)) (b : ι), (a, b) ∈ s → ∀ k < b, a k = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s.toList, ∀ k < ?m.56, x k = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Multiset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ ∀ x ∈ s, ∀ k < ?m.56, x k = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ (∏ xn ∈ s, xn.1) n = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ (∏ xn ∈ s, xn.1) n = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ ∀ xn ∈ s.toList, ∀ k < xn.2, xn.1 k = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset ((⨁ (i : ι), ↥(A i)) × ι)
hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0
n : ι
hn : n < ∑ xn ∈ s, xn.2
⊢ ∀ (a : ⨁ (i : ι), ↥(A i)) (b : ι), (a, b) ∈ s → ∀ k < b, a k = 0
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ (∏ x ∈ s, x) n = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : LinearOrder ι
inst✝⁶ : IsOrderedAddMonoid ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : CanonicallyOrderedAdd ι
inst✝³ : CommSemiring R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : SetLike.GradedMonoid A
s : Finset (⨁ (i : ι), ↥(A i))
m : ι
hs : ∀ x ∈ s, ∀ k < m, x k = 0
n : ι
hn : n < s.card • m
⊢ (∏ x ∈ s, x) n = 0