mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0

Tactic:
nth_rewrite 1 [show D'.rep = (⟨D'.rep, hD'_mem⟩ : s) by rfl]

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
⊢ (b.repr ↑⟨D'.rep, hD'_mem⟩) ⟨D.rep, hD_mem⟩ = 0
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.Quotient.Bilinear

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ ∀ (x : M ⧸ M'), ((M'.liftQ f hM') x) n = 0 x

Tactic:
Submodule.Quotient.forall,

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝¹¹ : Ring R
inst✝¹⁰ : Ring R₂
inst✝⁹ : Ring S
inst✝⁸ : Ring S₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ ∀ (a : M), ((M'.liftQ f hM') (Submodule.Quotient.mk a)) n = 0 (Submodule.Quotient.mk a)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: 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
hι : IsEmpty ι
⊢ Subsingleton V

Tactic:
rw [← Module.finrank_eq_zero_iff_of_free (R := R),
        Module.finrank_eq_card_basis b, Fintype.card_of_isEmpty]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
i : ι
hi : ¬v i = 0
⊢ ∃ i ∈ univ, 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)

Tactic:
refine ⟨i, mem_univ _, ?_⟩

Goal state after:
case hs
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set ι
hs : ∀ i ∈ s, 0 < w i
v : ι → 𝕜
hv : v ∈ Pi.spanSubset 𝕜 s
i : ι
hi : ¬v i = 0
⊢ 0 < w i • (↑⟨v, hv⟩ i * ↑⟨v, hv⟩ i)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (∑ a₁,
        0 k a₁ *
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
            (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
            (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
            (Sum.inl a₁) (Sum.inr l) +
      ∑ a₂,
        if P.root a₂ = P.root ↑i + P.root l then (if -k = a₂ then 1 else 0) * (↑(chainBotCoeff (↑i) l) + 1)
        else (if -k = a₂ then 1 else 0) * 0) =
    ∑ x,
        (if -k = ↑i then ↑|b.cartanMatrix i x| else 0) *
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl x) (Sum.inr l) +
      ∑ a₂,
        if a₂ = -l then (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 1
        else (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 0

Tactic:
Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)

Goal state after:
case inr.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : RootPairing ι R M N
inst✝⁴ : P.IsCrystallographic
b : P.Base
inst✝³ : Finite ι
inst✝² : IsDomain R
inst✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (∑ a₁,
        0 k a₁ *
          Matrix.fromBlocks 0 (Matrix.of fun i' j ↦ if i' = i ∧ j = -↑i then 1 else 0)
            (Matrix.of fun i' j ↦ if i' = ↑i then ↑|b.cartanMatrix i j| else 0)
            (Matrix.of fun i' j ↦ if P.root i' = P.root ↑i + P.root j then ↑(chainBotCoeff (↑i) j) + 1 else 0)
            (Sum.inl a₁) (Sum.inr l) +
      if P.root (-k) = P.root ↑i + P.root l then (if -k = -k then 1 else 0) * (↑(chainBotCoeff (↑i) l) + 1)
      else (if -k = -k then 1 else 0) * 0) =
    ∑ x,
        (if -k = ↑i then ↑|b.cartanMatrix i x| else 0) *
          Matrix.fromBlocks 1 0 0 (Matrix.of fun i j ↦ if i = -j then 1 else 0) (Sum.inl x) (Sum.inr l) +
      ∑ a₂,
        if a₂ = -l then (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 1
        else (if P.root k = P.root a₂ - P.root ↑i then ↑(chainTopCoeff (↑i) a₂) + 1 else 0) * 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
P : RootPairing ι R M N
inst✝⁵ : P.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : ↥(cartanSubalgebra' b)
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx' : x ∈ lieAlgebra b
hx : ⟨x, hx'⟩ ∈ cartanSubalgebra' b
⊢ x ∈ span R (range h)

Tactic:
by simpa using! hx

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i

Tactic:
classical
  suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i) by
    replace this := congr_arg (ω b * ·) this
    simpa [← mul_assoc, ω_mul_ω] using this
  calc ω b * ⁅h j, f i⁆ = ω b * (h j * f i - f i * h j) := by rw [Ring.lie_def]
                      _ = -(h j * e i - e i * h j) * ω b := ?_
                      _ = -⁅h j, e i⁆ * ω b := by rw [Ring.lie_def]
                      _ = -(b.cartanMatrix i j • e i) * ω b := by rw [lie_h_e]
                      _ = ω b * (-b.cartanMatrix i j • f i) := ?_
  · rw [mul_sub, ← mul_assoc, ← mul_assoc, ω_mul_h, ω_mul_f, mul_assoc, mul_assoc, ω_mul_f, ω_mul_h,
      neg_sub, neg_mul, neg_mul, mul_neg, sub_mul, mul_assoc, mul_assoc]
    abel
  · rw [Matrix.mul_smul, ω_mul_f]
    simp [mul_assoc]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
n : ℕ
hn : e i ^ n = 0
⊢ ω b * f i ^ n = 0

Tactic:
suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
n : ℕ
hn : e i ^ n = 0
⊢ ω b * f i ^ n = e i ^ n * ω b
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j k : ↥b.support
l : ι
⊢ ⁅e i, f j⁆ (Sum.inl k) (Sum.inr l) = 0

Tactic:
classical
  let := P.indexNeg
  have aux₁ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root i + P.root l ∧ k = j ∧ x = j) := by
    rintro x - ⟨hl, -, rfl⟩
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  have aux₂ : ∀ x ∈ Finset.univ, ¬ (P.root x = P.root l - P.root j ∧ k = i ∧ x = -i) := by
    rintro x - ⟨hl, -, rfl⟩
    replace hl : P.root i = P.root j - P.root l := by simpa [neg_eq_iff_eq_neg] using hl
    exact b.sub_notMem_range_root i.property j.property ⟨-l, by simp [hl]⟩
  simp [e, f, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux₁, Finset.sum_ite_of_false aux₂]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
_i✝ : P.EmbeddedG2
_i : Nonempty ι
⊢ b.support.card = Fintype.card (Fin 2)

Tactic:
← Module.finrank_eq_card_basis (EmbeddedG2.basis P),

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsG2
b : P.Base
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
_i✝ : P.EmbeddedG2
_i : Nonempty ι
⊢ b.support.card = Module.finrank R M
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
i : ↥b.support
⊢ h₀ i = ⁅e₀ i, f₀ i⁆

Tactic:
ext1

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
⊢ ↑(h₀ i) = ↑⁅e₀ i, f₀ i⁆
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ ⁅e₀ i, f₀ i⁆ ∈ ↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))

Tactic:
apply LieSubalgebra.lie_mem

Goal state after:
case hx
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ e₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)

