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
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))
⊢ 0 < b.height j

Tactic:
replace hj : 0 < b.height j := (isPos_iff _).mp <| isPos_of_mem_support 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' : 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))
hj : 0 < b.height j
⊢ b.height i + -P.pairingIn ℤ i j • b.height j < b.height i

Tactic:
aesop
-- 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)
⊢ (b.height ((P.reflectionPerm j : (a : ι) → ι) i)).natAbs < n

Tactic:
have : (b.height (P.reflectionPerm j i)).natAbs < n := by
      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
      have := P.reflection_apply_root' ℤ (i := j) (j := i)
      rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this
      rw [b.height_add_zsmul this]
      replace hj : 0 < b.height j := (isPos_iff _).mp <| isPos_of_mem_support hj
      aesop
-- 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)).natAbs < n
⊢ p i

Tactic:
simpa using h₂ (P.reflectionPerm j i) j
      (ih (m := (b.height (P.reflectionPerm j i)).natAbs) this hk rfl) hj

Premises used: RootPairing.Base.height, Int.natAbs, RootPairing.reflectionPerm, DFunLike.coe, rfl
-- 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
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)
N : ℕ
hN : (b.height i).natAbs = N
ind :
  ∀ (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), p i
⊢ p i

Tactic:
induction N using Nat.strongRecOn generalizing i with
  | ind 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
    have hk := h₀.reflectionPerm hj hij
    have : (b.height (P.reflectionPerm j i)).natAbs < n := by
      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
      have := P.reflection_apply_root' ℤ (i := j) (j := i)
      rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this
      rw [b.height_add_zsmul this]
      replace hj : 0 < b.height j := (isPos_iff _).mp <| isPos_of_mem_support hj
      aesop
    simpa using h₂ (P.reflectionPerm j i) j
      (ih (m := (b.height (P.reflectionPerm j i)).natAbs) this hk rfl) hj

Premises used: RootPairing.zero_lt_pairingIn_iff', RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn, 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
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
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
inst_9 : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
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
inst_9 : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos i
⊢ p i

Tactic:
hi.induction_on_reflect h₁ h₂

Premises used: RootPairing.Base.IsPos.induction_on_reflect
-- 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 : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos i
⊢ p i

Tactic:
exact hi.induction_on_reflect h₁ h₂

Premises used: RootPairing.Base.IsPos.induction_on_reflect
-- 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 : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
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
inst_9 : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
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
inst_9 : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
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
inst_9 : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
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
inst_9 : P.IsReduced
i : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
⊢ p (-i)

Tactic:
hi.induction_on_reflect h₁ h₂

Premises used: RootPairing.Base.IsPos.induction_on_reflect
-- 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 : ι
p : ι → Prop
h₀ : ∀ (i : ι), p i → p ((P.reflectionPerm i : (a : ι) → ι) i)
h₁ : ∀ i ∈ b.support, p i
h₂ : ∀ (i j : ι), p i → j ∈ b.support → p ((P.reflectionPerm j : (a : ι) → ι) i)
this : InvolutiveNeg ι := P.indexNeg
hi : b.IsPos (-i)
⊢ p (-i)

Tactic:
exact hi.induction_on_reflect h₁ h₂

Premises used: RootPairing.Base.IsPos.induction_on_reflect
-- 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
q : Submodule R M
⊢ (∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) ↔
    ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
⟨fun hq i ↦ ?_, fun hq i _ ↦ hq i⟩

Premises used: Iff.intro
-- 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
q : Submodule R M
refine :
  ∀ (hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) (i : ι),
    q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
⊢ (∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)) ↔
    ∀ (i : ι), q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
