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
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
h : ∀ (a : Fin (n + 1)), a ∈ Finset.Iic m ↔ Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ a
⊢ Finset.Iic m = Finset.univ

Tactic:
ext
-- 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
a : Fin (n + 1)
⊢ a ∈ Finset.Iic m ↔ Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ a

Tactic:
simp [hm, Fin.le_def, Fin.is_le]

Premises used: Fin.is_le, Fin.le_def
-- 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
⊢ Finset.Iic m = Finset.univ

Tactic:
replace hm : Finset.Iic m = Finset.univ := by ext; simp [hm, Fin.le_def, Fin.is_le]
-- 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 : Finset.Iic m = Finset.univ
⊢ 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:
simp [hm, 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 : ι
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
letI : p i
⊢ p i

Tactic:
letI := P.indexNeg
-- 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 : ι
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
inr : ∀ (hi : b.IsPos (-i)), p i
⊢ p i

Tactic:
rcases IsPos.or_neg b i with hi | hi

Premises used: RootPairing.Base.IsPos.or_neg
-- 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 : ι
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

Tactic:
hi.induction_on_add h₁ h₂

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 : ι
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

Tactic:
exact hi.induction_on_add h₁ h₂

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 : ι
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)
rw : p (- -i)
⊢ p i

Tactic:
rw [← neg_neg i]

Premises used: neg_neg
-- 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 : ι
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)

Tactic:
h₀ (-i) this

Premises used: Neg.neg
-- 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 : ι
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)

Tactic:
exact h₀ (-i) this

Premises used: Neg.neg
-- 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 : ι
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)
inr : p (-i)
⊢ p i

Tactic:
suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this
-- 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 : ι
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)

Tactic:
hi.induction_on_add h₁ h₂

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 : ι
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)

Tactic:
exact hi.induction_on_add h₁ h₂

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
inst_9 : P.IsReduced
i : ι
h₀ : b.IsPos i
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
generalize : ∀ (N_1 : ℕ) (hN : (b.height i).natAbs = N_1), p i
⊢ p i

Tactic:
generalize hN : (b.height i).natAbs = N

Premises used: RootPairing.Base.height, Int.natAbs
-- 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
ind : ∀ (j : ι) (hj : j ∈ b.support) (hj' : 0 < P.pairingIn ℤ j i), p i
⊢ p i

Tactic:
obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn

Premises used: RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn
-- 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ j i
⊢ 0 < P.pairingIn ℤ i j

Tactic:
rw [P.zero_lt_pairingIn_iff'] at hj'

Premises used: RootPairing.zero_lt_pairingIn_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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
ind : ∀ (hj : i ∈ b.support) (hj' : 0 < P.pairingIn ℤ i i), p i
ind₁ : ∀ (hij : i ≠ j), p i
⊢ p i

Tactic:
rcases eq_or_ne i j with rfl | hij

Premises used: eq_or_ne, 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
hj : i ∈ b.support
hj' : 0 < P.pairingIn ℤ i i
⊢ p i

Tactic:
h₁ i 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
hj : i ∈ b.support
hj' : 0 < P.pairingIn ℤ i i
⊢ p i

Tactic:
exact h₁ i 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
ind : ∀ (hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)), p i
⊢ p i

Tactic:
have hk := h₀.reflectionPerm hj hij
-- 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
this : b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i
⊢ (↑(b.height ((P.reflectionPerm j : (a : ι) → ι) i)).natAbs : ℤ) = b.height ((P.reflectionPerm j : (a : ι) → ι) i)

Tactic:
have : (b.height (P.reflectionPerm j i)).natAbs = b.height (P.reflectionPerm j i) :=
          Int.natAbs_of_nonneg <| (isPos_iff' _).mp 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
this_1 : b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i
this : (↑(b.height ((P.reflectionPerm j : (a : ι) → ι) i)).natAbs : ℤ) = b.height ((P.reflectionPerm j : (a : ι) → ι) i)
⊢ (b.height ((P.reflectionPerm j : (a : ι) → ι) i)).natAbs < 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
suffices : b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i
⊢ (b.height ((P.reflectionPerm j : (a : ι) → ι) i)).natAbs < n

Tactic:
suffices b.height (P.reflectionPerm j i) < b.height i by
        have : (b.height (P.reflectionPerm j i)).natAbs = b.height (P.reflectionPerm j i) :=
          Int.natAbs_of_nonneg <| (isPos_iff' _).mp hk
        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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
⊢ (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))

Tactic:
have := P.reflection_apply_root' ℤ (i := j) (j := i)
-- 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
this :
  (P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) i : M) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))

Tactic:
rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this

Premises used: neg_smul, sub_eq_add_neg, RootPairing.root_reflectionPerm
-- 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
inst_9 : P.IsReduced
p : ι → Prop
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
n : ℕ
ih : ∀ m < n, ∀ {i : ι} (h₀ : b.IsPos i) (hN : (b.height i).natAbs = m), p i
i : ι
h₀ : b.IsPos i
hN : (b.height i).natAbs = n
j : ι
hj : j ∈ b.support
hj' : 0 < P.pairingIn ℤ i j
hij : i ≠ j
hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)
this :
  (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul (β := M) (-P.pairingIn ℤ i j) ((P.root : (a : ι) → M) j : M))
rw : b.height i + -P.pairingIn ℤ i j • b.height j < b.height i
⊢ b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i

Tactic:
rw [b.height_add_zsmul this]

Premises used: RootPairing.Base.height_add_zsmul