case hy
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ f₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Finite ι
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
b : P.Base
inst✝² : Fintype ι
i j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
k : ι
l : ↥b.support
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inl l) = 0 (Sum.inr k) (Sum.inl l)

Tactic:
have aux₁ : P.root k ≠ P.root i - P.root j :=
      fun contra ↦ b.sub_notMem_range_root i.property j.property ⟨k, contra⟩
    simp [e, f, ← sub_eq_add_neg, if_neg aux₁]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
⊢ U = ⊤

Tactic:
suffices ∀ j, v b j ∈ U by
    simp_rw [← LieSubmodule.toSubmodule_eq_top, eq_top_iff,
      ← (Pi.basisFun K (b.support ⊕ ι)).span_eq, Submodule.span_le, range_subset_iff,
      Pi.basisFun_apply]
    aesop

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
aux : ∀ (k : ↥b.support), u k ∈ U
⊢ ∀ (j : ι), v b j ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h₁
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k : ι
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ⁅e ⟨k, hk⟩, u ⟨k, hk⟩⁆ = 2 • v b k
⊢ v b k ∈ U

Tactic:
let e' : lieAlgebra b := ⟨e ⟨k, hk⟩, e_mem_lieAlgebra ⟨k, hk⟩⟩

Goal state after:
case h₁
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CharZero K
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module K M
inst✝⁴ : AddCommGroup N
inst✝³ : Module K N
P : RootPairing ι K M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k : ι
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
this : ⁅e ⟨k, hk⟩, u ⟨k, hk⟩⁆ = 2 • v b k
e' : ↥(lieAlgebra b) := ⟨e ⟨k, hk⟩, ⋯⟩
⊢ v b k ∈ U
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I J : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x - y ∈ J
hJI : J ≤ I
h₁ : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
h₂ : ↑p = 0
⊢ ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (x + (p - 1 - x)) =
    ∑ x ∈ Finset.range p, (Ideal.Quotient.mk I) y ^ (p - 1)

Tactic:
exact Finset.sum_congr rfl fun _ _ ↦ by grind

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
h : IsSymmetricAlgebra f
motive : A → Prop
algebraMap : ∀ (r : R), motive ((Algebra.algebraMap R A) r)
ι : ∀ (x : M), motive (f x)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
add : ∀ (a b : A), motive a → motive b → motive (a + b)
a : A
⊢ motive a

Tactic:
by
  rw [← h.equiv.right_inv a]
  generalize h.equiv.invFun a = y
  change motive (SymmetricAlgebra.lift f y)
  induction y using SymmetricAlgebra.induction with
  | algebraMap r => simpa using algebraMap r
  | ι y => simpa using ι y
  | mul _ _ hx hy => simpa using mul _ _ hx hy
  | add _ _ hx hy => simpa using add _ _ hx hy

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hW : 1 < finrank K (V ⧸ W)
⊢ W ⊔ K ∙ v < ⊤

