awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
have h₁ : LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
  (![(P.root : (a : ι) → M) i,
      (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
    Fin (Nat.succ 0).succ → M)
Tactic: replace h : LinearIndependent R ![P.root i, P.root (P.chainTopIdx i j)] := by
    rwa [P.root_chainTopIdx, add_comm (P.root j), ← natCast_zsmul,
      LinearIndependent.pair_add_smul_right_iff]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
⊢ HSub.hSub (α := ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
have rw : P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i =
  P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
Tactic: rw [P.chainBotCoeff_sub_chainTopCoeff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
⊢ HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
have calc : HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
  (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
    ℤ)
Tactic: calc (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
    _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
    _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
    _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
calc :
  HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
have calc₁ : (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
        (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
    ℤ) =
  HSub.hSub (α := ℤ)
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ)
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ)
Tactic: calc (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
    _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
    _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
    _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
calc :
  HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ)
calc₁ :
  (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ) =
    HSub.hSub (α := ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
⊢ HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
have calc₂ : HSub.hSub (α := ℤ)
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ)
    (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ) =
  P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
Tactic: calc (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
    _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
    _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
    _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3
have pos : ∀
  (h :
    LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
pos :
  ∀
    (h :
      LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
      3
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3
have neg : ∀
  (h :
    ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
        (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)),
  chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3
Tactic: by_cases h : LinearIndependent R ![P.root i, P.root j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3
have pos : P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i ≤ 3
Tactic: rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat,
    chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Chain (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i ≤ 3
have this : Membership.mem (γ := Set (ℤ × ℤ))
  {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}
  (P.pairingIn ℤ i (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j),
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i)
Tactic: have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i (P.chainTopIdx i j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
inst_5 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
⊢ ∃ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)
have obtain : ∀ (i : ι), ∃ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)
Tactic: obtain ⟨i⟩ := (inferInstance : Nonempty ι)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
inst_5 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
⊢ Nontrivial M
have obtain : ∀ (i : ι) (hi : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)), Nontrivial M
Tactic: obtain ⟨i, hi⟩ := P.exists_ne_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i : ι
⊢ HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 = 1
have H : ∀ (j : ι), Eq (α := ι) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) ((1 : (a : ι) → ι) j : ι)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
⊢ Eq (α := ι) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) ((1 : (a : ι) → ι) j : ι)
have H : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) : M)
  ((P.root : (a : ι) → M) ((1 : (a : ι) → ι) j : ι) : M)
Tactic: apply P.root.injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
⊢ (P.reflectionPerm i : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) j : ι) = j
have a : Eq.{u_3 + 1} (α := M)
  ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : ι) : M)
  ((P.root : (a : ι) → M) j : M)
Tactic: apply P.root.injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i : ι
⊢ Eq (α := ι → ι) (⇑(P.reflectionPerm i) : (a : ι) → ι)^[2] id
have h : ∀ (x : ι), (⇑(P.reflectionPerm i) : (a : ι) → ι)^[2] x = id x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
⊢ P.reflection ((P.reflectionPerm j : (a : ι) → ι) i) = P.reflection j * P.reflection i * P.reflection j
have h : ∀ (x : M),
  Eq (α := M) ((P.reflection ((P.reflectionPerm j : (a : ι) → ι) i) : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i * P.reflection j : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
x : M
⊢ Eq (α := M) ((P.reflection ((P.reflectionPerm j : (a : ι) → ι) i) : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i * P.reflection j : (a : M) → M) x : M)
have h : x -
    HSub.hSub (α := R)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        (HMul.hMul (β := R) (P.pairing j i)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
            R)) •
      HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
        (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
  x -
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
          ((P.root : (a : ι) → M) j : M) -
      HSMul.hSMul (β := M)
        (HSub.hSub (α := R)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
          (HMul.hMul (α := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
            (P.pairing j i)))
        ((P.root : (a : ι) → M) i : M) -
    HSMul.hSMul (β := M)
      (HSub.hSub (α := R)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
          (HMul.hMul (α := R) (β := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
            (2 : R)) -
        HSub.hSub (α := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
            (HMul.hMul (α := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
                R)
              (P.pairing j i)) *
          P.pairing i j)
      ((P.root : (a : ι) → M) j : M)
Tactic: simp [reflection_apply, coreflection_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i : ι
⊢ (↑(P.reflection i).dualMap : Dual R M →ₗ[R] Dual R M) ∘ₗ P.flip = P.flip ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N)
have h : ∀ (n : N) (m : M),
  Eq.{u_2 + 1} (α := R)
    (((((↑(P.reflection i).dualMap : Dual R M →ₗ[R] Dual R M) ∘ₗ P.flip : (a : N) → M →ₗ[R] R) n : M →ₗ[R] R) :
          (a : M) → R)
        m :
      R)
    ((((P.flip ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) m : R)
Tactic: ext n m
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)
have hk₁ : k = (P.reflectionPerm i : (a : ι) → ι) j
Tactic: rw [← P.root_reflectionPerm, EmbeddingLike.apply_eq_iff_eq] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j k : ι
hk : k = (P.reflectionPerm i : (a : ι) → ι) j
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)
have rw : Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
  ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
Tactic: rw [← P.coroot_reflectionPerm, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j k : ι
hk : k = (P.reflectionPerm i : (a : ι) → ι) j
rw :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
    ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)
have rw₁ : Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
  ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
Tactic: rw [← P.coroot_reflectionPerm, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
⊢ P.coroot' ((P.reflectionPerm i : (a : ι) → ι) j) = P.coroot' j ∘ₗ (↑(P.reflection i) : M →ₗ[R] M)
have h : ∀ (y : M),
  Eq.{u_2 + 1} (α := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) j) : (a : M) → R) y : R)
    ((P.coroot' j ∘ₗ (↑(P.reflection i) : M →ₗ[R] M) : (a : M) → R) y : R)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j k : ι
⊢ P.pairing j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairing ((P.reflectionPerm i : (a : ι) → ι) j) k
have simp : Eq.{u_2 + 1} (α := R)
  ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
      ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N) :
    R)
  ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) k : N) :
    R)
Tactic: simp only [pairing, root', coroot_reflectionPerm, root_reflectionPerm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i : ι
⊢ (P.toPerfPair.conj : (a : End R M) → End R (Dual R N)) (↑(P.reflection i) : M →ₗ[R] M) =
    (↑(P.coreflection i) : N →ₗ[R] N).dualMap
have h : ∀ (f : Dual R N) (n : N),
  Eq.{u_2 + 1} (α := R)
    ((((((P.toPerfPair.conj : (a : End R M) → End R (Dual R N)) (↑(P.reflection i) : M →ₗ[R] M) : End R (Dual R N)) :
                (a : Dual R N) → Dual R N)
              f :
            Dual R N) :
          (a : N) → R)
        n :
      R)
    (((((↑(P.coreflection i) : N →ₗ[R] N).dualMap : (a : Dual R N) → Dual R N) f : Dual R N) : (a : N) → R) n : R)
Tactic: ext f n