awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
this_1 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) m : M))
hik_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) k : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
h₁' :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) i : M) =
    (P.root : (a : ι) → M) (-l)
h₂' :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) (-m)
h₃' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) i : M))
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) = 0
aux₁ :
  ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 0)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (- -m) : M))

Tactic:
simpa only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
this_1 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) m : M))
hik_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) k : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
h₁' :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) i : M) =
    (P.root : (a : ι) → M) (-l)
h₂' :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) (-m)
h₃' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) i : M))
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) = 0
aux₁ :
  ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 0)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) (- -k) : M))

Tactic:
simpa only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
this_1 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) m : M))
hik_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) k : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
h₁' :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) i : M) =
    (P.root : (a : ι) → M) (-l)
h₂' :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) (-m)
h₃' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) i : M))
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) = 0
aux₁ :
  ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 0)
⊢ ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 0)

Tactic:
simpa using aux_2 hj hi hij.symm h₂' h₁' h₃' hkj (by simpa)
      hjl_mem (by simpa only [neg_neg]) (by simpa only [neg_neg])

Premises used: Ne.symm, _private.0.RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_2
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
this_1 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) m : M))
hik_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) k : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
h₁' :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) i : M) =
    (P.root : (a : ι) → M) (-l)
h₂' :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) (-m)
h₃' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) i : M))
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) = 0
aux₁ :
  ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 0)
⊢ ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 0)

Tactic:
have aux₂ : ¬(P.chainBotCoeff j (-l) = 1 ∧ P.chainBotCoeff i m = 0) := by
    simpa using aux_2 hj hi hij.symm h₂' h₁' h₃' hkj (by simpa)
      hjl_mem (by simpa only [neg_neg]) (by simpa only [neg_neg])
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M) = (P.root : (a : ι) → M) l
h₂ :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M) = (P.root : (a : ι) → M) m
h₃ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
this_1 : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) m : M))
hik_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) k : M))
hjk_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
hjl_mem :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (-l) : M))
h₁' :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) i : M) =
    (P.root : (a : ι) → M) (-l)
h₂' :
  HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) (-m)
h₃' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) (-k) : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) i : M))
hki : P.pairingIn ℤ k i < 0
hik : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i k = 0
hkj : P.pairingIn ℤ (-k) j < 0
hjk : chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-k) = 0
aux₁ :
  ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 0)
aux₂ :
  ¬(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) j (-l) = 1 ∧
      chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = 0)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i m = if P.pairingIn ℤ i m = 0 then 1 else 0

Tactic:
have := P.chainBotCoeff_if_one_zero him_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
a : ∀ (k l : ↥b.support), ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)
a₃ : ∀ (k l : ι), ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
⊢ ⁅h j, e i⁆ = b.cartanMatrix i j • e i

Tactic:
ext (k | k) (l | l)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k l : ↥b.support
⊢ ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)

Tactic:
simp [h, e]

Premises used: RootPairing.GeckConstruction.h, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j k : ↥b.support
l : ι
⊢ ∀ (b_1 : ι),
    Membership.mem (γ := Finset ι) Finset.univ b_1 →
      b_1 ≠ l →
        HMul.hMul (α := R) (β := R)
            ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R)
                (fun (i' : ↥b.support) (j : ι) ↦ if i' = i ∧ j = -(↑i : ι) then 1 else 0) k b_1 :
              R)
            (Matrix.fromBlocks (l := ↥b.support) (n := ↥b.support) 0 0 0
                (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) (Sum.inr b_1) (Sum.inr l) :
              R) =
          0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k : ι
l : ↥b.support
a :
  Bracket.bracket (L := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)))
      (Matrix.fromBlocks 0
        ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
          if i' = i ∧ j = -(↑i : ι) then 1 else 0)
        ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
          if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
          if
              (P.root : (a : ι) → M) i' =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M) then
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
          else 0))
      (Sum.inr k) (Sum.inl l) =
    HSMul.hSMul (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (b.cartanMatrix i j)
      (Matrix.fromBlocks 0
        ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
          if i' = i ∧ j = -(↑i : ι) then 1 else 0)
        ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
          if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
          if
              (P.root : (a : ι) → M) i' =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M) then
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
          else 0))
      (Sum.inr k) (Sum.inl l)
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)

Tactic:
simp only [h, e]

Premises used: RootPairing.GeckConstruction.h, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k : ι
l : ↥b.support
⊢ Bracket.bracket (L := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)))
      (Matrix.fromBlocks 0
        ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
          if i' = i ∧ j = -(↑i : ι) then 1 else 0)
        ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
          if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
          if
              (P.root : (a : ι) → M) i' =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M) then
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
          else 0))
      (Sum.inr k) (Sum.inl l) =
    HSMul.hSMul (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (b.cartanMatrix i j)
      (Matrix.fromBlocks 0
        ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
          if i' = i ∧ j = -(↑i : ι) then 1 else 0)
        ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
          if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
        ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
          if
              (P.root : (a : ι) → M) i' =
                HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M) then
            HAdd.hAdd (α := R)
              (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
          else 0))
      (Sum.inr k) (Sum.inl l)

Tactic:
aesop