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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -3
h₄ : 2 * x + -3 * y = -3 ∨ 2 * x + -3 * y = -1 ∨ 2 * x + -3 * y = 0 ∨ 2 * x + -3 * y = 1 ∨ 2 * x + -3 * y = 3
⊢ False
have h₅ : 2 * (x + 1) + -3 * y = -3 ∨
  2 * (x + 1) + -3 * y = -1 ∨ 2 * (x + 1) + -3 * y = 0 ∨ 2 * (x + 1) + -3 * y = 1 ∨ 2 * (x + 1) + -3 * y = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -3
h₄ : 2 * x + -3 * y = -3 ∨ 2 * x + -3 * y = -1 ∨ 2 * x + -3 * y = 0 ∨ 2 * x + -3 * y = 1 ∨ 2 * x + -3 * y = 3
h₅ :
  2 * (x + 1) + -3 * y = -3 ∨
    2 * (x + 1) + -3 * y = -1 ∨ 2 * (x + 1) + -3 * y = 0 ∨ 2 * (x + 1) + -3 * y = 1 ∨ 2 * (x + 1) + -3 * y = 3
⊢ False
have h₆ : 2 * x + -3 * (y - 1) = -3 ∨
  2 * x + -3 * (y - 1) = -1 ∨ 2 * x + -3 * (y - 1) = 0 ∨ 2 * x + -3 * (y - 1) = 1 ∨ 2 * x + -3 * (y - 1) = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -3
h₄ : 2 * x + -3 * y = -3 ∨ 2 * x + -3 * y = -1 ∨ 2 * x + -3 * y = 0 ∨ 2 * x + -3 * y = 1 ∨ 2 * x + -3 * y = 3
h₅ :
  2 * (x + 1) + -3 * y = -3 ∨
    2 * (x + 1) + -3 * y = -1 ∨ 2 * (x + 1) + -3 * y = 0 ∨ 2 * (x + 1) + -3 * y = 1 ∨ 2 * (x + 1) + -3 * y = 3
h₆ :
  2 * x + -3 * (y - 1) = -3 ∨
    2 * x + -3 * (y - 1) = -1 ∨ 2 * x + -3 * (y - 1) = 0 ∨ 2 * x + -3 * (y - 1) = 1 ∨ 2 * x + -3 * (y - 1) = 3
⊢ False
have h₇ : 2 * (x + 1) + -3 * (y - 1) = -3 ∨
  2 * (x + 1) + -3 * (y - 1) = -1 ∨
    2 * (x + 1) + -3 * (y - 1) = 0 ∨ 2 * (x + 1) + -3 * (y - 1) = 1 ∨ 2 * (x + 1) + -3 * (y - 1) = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -1
⊢ False
have h₄ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -1
h₄ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
⊢ False
have h₅ : 2 * (x + 1) + -1 * y = -3 ∨
  2 * (x + 1) + -1 * y = -1 ∨ 2 * (x + 1) + -1 * y = 0 ∨ 2 * (x + 1) + -1 * y = 1 ∨ 2 * (x + 1) + -1 * y = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -1
h₄ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
h₅ :
  2 * (x + 1) + -1 * y = -3 ∨
    2 * (x + 1) + -1 * y = -1 ∨ 2 * (x + 1) + -1 * y = 0 ∨ 2 * (x + 1) + -1 * y = 1 ∨ 2 * (x + 1) + -1 * y = 3
⊢ False
have h₆ : 2 * x + -1 * (y - 1) = -3 ∨
  2 * x + -1 * (y - 1) = -1 ∨ 2 * x + -1 * (y - 1) = 0 ∨ 2 * x + -1 * (y - 1) = 1 ∨ 2 * x + -1 * (y - 1) = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = -1
h₄ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
h₅ :
  2 * (x + 1) + -1 * y = -3 ∨
    2 * (x + 1) + -1 * y = -1 ∨ 2 * (x + 1) + -1 * y = 0 ∨ 2 * (x + 1) + -1 * y = 1 ∨ 2 * (x + 1) + -1 * y = 3
