awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N_1 : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
P : RootPairing ι R M N_1
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
N : ℤ
hN : b.height i = N
zero : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = 0), p i
⊢ p i
have succ : ∀ (n : ℕ) (ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i) {i : ι} (h₀ : b.IsPos i)
  (hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), p i
Tactic: induction N using Int.induction_on generalizing i with
  | zero => exact False.elim <| b.height_ne_zero i hN
  | succ n ih =>
    obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
    rw [P.zero_lt_pairingIn_iff'] at hj'
    rcases eq_or_ne i j with rfl | hij; · exact h₁ i hj
    obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' hij
    have hkn : b.height k = n := by rw [b.height_sub hk, height_one_of_mem_support hj]; lia
    have hkpos : b.IsPos k := by rw [isPos_iff']; lia
    exact h₂ k j i (by rw [hk]; module) (ih hkpos hkn) hj
  | pred n ih =>
    rw [isPos_iff] at h₀
    lia
Cleared hypotheses: i, h₀, N, hN
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N_1 : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
P : RootPairing ι R M N_1
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
h₀ : b.IsPos i
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
N : ℤ
hN : b.height i = N
zero : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = 0), p i
succ :
  ∀ (n : ℕ) (ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = (↑n : ℤ)), p i) {i : ι} (h₀ : b.IsPos i)
    (hN : b.height i = HAdd.hAdd (α := ℤ) (↑n : ℤ) 1), p i
⊢ p i
have pred : ∀ (n : ℕ) (ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = -(↑n : ℤ)), p i) {i : ι} (h₀ : b.IsPos i)
  (hN : b.height i = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1), p i
Tactic: induction N using Int.induction_on generalizing i with
  | zero => exact False.elim <| b.height_ne_zero i hN
  | succ n ih =>
    obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
    rw [P.zero_lt_pairingIn_iff'] at hj'
    rcases eq_or_ne i j with rfl | hij; · exact h₁ i hj
    obtain ⟨k, hk⟩ := P.root_sub_root_mem_of_pairingIn_pos hj' hij
    have hkn : b.height k = n := by rw [b.height_sub hk, height_one_of_mem_support hj]; lia
    have hkpos : b.IsPos k := by rw [isPos_iff']; lia
    exact h₂ k j i (by rw [hk]; module) (ih hkpos hkn) hj
  | pred n ih =>
    rw [isPos_iff] at h₀
    lia
Cleared hypotheses: i, h₀, N, hN
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
⊢ ∃ (n : ℕ) (f : Fin n → ι),
    range f ⊆ (↑b.support : Set ι) ∧
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
        ∀ (m : Fin n),
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
have apply : ∀ (i j k : ι),
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
    (∃ (n : ℕ) (f : Fin n → ι),
        range f ⊆ (↑b.support : Set ι) ∧
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
            ∀ (m : Fin n),
              Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
                (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))) →
      j ∈ b.support →
        ∃ (n : ℕ) (f : Fin n → ι),
          range f ⊆ (↑b.support : Set ι) ∧
            Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
              ∀ (m : Fin n),
                Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
                  (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
Tactic: apply hi.induction_on_add (fun j hj ↦ ⟨1, ![j], by simpa⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
⊢ (∃ (n : ℕ) (f : Fin n → ι),
      range f ⊆ (↑b.support : Set ι) ∧
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
          ∀ (m : Fin n),
            Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
              (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))) →
    k ∈ b.support →
      ∃ (n : ℕ) (f : Fin n → ι),
        range f ⊆ (↑b.support : Set ι) ∧
          Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
            ∀ (m : Fin n),
              Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
                (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
have this : ∀ (n : ℕ) (f : Fin n → ι) (h₂ : range f ⊆ (↑b.support : Set ι))
  (h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M))
  (h₄ :
    ∀ (m : Fin n),
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))),
  k ∈ b.support →
    ∃ (n : ℕ) (f : Fin n → ι),
      range f ⊆ (↑b.support : Set ι) ∧
        Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
          ∀ (m : Fin n),
            Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
              (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
Tactic: ⟨n, f, h₂, h₃, h₄⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
⊢ ∃ (n : ℕ) (f : Fin n → ι),
    range f ⊆ (↑b.support : Set ι) ∧
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
        ∀ (m : Fin n),
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
have refine_1 : range (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k) ⊆ (↑b.support : Set ι)
Tactic: refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
refine_1 : range (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k) ⊆ (↑b.support : Set ι)
⊢ ∃ (n : ℕ) (f : Fin n → ι),
    range f ⊆ (↑b.support : Set ι) ∧
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
        ∀ (m : Fin n),
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
have refine_2 : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M)
  (∑ m : Fin (n + 1), (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m : ι) : M)
Tactic: refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
refine_1 : range (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k) ⊆ (↑b.support : Set ι)
refine_2 :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M)
    (∑ m : Fin (n + 1), (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m : ι) : M)
⊢ ∃ (n : ℕ) (f : Fin n → ι),
    range f ⊆ (↑b.support : Set ι) ∧
      Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) l : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M) ∧
        ∀ (m : Fin n),
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
            (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
have refine_3 : ∀ (m : Fin (n + 1)),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
Tactic: refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
have pos : ∀ (hm : (↑m : ℕ) < n),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
Tactic: by_cases hm : m < n
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
pos :
  ∀ (hm : (↑m : ℕ) < n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
have neg : ∀ (hm : ¬(↑m : ℕ) < n),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
Tactic: by_cases hm : m < n
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : (↑m : ℕ) < n
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
have this : m = ⟨(↑m : ℕ), hm⟩.castSucc
Tactic: have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : (↑m : ℕ) < n
this : m = ⟨(↑m : ℕ), hm⟩.castSucc
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
have pos : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (∑ i ∈ Finset.Iic (⟨(↑m : ℕ), hm⟩ : Fin n),
    (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k i.castSucc : ι))
Tactic: rw [this, Fin.sum_Iic_castSucc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : ¬(↑m : ℕ) < n
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
have hm₁ : (↑m : ℕ) = n
Tactic: replace hm : m = n := by lia
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : (↑m : ℕ) = n
⊢ Finset.Iic m = Finset.univ
have h : ∀ (a : Fin (n + 1)), a ∈ Finset.Iic m ↔ Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
hi : b.IsPos i
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
n : ℕ
f : Fin n → ι
h₂ : range f ⊆ (↑b.support : Set ι)
h₃ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin n, (P.root : (a : ι) → M) (f m) : M)
h₄ :
  ∀ (m : Fin n),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (f m'))
h₅ : k ∈ b.support
m : Fin (n + 1)
hm : (↑m : ℕ) = n
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k m' : ι))
have hm₁ : Finset.Iic m = Finset.univ
Tactic: replace hm : Finset.Iic m = Finset.univ := by ext; simp [hm, Fin.le_def, Fin.is_le]
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
this : InvolutiveNeg ι := P.indexNeg
⊢ p i
have inl : ∀ (hi : b.IsPos i), p i
Tactic: rcases IsPos.or_neg b i with hi | hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
this : InvolutiveNeg ι := P.indexNeg
inl : ∀ (hi : b.IsPos i), p i
⊢ p i
have inr : ∀ (hi : b.IsPos (-i)), p i
Tactic: rcases IsPos.or_neg b i with hi | hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
this_1 : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
this : p (-i)
⊢ p i
have rw : p (- -i)
Tactic: rw [← neg_neg i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : CharZero R
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : P.IsCrystallographic
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ :
  ∀ (i j k : ι),
    (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
      p i → j ∈ b.support → p k
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
⊢ p i
have inr : p (-i)
Tactic: suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this