refine ⟨fun hq i ↦ ?_, fun hq i _ ↦ hq 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
this : InvolutiveNeg ι := P.indexNeg
j : ι
h : ∀ (x : M), Eq (α := M) ((P.reflection (-j) : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
⊢ P.reflection (-j) = P.reflection j

Tactic:
ext x
-- 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
this : InvolutiveNeg ι := P.indexNeg
j : ι
x : M
⊢ Eq (α := M) ((P.reflection (-j) : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)

Tactic:
simp [reflection_apply, two_smul]

Premises used: two_smul, RootPairing.reflection_apply
-- 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
this : InvolutiveNeg ι := P.indexNeg
⊢ ∀ (j : ι), P.reflection (-j) = P.reflection j

Tactic:
have (j : ι) : P.reflection (-j) = P.reflection j := by ext x; simp [reflection_apply, two_smul]
-- 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
⊢ ∀ (i : ι),
    q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M) →
      q ∈ invtSubmodule (↑(P.reflection ((P.reflectionPerm i : (a : ι) → ι) i)) : M →ₗ[R] M)

Tactic:
simp_all
-- 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
i : ι
this_1 : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
refine :
  ∀ (i j : ι),
    q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M) →
      j ∈ b.support → q ∈ invtSubmodule (↑(P.reflection ((P.reflectionPerm j : (a : ι) → ι) i)) : M →ₗ[R] M)
⊢ q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
refine b.induction_reflect i (by simp_all) hq ?_

Premises used: RootPairing.Base.induction_reflect
-- 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
this_1 : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
i j : ι
hi : q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
hj : j ∈ b.support
rw : q ∈ invtSubmodule (↑(P.reflection j * P.reflection i * P.reflection j) : M →ₗ[R] M)
⊢ q ∈ invtSubmodule (↑(P.reflection ((P.reflectionPerm j : (a : ι) → ι) i)) : M →ₗ[R] M)

Tactic:
rw [reflection_reflectionPerm]

Premises used: RootPairing.reflection_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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
this_1 : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
i j : ι
hi : q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
hj : j ∈ b.support
⊢ q ∈ invtSubmodule (↑(P.reflection j * P.reflection i * P.reflection j) : M →ₗ[R] M)

Tactic:
Module.End.invtSubmodule.comp _ (Module.End.invtSubmodule.comp _ (hq j hj) hi) (hq j hj)

Premises used: Set.Mem, setOf, Module.End.invtSubmodule.comp
-- 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
q : Submodule R M
hq : ∀ i ∈ b.support, q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
this_1 : InvolutiveNeg ι := P.indexNeg
this : ∀ (j : ι), P.reflection (-j) = P.reflection j
i j : ι
hi : q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
hj : j ∈ b.support
⊢ q ∈ invtSubmodule (↑(P.reflection j * P.reflection i * P.reflection j) : M →ₗ[R] M)

Tactic:
exact Module.End.invtSubmodule.comp _ (Module.End.invtSubmodule.comp _ (hq j hj) hi) (hq j hj)

Premises used: Module.End.invtSubmodule.comp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsRootSystem
⊢ P.IsPerfectCompl (P.rootSpan R) (P.corootSpan R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
⊢ P.IsPerfectCompl
    (span L
      (↑(LinearMap.range (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
            (Submodule.subtype (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))) :
        Set M))
    (span L
      (↑(LinearMap.range (M := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
            (Submodule.subtype (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))) :
        Set N))

Tactic:
simpa using IsBalanced.isPerfectCompl

Premises used: RootPairing.IsBalanced.isPerfectCompl
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i j : ι
h :
  Eq.{u_3 + 1} (α := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((fun (i : ι) ↦
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
            ((P.root : (a : ι) → M) i) ⋯ :
          ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))))
      i)
    ((fun (i : ι) ↦
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
            ((P.root : (a : ι) → M) i) ⋯ :
          ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))))
      j)
⊢ i = j

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i j : ι
h :
  Eq.{u_4 + 1} (α := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    ((fun (i : ι) ↦
        (Subtype.mk (p := fun (x : N) ↦
            Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
            ((P.coroot : (a : ι) → N) i) ⋯ :
          ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))))
      i)
    ((fun (i : ι) ↦
        (Subtype.mk (p := fun (x : N) ↦
            Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
            ((P.coroot : (a : ι) → N) i) ⋯ :
          ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))))
      j)
⊢ i = j

Tactic:
simpa using h