Tactic:
rw [lt_top_iff_ne_top]

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hW : 1 < finrank K (V ⧸ W)
⊢ W ⊔ K ∙ v ≠ ⊤
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: case succ
K : Type u_1
inst✝³ : DivisionRing K
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
n : ℕ
hind :
  ∀ {e : V ≃ₗ[K] V},
    e.fixedReduce = 1 →
      finrank K (V ⧸ (↑e).fixedSubmodule) = n → e ∈ transvections K V ^ (n - 1) * dilatransvections K V
e : V ≃ₗ[K] V
he : e.fixedReduce = 1
h : finrank K (V ⧸ (↑e).fixedSubmodule) = n + 1
⊢ e ∈ transvections K V ^ (n + 1 - 1) * dilatransvections K V

Tactic:
match n with
    | 0 => simp [mem_dilatransvections_iff_finrank_quotient, h]
    | n + 1 =>
      simp only [add_assoc, Nat.reduceAdd] at h
      simp only [add_tsub_cancel_right] at hind
      simp only [add_tsub_cancel_right, pow_succ', mul_assoc, Set.mem_mul]
      /- We construct a linear form `f` which vanishes on `e.fixedSubmodule`,
        and a vector `v` such that `f v = 1`.
        Consider the transvection `t = transvection f v`.
        Then `t * e` satisfies the induction hypothesis and
        the relation `e = t⁻¹ * (t * e)` implies that `e` satisfies the theorem.
        This transvection is given by `auxTransvection`. -/
      have : ∃ f : Dual K V, ∃ v : V, e.fixedSubmodule ≤ ker f ∧ f v = 1 := by
        have : ∃ u : V, u ∉ e.fixedSubmodule := by
          by_contra! he
          rw [← Submodule.eq_top_iff'] at he
          rw [he, ← Nat.add_left_inj, Submodule.finrank_quotient_add_finrank, finrank_top] at h
          simp at h
        obtain ⟨u, hu⟩ := this
        obtain ⟨f, hfu, hf⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hu inferInstance
        let v := (f u)⁻¹ • u
        have hv : f v = 1 := by simp [v, inv_mul_cancel₀ hfu]
        exact ⟨f, v, by rwa [LinearMap.le_ker_iff_map], hv⟩
      obtain ⟨f, v, hf, hv⟩ := this
      -- We have chosen `f` and `v`.
      -- Since `f v = 1`, one has `v ∉ e.fixedSubmodule`.
      have hv_notMem : v ∉ e.fixedSubmodule := fun hv' ↦ by
        apply one_ne_zero' K
        rw [← hv, ← LinearMap.mem_ker]
        exact hf hv'
      -- Using that `e.fixedReduce = 1`, we have `v - e v ∈ e.fixedSubmodule`.
      have hv' : v - e v ∈ e.fixedSubmodule := by
        rw [← e.fixedSubmodule.ker_mkQ, LinearMap.mem_ker,
          map_sub, sub_eq_zero]
        simp [← fixedReduce_mk, he]
      set t := auxTransvection (e := e) (f := f) (u := v) (by
        simpa [hf] using hf (sub_mem_comm_iff.mp hv')) with ht
      refine ⟨t⁻¹, ?_, t * e, ?_, by simp⟩
      · -- We prove that `t⁻¹` is a transvection
        rw [inv_mem_transvections_iff, ht]
        apply mem_transvections
      -- It remains to prove that `t * e` satisfies the induction hypothesis
      apply hind
      · -- We prove that `(t * e).fixedReduce = 1`.
        simp only [ht, one_eq_refl, fixedReduce_eq_one, auxTransvection_mul_fixed hv] at he ⊢
        intro w
        simp only [auxTransvection, LinearEquiv.mul_apply, transvection.apply,
          add_sub_right_comm]
        apply mem_sup_left
        apply Submodule.add_mem _ (he w)
        exact smul_mem _ _ hv'
      · -- `finrank` condition
        rw [← Nat.add_left_inj, finrank_mod_auxTransvection_mul_fixed hv hv_notMem, h]

Goal state after:
Module: Mathlib.LinearAlgebra.Transvection.Generation

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
he : ∀ (v : V ⧸ (↑e).fixedSubmodule), ¬LinearIndependent K ![v, e.fixedReduce v]
⊢ ∃ a, ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x

Tactic:
obtain ⟨a, ha⟩ :=
      LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent h.ne' he

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
e : V ≃ₗ[K] V
h : 1 < finrank K (V ⧸ (↑e).fixedSubmodule)
he : ∀ (v : V ⧸ (↑e).fixedSubmodule), ¬LinearIndependent K ![v, e.fixedReduce v]
a : ↥(Subring.center K)
ha : ↑e.fixedReduce = a • 1
⊢ ∃ a, ∀ (x : V ⧸ (↑e).fixedSubmodule), e.fixedReduce x = a • x