h₆ :
  2 * x + -1 * (y - 1) = -3 ∨
    2 * x + -1 * (y - 1) = -1 ∨ 2 * x + -1 * (y - 1) = 0 ∨ 2 * x + -1 * (y - 1) = 1 ∨ 2 * x + -1 * (y - 1) = 3
⊢ False
have h₇ : 2 * (x + 1) + -1 * (y - 1) = -3 ∨
  2 * (x + 1) + -1 * (y - 1) = -1 ∨
    2 * (x + 1) + -1 * (y - 1) = 0 ∨ 2 * (x + 1) + -1 * (y - 1) = 1 ∨ 2 * (x + 1) + -1 * (y - 1) = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = 0
⊢ False
have h₄ : 2 * x + 0 * y = -3 ∨ 2 * x + 0 * y = -1 ∨ 2 * x + 0 * y = 0 ∨ 2 * x + 0 * y = 1 ∨ 2 * x + 0 * y = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = 0
h₄ : 2 * x + 0 * y = -3 ∨ 2 * x + 0 * y = -1 ∨ 2 * x + 0 * y = 0 ∨ 2 * x + 0 * y = 1 ∨ 2 * x + 0 * y = 3
⊢ False
have h₅ : 2 * (x + 1) + 0 * y = -3 ∨
  2 * (x + 1) + 0 * y = -1 ∨ 2 * (x + 1) + 0 * y = 0 ∨ 2 * (x + 1) + 0 * y = 1 ∨ 2 * (x + 1) + 0 * y = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA
-- 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
this_1 : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M)
hki' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) k : M) (-(P.root : (a : ι) → M) i : M)
hli : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) i : M)
hli' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) l : M) (-(P.root : (a : ι) → M) i : M)
hmi : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) ((P.root : (a : ι) → M) i : M)
hmi' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) m : M) (-(P.root : (a : ι) → M) i : M)
hni : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) ((P.root : (a : ι) → M) i : M)
hni' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) n : M) (-(P.root : (a : ι) → M) i : M)
h₀ : 2 * x + A * y = -3 ∨ 2 * x + A * y = -1 ∨ 2 * x + A * y = 0 ∨ 2 * x + A * y = 1 ∨ 2 * x + A * y = 3
h₁ :
  2 * (x + 1) + A * y = -3 ∨
    2 * (x + 1) + A * y = -1 ∨ 2 * (x + 1) + A * y = 0 ∨ 2 * (x + 1) + A * y = 1 ∨ 2 * (x + 1) + A * y = 3
h₂ :
  2 * x + A * (y - 1) = -3 ∨
    2 * x + A * (y - 1) = -1 ∨ 2 * x + A * (y - 1) = 0 ∨ 2 * x + A * (y - 1) = 1 ∨ 2 * x + A * (y - 1) = 3
h₃ :
  2 * (x + 1) + A * (y - 1) = -3 ∨
    2 * (x + 1) + A * (y - 1) = -1 ∨
      2 * (x + 1) + A * (y - 1) = 0 ∨ 2 * (x + 1) + A * (y - 1) = 1 ∨ 2 * (x + 1) + A * (y - 1) = 3
hA : A = 0
h₄ : 2 * x + 0 * y = -3 ∨ 2 * x + 0 * y = -1 ∨ 2 * x + 0 * y = 0 ∨ 2 * x + 0 * y = 1 ∨ 2 * x + 0 * y = 3
h₅ :
  2 * (x + 1) + 0 * y = -3 ∨
    2 * (x + 1) + 0 * y = -1 ∨ 2 * (x + 1) + 0 * y = 0 ∨ 2 * (x + 1) + 0 * y = 1 ∨ 2 * (x + 1) + 0 * y = 3
⊢ False
have h₆ : 2 * x + 0 * (y - 1) = -3 ∨
  2 * x + 0 * (y - 1) = -1 ∨ 2 * x + 0 * (y - 1) = 0 ∨ 2 * x + 0 * (y - 1) = 1 ∨ 2 * x + 0 * (y - 1) = 3
Tactic: rw [hA] at h₀ h₁ h₂ h₃
Cleared hypotheses: h₀, h₁, h₂, h₃, hA