awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₂ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₃ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₄ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₅ : (P.root' i : (a : N) → R) (-(P.coroot : (a : ι) → N) j : N) = -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₆ : -(P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- 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 : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₂ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₃ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₄ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₅ : (P.root' i : (a : N) → R) (-(P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₆ : -(P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₇ : -P.pairing i j = -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- 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_1 j i : ι
⊢ (P.reflectionPerm ((P.reflectionPerm i : (a : ι) → ι) i) : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) i : ι) = i
have a : Eq.{u_3 + 1} (α := M)
  ((P.root : (a : ι) → M)
      ((P.reflectionPerm ((P.reflectionPerm i : (a : ι) → ι) i) : (a : ι) → ι)
          ((P.reflectionPerm i : (a : ι) → ι) i : ι) :
        ι) :
    M)
  ((P.root : (a : ι) → M) i : 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_1 j i : ι
⊢ Eq.{u_3 + 1} (α := M)
    ((P.root : (a : ι) → M)
        ((P.reflectionPerm ((P.reflectionPerm i : (a : ι) → ι) i) : (a : ι) → ι)
            ((P.reflectionPerm i : (a : ι) → ι) i : ι) :
          ι) :
      M)
    ((P.root : (a : ι) → M) i : M)
have a : HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
        (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)))) -
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M) +
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))))) =
  (P.root : (a : ι) → M) i
Tactic: simp only [root_reflectionPerm, reflection_apply, LinearMap.flip_apply, root_coroot_eq_pairing,
      pairing_same, map_sub, coroot_reflectionPerm, coreflection_apply_self, map_neg, neg_smul,
      sub_neg_eq_add, map_smul, smul_add]
-- 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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
⊢ i ≠ -i
have this : IsReflexive R M
Tactic: have := Module.IsReflexive.of_isPerfPair P.toLinearMap
-- 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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
contra : i = -i
⊢ False
have contra₁ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)
Tactic: replace contra : P.root i = -P.root i := by simpa using congr_arg P.root contra
Cleared hypotheses: contra
-- 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.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M) ↔
    i = (P.reflectionPerm j : (a : ι) → ι) j
have refine : ∀ (h : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M)
Tactic: refine ⟨fun h ↦ P.root.injective ?_, fun h ↦ by simp [h]⟩
-- 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 : ι
h : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M)
have rw : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)
Tactic: rw [root_reflectionPerm, reflection_apply_self, h]
-- 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 : ι
h : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
rw :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)
rw₁ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M)
have rw₂ : Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) j : M)
Tactic: rw [root_reflectionPerm, reflection_apply_self, h]
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) ↔
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have refine : ∀ (h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x)
Tactic: refine ⟨this x, fun h ↦ ?_⟩
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x)
have h₁ : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (- -x)
Tactic: rw [← neg_neg x] at h
Cleared hypotheses: h
-- 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
x : M
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) ↔
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
have suffices : ∀ (x : M),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
Tactic: suffices ∀ x : M, -x ∈ range P.root → x ∈ range P.root by
    refine ⟨this x, fun h ↦ ?_⟩
    rw [← neg_neg x] at h
    exact this (-x) h
