awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (hypothesis)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
⊢ (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 (-k) + 1) =
    (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 k + 1)
have key₂ : P.pairingIn ℤ i m = 0
Tactic: have key₂ : P.pairingIn ℤ i m = 0 := P.pairingIn_eq_zero_iff.mp <| by simpa [aux₁] using aux₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (hypothesis)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this_4 : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
this : 2 ≤ P.pairingIn ℤ j k
⊢ P.pairingIn ℤ j k = 2
have this₁ : Membership.mem (γ := Set ℤ) {-2, -1, 0, 1, 2} (P.pairingIn ℤ j k)
Tactic: have := IsNotG2.pairingIn_mem_zero_one_two (P := P) j k
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
⊢ P.pairingIn ℤ j k = 2
have suffices : 2 ≤ P.pairingIn ℤ j k
Tactic: suffices 2 ≤ P.pairingIn ℤ j k by have := IsNotG2.pairingIn_mem_zero_one_two (P := P) j k; grind
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
⊢ P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k
have a : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ n k) : R)
  ((algebraMap ℤ R : (a : ℤ) → R) (2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k) : R)
Tactic: apply algebraMap_injective ℤ R
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
⊢ Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ n k) : R)
    ((algebraMap ℤ R : (a : ℤ) → R) (2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k) : R)
have a : (HSub.hSub (β := N →ₗ[R] R)
        (HAdd.hAdd («α» := N →ₗ[R] R) (β := N →ₗ[R] R)
          ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) k) : N →ₗ[R] R)
          ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R))
        ((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) :
      (a : N) → R)
    ((P.coroot : (a : ι) → N) k : N) =
  HSub.hSub (β := R)
    (HAdd.hAdd («α» := R) (β := R) ((algebraMap ℤ R : (a : ℤ) → R) 2 : R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) k : N) :
        R))
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) k : N) :
      R)
Tactic: simp only [map_add, map_sub, algebraMap_pairingIn, ← root_coroot_eq_pairing, hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (hypothesis)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
⊢ 2 ≤ P.pairingIn ℤ j k
have hn₁ : P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k
Tactic: have hn₁ : P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k := by
      apply algebraMap_injective ℤ R
      simp only [map_add, map_sub, algebraMap_pairingIn, ← root_coroot_eq_pairing, hn]
      simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
hn₁ : P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k
⊢ P.pairingIn ℤ n k ≤ 0
have by_contra! : ∀ (contra : 0 < P.pairingIn ℤ n k), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (hypothesis)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
hn₁ : P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k
⊢ 2 ≤ P.pairingIn ℤ j k
have hn₂ : P.pairingIn ℤ n k ≤ 0
Tactic: have hn₂ : P.pairingIn ℤ n k ≤ 0 := by
      by_contra! contra; exact hnk_notMem <| P.root_sub_root_mem_of_pairingIn_pos contra hnk_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (hypothesis)
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
hki : P.pairingIn ℤ k i = 0
this_1 : Module.IsReflexive R M := ⋯
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))
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))
hjk_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) (-k) : M))
this_2 : P.IsNotG2
this_3 : InvolutiveNeg ι := P.indexNeg
this : IsAddTorsionFree M
n : ι
hn :
  (P.root : (a : ι) → M) n =
    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)
hnk_ne : n ≠ k
hkj_ne : k ≠ j ∧ Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) j : M)
hnk_notMem :
  HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) k : M) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
aux₀ : P.pairingIn ℤ j i = -P.pairingIn ℤ m i
aux₁ : P.pairingIn ℤ j i = 0
key₁ : P.pairingIn ℤ i k = 0
key₂ : P.pairingIn ℤ i m = 0
⊢ (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 (-k) + 1) =
    (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 k + 1)
have key₃ : P.pairingIn ℤ j k = 2
Tactic: have key₃ : P.pairingIn ℤ j k = 2 := by
    suffices 2 ≤ P.pairingIn ℤ j k by have := IsNotG2.pairingIn_mem_zero_one_two (P := P) j k; grind
    have hn₁ : P.pairingIn ℤ n k = 2 + P.pairingIn ℤ i k - P.pairingIn ℤ j k := by
      apply algebraMap_injective ℤ R
      simp only [map_add, map_sub, algebraMap_pairingIn, ← root_coroot_eq_pairing, hn]
      simp
    have hn₂ : P.pairingIn ℤ n k ≤ 0 := by
      by_contra! contra; exact hnk_notMem <| P.root_sub_root_mem_of_pairingIn_pos contra hnk_ne
    lia