awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
rwa₄ : ∀ (h : P.pairing i j = 0 ∧ P.pairing j i = 0), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₅ : ∀ (h : P.pairing i j = 0 ∧ P.pairing i j = 0), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
rwa₄ : ∀ (h : P.pairing i j = 0 ∧ P.pairing j i = 0), P.pairingIn ℤ i j = 0
rwa₅ : ∀ (h : P.pairing i j = 0 ∧ P.pairing i j = 0), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₆ : ∀ (h : P.pairing i j = 0), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
rwa₄ : ∀ (h : P.pairing i j = 0 ∧ P.pairing j i = 0), P.pairingIn ℤ i j = 0
rwa₅ : ∀ (h : P.pairing i j = 0 ∧ P.pairing i j = 0), P.pairingIn ℤ i j = 0
rwa₆ : ∀ (h : P.pairing i j = 0), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₇ : ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
rwa₄ : ∀ (h : P.pairing i j = 0 ∧ P.pairing j i = 0), P.pairingIn ℤ i j = 0
rwa₅ : ∀ (h : P.pairing i j = 0 ∧ P.pairing i j = 0), P.pairingIn ℤ i j = 0
rwa₆ : ∀ (h : P.pairing i j = 0), P.pairingIn ℤ i j = 0
rwa₇ : ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0
have rwa₈ : ∀ (h : P.pairingIn ℤ i j = 0), P.pairingIn ℤ i j = 0
Tactic: rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have this : Module.IsReflexive R M
Tactic: have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this : Module.IsReflexive R M
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have this₁ : Module.IsReflexive R N
Tactic: have : Module.IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this : Module.IsReflexive R N
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have this₁ : IsAddTorsionFree M
Tactic: have : IsAddTorsionFree M := .of_isTorsionFree R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have pos : ∀
  (hli :
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
Tactic: by_cases hli : LinearIndependent R ![α i, α j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
pos :
  ∀
    (hli :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have neg : ∀
  (hli :
    ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
Tactic: by_cases hli : LinearIndependent R ![α i, α j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
this : P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have inl : ∀ (h₁ : P.pairingIn ℤ i j = 1),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
Tactic: rcases this with h₁ | h₁
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
this : P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
inl :
  ∀ (h₁ : P.pairingIn ℤ i j = 1),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have inr : ∀ (h₁ : P.pairingIn ℤ j i = 1),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
Tactic: rcases this with h₁ | h₁
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
h₁ : P.pairingIn ℤ i j = 1
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have h₂ : P.pairing i j = 1
Tactic: replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
h₁ : P.pairingIn ℤ j i = 1
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have h₂ : P.pairing j i = 1
Tactic: replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
h₁ : P.pairing j i = 1
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have inr : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M))
Tactic: rw [← neg_mem_range_root_iff, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
have pos : P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
Tactic: suffices P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1 by
      rcases this with h₁ | h₁
      · replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        exact ⟨P.reflectionPerm j i, by simpa [h₁] using P.reflection_apply_root j i⟩
      · replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        rw [← neg_mem_range_root_iff, neg_sub]
        exact ⟨P.reflectionPerm i j, by simpa [h₁] using P.reflection_apply_root i j⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)
have aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
Tactic: have aux₁ := P.coxeterWeightIn_mem_set_of_isCrystallographic i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
⊢ Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)
have aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
Tactic: have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
⊢ Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)
have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0
Tactic: have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by
        simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
have this₁ : Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)
Tactic: have : P.coxeterWeightIn ℤ i j ∈ ({1, 2, 3} : Set _) := by
      have aux₁ := P.coxeterWeightIn_mem_set_of_isCrystallographic i j
      have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli
      have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by
        simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'
      simp_all
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
this : Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)
⊢ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
have this₁ : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
  P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
    P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
      P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 1 ∨
        P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
          P.pairingIn ℤ i j = -2 ∧ P.pairingIn ℤ j i = -1 ∨
            P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
              P.pairingIn ℤ i j = 3 ∧ P.pairingIn ℤ j i = 1 ∨
                P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -3 ∧ P.pairingIn ℤ j i = -1
Tactic: simp_rw [coxeterWeightIn, Int.mul_mem_one_two_three_iff, mem_insert_iff, mem_singleton_iff,
      Prod.mk.injEq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(1, 4), (2, 2), (4, 1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
have this₁ : Membership.mem (γ := Set (ℤ × ℤ))
  {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
    (-4, -1), (-1, -4), (2, 2), (-2, -2)}
  (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
Tactic: have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j