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 : 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)
⊢ p i
have generalize : ∀ (N_1 : ℕ) (hN : (b.height i).natAbs = N_1), p i
Tactic: generalize hN : (b.height i).natAbs = 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
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
⊢ p i
have ind : ∀ (j : ι) (hj : j ∈ b.support) (hj' : 0 < P.pairingIn ℤ j i), p i
Tactic: obtain ⟨j, hj, hj'⟩ := h₀.exists_mem_support_pos_pairingIn
-- 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
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
⊢ p i
have hj'₁ : 0 < P.pairingIn ℤ i j
Tactic: rw [P.zero_lt_pairingIn_iff'] at hj'
Cleared hypotheses: hj'
-- 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
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
⊢ p i
have ind : ∀ (hj : i ∈ b.support) (hj' : 0 < P.pairingIn ℤ i i), p i
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j, hj, hj'
-- 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
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
⊢ p i
have ind₁ : ∀ (hij : i ≠ j), p i
Tactic: rcases eq_or_ne i j with rfl | hij
-- 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
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
⊢ p i
have ind : ∀ (hk : b.IsPos ((P.reflectionPerm j : (a : ι) → ι) i)), p i
Tactic: have hk := h₀.reflectionPerm hj hij
-- 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
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 < n
have this₁ : (↑(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
-- 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
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
have suffices : b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i
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
-- 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
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) < b.height i
have 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))
Tactic: have := P.reflection_apply_root' ℤ (i := j) (j := i)
-- 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
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))
⊢ b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i
have 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))
Tactic: rw [← root_reflectionPerm, sub_eq_add_neg, ← neg_smul] at this
Cleared hypotheses: this
-- 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
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))
⊢ b.height ((P.reflectionPerm j : (a : ι) → ι) i) < b.height i
have rw : b.height i + -P.pairingIn ℤ i j • b.height j < b.height i
Tactic: rw [b.height_add_zsmul this]
-- 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
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))
⊢ b.height i + -P.pairingIn ℤ i j • b.height j < b.height i
have hj₁ : 0 < b.height j
Tactic: replace hj : 0 < b.height j := (isPos_iff _).mp <| isPos_of_mem_support hj
Cleared hypotheses: hj
-- 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
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 i
have this : (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
-- 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
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
⊢ p i
have 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
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
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
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
⊢ 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
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
⊢ 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
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
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
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
have inr : p (-i)
Tactic: suffices p (-i) by rw [← neg_neg i]; exact h₀ (-i) this
-- 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
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)
have refine : ∀ (hq : ∀ 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⟩
-- 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
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
have h : ∀ (x : M), Eq (α := M) ((P.reflection (-j) : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
Tactic: ext x
-- 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
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
⊢ q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
have this₁ : ∀ (j : ι), P.reflection (-j) = P.reflection j
Tactic: have (j : ι) : P.reflection (-j) = P.reflection j := by ext x; simp [reflection_apply, two_smul]
-- 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
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
⊢ q ∈ invtSubmodule (↑(P.reflection i) : M →ₗ[R] M)
have 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)
Tactic: refine b.induction_reflect i (by simp_all) hq ?_
-- 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
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 ((P.reflectionPerm j : (a : ι) → ι) i)) : M →ₗ[R] M)
have rw : q ∈ invtSubmodule (↑(P.reflection j * P.reflection i * P.reflection j) : M →ₗ[R] M)
Tactic: rw [reflection_reflectionPerm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
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 : ι
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)
have rw : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) (2 : L)
Tactic: rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
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 : ι
rw : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) (2 : L)
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)
have rw₁ : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) ((↑2 : L) : L)
Tactic: rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseChange (goal)
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 : ι
rw : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) (2 : L)
rw₁ : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) ((↑2 : L) : L)
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)
have rw₂ : Eq.{u_2 + 1} (α := L) (↑2 : L) (↑2 : L)
Tactic: rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]