awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ℕ
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
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hkn : b.height k = (↑n : ℤ)
hkpos : b.IsPos k
rw :
  (P.root : (a : ι) → M) i =
    HAdd.hAdd (β := M) (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) j : M)
⊢ (P.root : (a : ι) → M) i = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M)

Tactic:
rw [hk]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ℕ
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
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hkn : b.height k = (↑n : ℤ)
hkpos : b.IsPos k
⊢ (P.root : (a : ι) → M) i =
    HAdd.hAdd (β := M) (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
      ((P.root : (a : ι) → M) j : M)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ℕ
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
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
k : ι
hk :
  (P.root : (a : ι) → M) k = HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hkn : b.height k = (↑n : ℤ)
hkpos : b.IsPos k
⊢ p i

Tactic:
exact h₂ k j i (by rw [hk]; module) (ih hkpos hkn) hj
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ℕ
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
⊢ 0 < b.height i

Tactic:
rw [isPos_iff] at h₀

Premises used: RootPairing.Base.isPos_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ℕ
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
h₃ : 0 < b.height i
⊢ b.height i = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1

Tactic:
rw [isPos_iff] at h₀

Premises used: RootPairing.Base.isPos_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ℕ
ih : ∀ {i : ι} (h₀ : b.IsPos i) (hN : b.height i = -(↑n : ℤ)), p i
i : ι
h₀ : 0 < b.height i
hN : b.height i = HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1
⊢ p i

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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
⊢ 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

Premises used: False.elim, RootPairing.zero_lt_pairingIn_iff', RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn, Submodule.zero, RootPairing.Base.isPos_iff, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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 : ι
hj : j ∈ b.support
⊢ range ![j] ⊆ (↑b.support : Set ι) ∧
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (∑ m : Fin 1, (P.root : (a : ι) → M) (![j] m) : M) ∧
      ∀ (m : Fin 1),
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
          (∑ m' ∈ Finset.Iic m, (P.root : (a : ι) → M) (![j] m'))

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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'))
⊢ ∃ (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'))

Tactic:
apply hi.induction_on_add (fun j hj ↦ ⟨1, ![j], by simpa⟩)

Premises used: RootPairing.Base.IsPos.induction_on_add
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
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'))
⊢ (∃ (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'))

Tactic:
⟨n, f, h₂, h₃, h₄⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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'))

Tactic:
⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩

Premises used: Fin.snoc, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
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' : ι))
⊢ ∃ (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:
refine ⟨n + 1, Fin.snoc f k, ?_, ?_, fun m ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ range (ι := Fin (n + 1)) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k) ⊆ (↑b.support : Set ι)

Tactic:
simpa using insert_subset h₅ h₂

Premises used: Set.insert_subset
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ 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:
simp [Fin.sum_univ_castSucc, h₁, h₃]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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' : ι))
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' : ι))
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ m = ⟨(↑m : ℕ), hm⟩.castSucc

Tactic:
have : m = (⟨m, hm⟩ : Fin n).castSucc := rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
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 : ι))
⊢ 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:
rw [this, Fin.sum_Iic_castSucc]

Premises used: Fin.sum_Iic_castSucc
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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))
    (∑ i ∈ Finset.Iic (⟨(↑m : ℕ), hm⟩ : Fin n),
      (P.root : (a : ι) → M) (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ ι) f k i.castSucc : ι))

Tactic:
simp only [Fin.snoc_castSucc, h₄]

Premises used: Fin.snoc_castSucc
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ (↑m : ℕ) = n

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ (↑m : ℕ) = n

Tactic:
replace hm : m = n := by lia