mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ibc : IsBaseChange R (Fintype.linearCombination S ⇑b)
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
set ε := Fintype.linearCombination S (fun i ↦ b i)

Goal state after:
case inr
R : Type u_3
V : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Free R V
inst✝ : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R := ↑(MvPolynomial.aeval (Sum.elim (fun i ↦ f (b i)) fun i ↦ (b.coord i) v))
this : IsDomain S
x✝² : Algebra S R := γ.toAlgebra
x✝¹ : Module S V := compHom V γ
x✝ : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun i ↦ b i
ibc : IsBaseChange R ε
⊢ LinearMap.det (transvection f v) = 1 + f v
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₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (e0 Q * (v Q) m₂) -
      (e0 Q * (v Q) m₁ * (algebraMap R (CliffordAlgebra (Q' Q))) r₂ +
        (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (algebraMap R (CliffordAlgebra (Q' Q))) r₂) =
    e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)

Tactic:
← Algebra.commutes,

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₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (e0 Q * (v Q) m₂) -
      ((algebraMap R (CliffordAlgebra (Q' Q))) r₂ * (e0 Q * (v Q) m₁) +
        (algebraMap R (CliffordAlgebra (Q' Q))) r₁ * (algebraMap R (CliffordAlgebra (Q' Q))) r₂) =
    e0 Q * (v Q) m₁ * (e0 Q * (v Q) m₂) + r₁ • e0 Q * (v Q) m₂ - r₂ • e0 Q * (v Q) m₁ -
      (algebraMap R (CliffordAlgebra (Q' Q))) (r₁ * r₂)
Module: Mathlib.LinearAlgebra.TensorProduct.Graded.External

Goal state before:
pp: 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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ ↑↑((-1) ^ (j * i)) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a = (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a

Tactic:
Int.cast_smul_eq_zsmul,

Goal state after:
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)
i j : ι
a : 𝒜 i
b : ℬ j
⊢ ↑((-1) ^ (j * i)) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a = (-1) ^ (j * i) • (lof R ι ℬ j) b ⊗ₜ[R] (lof R ι 𝒜 i) a
Module: Mathlib.LinearAlgebra.FreeProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
inst✝² : DecidableEq ι
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
motive : (⨁ (i : ι), M i) → Prop
x : ⨁ (i : ι), M i
zero : motive 0
lof : ∀ (i : ι) (x : M i), motive ((DirectSum.lof R ι M i) x)
add : ∀ (x y : ⨁ (i : ι), M i), motive x → motive y → motive (x + y)
⊢ motive x

Tactic:
by
  induction x using DirectSum.induction_on with
  | zero => exact zero
  | of => exact lof _ _
  | add x y hx hy => exact add x y hx hy

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

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (S • B) → C B

Tactic:
intro ih

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (S • B)
⊢ C B
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
⊢ C (T • B) → C B

Tactic:
intro ih

Goal state after:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m
ih : C (T • B)
⊢ C B
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
hA : C (reduce A)
⊢ C A

Tactic:
← reduce_reduceStep hc

Goal state after:
case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
hA : C (reduce (reduceStep A))
⊢ C A
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j (c • u) (p i) i =
    c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j u (p i) i

Tactic:
Finset.prod_congr rfl (fun i hi ↦ ?_)

Goal state after:
case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ c * u (p j) * (univ.erase j).prod ?m.57 = c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j u (p i) i

n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ n → R

n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
i : n
hi : i ∈ univ.erase j
⊢ M.updateCol j (c • u) (p i) i = ?m.57 i
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → (j : κ i) → M i j
i : ι
x y : (j : κ i) → M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update m i (x + y) i_1 (p i_1)) =
    ((fun p ↦ (f p) fun i_1 ↦ Function.update m i x i_1 (p i_1)) + fun p ↦
        (f p) fun i_1 ↦ Function.update m i y i_1 (p i_1))
      p

Tactic:
dsimp
    simp_rw [Function.apply_update (fun i m => m (p i)) m, Pi.add_apply, (f p).map_update_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
this : Fintype ι
⊢ ((fromDirectSumEquiv f) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) = (f p) x

Tactic:
fromDirectSumEquiv,

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
this : Fintype ι
⊢ (((fromDFinsuppEquiv κ R) f) fun i ↦ (lof R (κ i) (M i) (p i)) (x i)) = (f p) x
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁶ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
x : ⨁ (i : ι) (j : κ i), M i j
⊢ (fromDirectSumEquiv f) ⇑x = ∑ p ∈ Fintype.piFinset fun i ↦ DFinsupp.support (x i), (f p) fun i ↦ (x i) (p i)

Tactic:
fromDirectSumEquiv,

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁶ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) M'
x : ⨁ (i : ι) (j : κ i), M i j
⊢ ((fromDFinsuppEquiv κ R) f) ⇑x = ∑ p ∈ Fintype.piFinset fun i ↦ DFinsupp.support (x i), (f p) fun i ↦ (x i) (p i)
Module: Mathlib.LinearAlgebra.Multilinear.DirectSum

Goal state before:
pp: R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ fromDirectSumEquiv.symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)

Tactic:
fromDirectSumEquiv,

Goal state after:
R : Type u_1
ι : Type u_2
M' : Type u_3
κ : ι → Type u_4
M : (i : ι) → κ i → Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (j : κ i) → AddCommMonoid (M i j)
inst✝⁵ : (i : ι) → (j : κ i) → Module R (M i j)
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
inst✝² : DecidableEq ι
inst✝¹ : Finite ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ ⨁ (j : κ i), M i j) M'
p : (i : ι) → κ i
this : Fintype ι
⊢ (fromDFinsuppEquiv κ R).symm f p = f.compLinearMap fun i ↦ lof R (κ i) (M i) (p i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Generators

Goal state before:
pp: R : Type u_1
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
n : ℕ
hn :
  ∀ {ι : Type u_2} [Finite ι] {M : ι → Type u_3} {γ : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (M i)]
    [inst_1 : (i : ι) → Module R (M i)] {g : ⦃i : ι⦄ → γ i → M i},
    (∀ (i : ι), Submodule.span R (Set.range g) = ⊤) →
      ∀ {φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N},
        (∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))) → Nat.card ι = n → φ = φ'
ι : Type u_2
inst✝² : Finite ι
M : ι → Type u_3
γ : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
g : ⦃i : ι⦄ → γ i → M i
hg : ∀ (i : ι), Submodule.span R (Set.range g) = ⊤
φ φ' : (⨂[R] (i : ι), M i) →ₗ[R] N
h : ∀ (j : (i : ι) → γ i), φ (⨂ₜ[R] (i : ι), g (j i)) = φ' (⨂ₜ[R] (i : ι), g (j i))
hι : Nat.card ι = n + 1
⊢ 0 < Nat.card ι

Tactic:
by omega

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 ι
p : ℙ F (Fin 2 → F)
g_SL : SL(2, F)
⊢ Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (MulAut.conj g_SL • lineStab p.submodule) =
    MulAut.conj ↑g_SL • PSL.iwasawaT p

Tactic:
PSL.iwasawaT_map_conj

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : Field F
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
p : ℙ F (Fin 2 → F)
g_SL : SL(2, F)
⊢ MulAut.conj ↑g_SL • Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (lineStab p.submodule) =
    MulAut.conj ↑g_SL • PSL.iwasawaT p
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
hF : 4 ≤ Nat.card F
⊢ 0 < Nat.card F

Tactic:
by omega

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

Goal state before:
pp: 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
this : (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1
⊢ a • D.rep = D.rep + 1 • (↑a - 1) • ↑⟨D.rep, hD_mem⟩

Tactic:
Units.smul_def

Goal state after:
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
this : (b.repr D.rep) ⟨D.rep, hD_mem⟩ = 1
⊢ ↑a • D.rep = D.rep + 1 • (↑a - 1) • ↑⟨D.rep, hD_mem⟩
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := Module.Free.chooseBasis R V
this : Fintype (Module.Free.ChooseBasisIndex R V) := Module.Free.ChooseBasisIndex.fintype R V
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R :=
  (Matrix.SpecialLinearGroup.toLin_equiv b).symm
⊢ (∃ r,
      r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1 ∧
        (Matrix.scalar (Module.Free.ChooseBasisIndex R V)) r = ↑(e g)) ↔
    ∃ r, r ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1 ∧ ↑↑g = r • LinearMap.id

Tactic:
apply exists_congr

Goal state after:
case inr
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g : SpecialLinearGroup R V
hR : Nontrivial R
b : Module.Basis (Module.Free.ChooseBasisIndex R V) R V := ⋯
this : Fintype (Module.Free.ChooseBasisIndex R V) := ⋯
e : SpecialLinearGroup R V ≃* Matrix.SpecialLinearGroup (Module.Free.ChooseBasisIndex R V) R := ⋯
⊢ ∀ (a : R),
    a ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1 ∧
        (Matrix.scalar (Module.Free.ChooseBasisIndex R V)) a = ↑(e g) ↔
      a ^ Fintype.card (Module.Free.ChooseBasisIndex R V) = 1 ∧ ↑↑g = a • LinearMap.id
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case refine_2
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
l : ℙ K (ι → K)
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
⊢ m • l = l

Tactic:
induction l using Projectivization.ind with | _ v hv =>
    simp only [smul_mk, mk_eq_mk_iff']
    use r
    change _ = m.1 • v
    simp [← hr2]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ ↑(centerEquivRootsOfUnity g) = 1

Tactic:
apply rootsOfUnity.eq_one

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
d1 : Module.finrank R V ≤ 1
g : ↥(Subgroup.center (SpecialLinearGroup R V))
⊢ max (Module.finrank R V) 1 = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case e'_2
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(((centerCongr (toLin_equiv b)).trans centerEquivRootsOfUnity) g) = 1

Tactic:
apply rootsOfUnity.eq_one

Goal state after:
case e'_2
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ max (Module.finrank R V) 1 = 1
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case e'_3
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ ↑(center_equiv_rootsOfUnity g) = 1

Tactic:
apply rootsOfUnity.eq_one

Goal state after:
case e'_3
R : Type u_4
inst✝⁶ : CommRing R
V : Type u_5
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Free R V
inst✝² : Module.Finite R V
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Module.Basis ι R V
g : ↥(center (Matrix.SpecialLinearGroup ι R))
a✝ : Nontrivial R
hV : Subsingleton V
⊢ max (Fintype.card ι) 1 = 1
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Module.finrank R ↥Q.radical = Module.finrank R ↥Q'.radical

Tactic:
← e.map_radical,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Module.finrank R ↥Q.radical = Module.finrank R ↥(Submodule.map (↑e.toLinearEquiv) Q.radical)
Module: Mathlib.LinearAlgebra.QuadraticForm.Radical

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
⊢ Q.radical = LinearMap.ker (associated Q)

Tactic:
rw [radical_eq_ker_polarBilin]

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup P
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module R P
Q : QuadraticMap R M P
inst✝ : Invertible 2
⊢ LinearMap.ker Q.polarBilin = LinearMap.ker (associated Q)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' : P.root k + P.root l ∈ range ⇑P.root
hl : P.root l = P.root l + P.root k - P.root j
⊢ False

Tactic:
add_sub_assoc,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' : P.root k + P.root l ∈ range ⇑P.root
hl : P.root l = P.root l + (P.root k - P.root j)
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
⊢ P.root (-k) + P.root j - P.root i ∈ range ⇑P.root

Tactic:
rw [← neg_mem_range_root_iff]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk : P.root k + P.root i - P.root j ∈ range ⇑P.root
hkj : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
⊢ -(P.root (-k) + P.root j - P.root i) ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
hk : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
⊢ P.root k + P.root i ∈ range ⇑P.root

Tactic:
rw [← neg_mem_range_root_iff]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CharZero R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : Finite ι
inst✝ : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hkj : P.root k ≠ -P.root i
hk' : P.root k - P.root j ∈ range ⇑P.root
_i : InvolutiveNeg ι := P.indexNeg
hk : P.root (-k) + P.root j - P.root i ∈ range ⇑P.root
⊢ -(P.root k + P.root i) ∈ range ⇑P.root