-- 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
x y : M
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-y) →
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y
have this : ∀ (i : ι) (hi : (P.root : (a : ι) → M) i = -y),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y
Tactic: ⟨i, hi⟩
-- 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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N) = (P.coroot : (a : ι) → N) i
have hij : t * P.pairing i j = 2
Tactic: have hij : t * P.pairing i j = 2 := by simpa using ((P.coroot' j).congr_arg h).symm
-- 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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
⊢ HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N) = (P.coroot : (a : ι) → N) i
have refine : MapsTo (α := N) (β := N)
  (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
  (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
Tactic: refine Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i)
    (finite_range P.coroot) (by simp [hij]) (by simp) (by simp [hij]) (by simp) ?_
    (P.mapsTo_coreflection_coroot i) (mem_range_self i)
-- 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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
⊢ MapsTo (α := N) (β := N)
    (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
have h₁ : Eq (α := N → N) (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
  (⇑(P.coreflection j) : (a : N) → N)
Tactic: convert! P.mapsTo_coreflection_coroot 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 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
⊢ Eq (α := N → N) (⇑(preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i)) : (a : N) → N)
    (⇑(P.coreflection j) : (a : N) → N)
have h₁ : ∀ (x : N),
  Eq (α := N)
    ((preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i) : (a : N) → N) x : N)
    ((P.coreflection j : (a : N) → N) x : N)
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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
x : N
⊢ P.root' j = t • P.root' i
have h₁ : ∀ (x : N), Eq.{u_2 + 1} (α := R) ((P.root' j : (a : N) → R) x : R) ((t • P.root' i : (a : N) → R) x : R)
Tactic: ext
-- 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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
x : N
⊢ Eq (α := N)
    ((preReflection (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) (P.root' i) : (a : N) → N) x : N)
    ((P.coreflection j : (a : N) → N) x : N)
have h₁ : P.root' j = t • P.root' i
Tactic: replace h : P.root' j = t • P.root' i := by ext; simp [h, root']
Cleared hypotheses: h
-- 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
r : M ≃ₗ[R] M
α : M
hr : r ∈ range P.reflection
hα : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) α
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (r • α)
have obtain : ∀ (i : ι), Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (P.reflection i • α)
Tactic: obtain ⟨i, rfl⟩ := hr
Cleared hypotheses: r, hr
-- 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
α : M
hα : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) α
i : ι
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (P.reflection i • α)
have obtain : ∀ (j : ι),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) (P.reflection i) ((P.root : (a : ι) → M) j : M))
Tactic: obtain ⟨j, rfl⟩ := hα
Cleared hypotheses: α, hα
-- 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
r : N ≃ₗ[R] N
α : N
hr : r ∈ range P.coreflection
hα : Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) α
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (r • α)
have obtain : ∀ (i : ι), Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (P.coreflection i • α)
Tactic: obtain ⟨i, rfl⟩ := hr
Cleared hypotheses: r, hr
-- 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
α : N
hα : Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) α
i : ι
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (P.coreflection i • α)
have obtain : ∀ (j : ι),
  Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (HSMul.hSMul (β := N) (P.coreflection i) ((P.coroot : (a : ι) → N) j : N))
Tactic: obtain ⟨j, rfl⟩ := hα
Cleared hypotheses: α, hα
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ HSMul.hSMul (β := M) (P.pairing k i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (P.pairing k j) ((P.root : (a : ι) → M) j : M)
have h : Eq (α := M) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)
  ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) k : M) : M)
Tactic: have h : P.reflection i (P.root k) = P.reflection j (P.root k) := by
    simp only [← root_reflectionPerm, hij]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ HSMul.hSMul (β := N) (P.pairing i k) ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (β := N) (P.pairing j k) ((P.coroot : (a : ι) → N) j : N)
have h : Eq (α := N) ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)
  ((P.coreflection j : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N)
Tactic: have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
    simp only [← coroot_reflectionPerm, hij]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
⊢ HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) =
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M)
have h : ∀ (x : M),
  HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) x =
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M) x
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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection i) : (a : M) → M) x =
    HSMul.hSMul (α := ℕ) (β := (a : M) → M) 2 (⇑(P.reflection j) : (a : M) → M) x
have h : HSMul.hSMul (α := ℕ) 2
    (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) i : N) : R)
      ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul (α := ℕ) 2
    (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))
Tactic: suffices
      2 • P.toLinearMap x (P.coroot i) • P.root i = 2 • P.toLinearMap x (P.coroot j) • P.root j by
    simpa [reflection_apply, smul_sub]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul (α := ℕ) 2
      (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) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul (α := ℕ) 2
      (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))
have h : HSMul.hSMul (α := ℕ) 2
    (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) i : N) : R)
      ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
Tactic: calc 2 • P.toLinearMap x (P.coroot i) • P.root i
      = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
    _ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
    _ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
    _ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
    _ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_