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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
have h₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
      R)
    ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
      R)
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [← P.pairing_smul_coroot_eq j i j hij.symm, pairing_same]
-- 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.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : 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 (β := M)
    (HSMul.hSMul (α := R) (β := R) 2
      ((((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 (α := ℕ) 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: rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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
h :
  HSMul.hSMul (β := M)
      (HSMul.hSMul (α := R) (β := R) 2
        ((((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 (α := ℕ) 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))
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : 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.{u_2, u_3, u_3} (α := R) 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)) =
  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: rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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
h :
  HSMul.hSMul (β := M)
      (HSMul.hSMul (α := R) (β := R) 2
        ((((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 (α := ℕ) 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))
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 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)) =
    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))
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : 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.{u_2, u_3, u_3} (α := R) 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)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (↑2 : R)
    (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: rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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
h :
  HSMul.hSMul (β := M)
      (HSMul.hSMul (α := R) (β := R) 2
        ((((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 (α := ℕ) 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))
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 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)) =
    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))
h₂ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 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)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (↑2 : R)
      (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.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : 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.{u_2, u_3, u_3} (α := R) 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)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) 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: rw [map_smul, smul_assoc, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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 : ι
h2 : IsSMulRegular (R := ℕ) M 2
⊢ P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j
have refine : ∀ (h : P.reflectionPerm i = P.reflectionPerm j), P.reflection i = P.reflection j
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| 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 : ι
h2 : IsSMulRegular (R := ℕ) M 2
h : P.reflectionPerm i = P.reflectionPerm j
⊢ P.reflection i = P.reflection j
have suffices : Eq (α := (a : M) → M) (⇑(P.reflection i) : (a : M) → M) (⇑(P.reflection j) : (a : M) → M)
Tactic: suffices ⇑(P.reflection i) = ⇑(P.reflection j) from DFunLike.coe_injective this
-- 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 : ι
h2 : IsSMulRegular (R := ℕ) M 2
h : P.reflectionPerm i = P.reflectionPerm j
⊢ Eq (α := (a : M) → M) (⇑(P.reflection i) : (a : M) → M) (⇑(P.reflection j) : (a : M) → M)
have h2₁ : IsSMulRegular.{0, u_3} (R := ℕ) (M → M) 2
Tactic: replace h2 : IsSMulRegular (M → M) 2 := IsSMulRegular.pi fun _ ↦ h2
Cleared hypotheses: h2
-- 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 = P.reflectionPerm j ↔
    ∀ (x : M),
      Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
        Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_1 : ∀ (h : P.reflectionPerm i = P.reflectionPerm j) (x : M)
  (hx : Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x),
  Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
Tactic: refine ⟨fun h x hx ↦ ?_, fun 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 : ι
refine_1 :
  ∀ (h : P.reflectionPerm i = P.reflectionPerm j) (x : M)
    (hx : Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x),
    Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
⊢ P.reflectionPerm i = P.reflectionPerm j ↔
    ∀ (x : M),
      Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
        Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_2 : ∀
  (h :
    ∀ (x : M),
      Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
        Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)),
  P.reflectionPerm i = P.reflectionPerm j
Tactic: refine ⟨fun h x hx ↦ ?_, fun 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 : P.reflectionPerm i = P.reflectionPerm j
x_1 x : M
hx : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_1 : ∀ (k : ι),
  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: obtain ⟨k, rfl⟩ := hx
Cleared hypotheses: x, hx
-- 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 : P.reflectionPerm i = P.reflectionPerm j
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_1 : ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
  Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
Tactic: induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨k, rfl⟩ := hx
      simp only [← root_reflectionPerm, h]
    | zero => simp
    | add x y _ _ hx hy => simp [hx, hy]
    | smul t x _ hx => simp [hx]
Cleared hypotheses: hx
-- 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 : P.reflectionPerm i = P.reflectionPerm j
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_1₁ : Eq (α := M) ((P.reflection i : (a : M) → M) 0 : M) ((P.reflection j : (a : M) → M) 0 : M)
Tactic: induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨k, rfl⟩ := hx
      simp only [← root_reflectionPerm, h]
    | zero => simp
    | add x y _ _ hx hy => simp [hx, hy]
    | smul t x _ hx => simp [hx]
Cleared hypotheses: hx
-- 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 : P.reflectionPerm i = P.reflectionPerm j
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
refine_1₁ : Eq (α := M) ((P.reflection i : (a : M) → M) 0 : M) ((P.reflection j : (a : M) → M) 0 : M)
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_1₂ : ∀ (x y : M),
  Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
    Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y →
      ∀ (hx : Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M))
        (hy : Eq (α := M) ((P.reflection i : (a : M) → M) y : M) ((P.reflection j : (a : M) → M) y : M)),
        Eq (α := M) ((P.reflection i : (a : M) → M) (x + y) : M) ((P.reflection j : (a : M) → M) (x + y) : M)
Tactic: induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨k, rfl⟩ := hx
      simp only [← root_reflectionPerm, h]
    | zero => simp
    | add x y _ _ hx hy => simp [hx, hy]
    | smul t x _ hx => simp [hx]
Cleared hypotheses: hx
-- 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 : P.reflectionPerm i = P.reflectionPerm j
x : M
hx : Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
refine_1 :
  ∀ (x : M) (hx : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
refine_1₁ : Eq (α := M) ((P.reflection i : (a : M) → M) 0 : M) ((P.reflection j : (a : M) → M) 0 : M)
refine_1₂ :
  ∀ (x y : M),
    Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
      Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y →
        ∀ (hx : Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M))
          (hy : Eq (α := M) ((P.reflection i : (a : M) → M) y : M) ((P.reflection j : (a : M) → M) y : M)),
          Eq (α := M) ((P.reflection i : (a : M) → M) (x + y) : M) ((P.reflection j : (a : M) → M) (x + y) : M)
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
have refine_1₃ : ∀ (t : R) (x : M),
  Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
    ∀ (hx : Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)),
      Eq (α := M) ((P.reflection i : (a : M) → M) (t • x) : M) ((P.reflection j : (a : M) → M) (t • x) : M)
Tactic: induction hx using Submodule.span_induction with
    | mem x hx =>
      obtain ⟨k, rfl⟩ := hx
      simp only [← root_reflectionPerm, h]
    | zero => simp
    | add x y _ _ hx hy => simp [hx, hy]
    | smul t x _ hx => simp [hx]
Cleared hypotheses: hx
-- 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 :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
      Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
⊢ P.reflectionPerm i = P.reflectionPerm j
have refine_2 : ∀ (k : ι), Eq (α := ι) ((P.reflectionPerm i : (a : ι) → ι) k : ι) ((P.reflectionPerm j : (a : ι) → ι) k : ι)
Tactic: ext k
-- 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 :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x →
      Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((P.reflection j : (a : M) → M) x : M)
k : ι
⊢ Eq (α := ι) ((P.reflectionPerm i : (a : ι) → ι) k : ι) ((P.reflectionPerm j : (a : ι) → ι) k : ι)
have refine_2 : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) k : ι) : M)
  ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) k : ι) : 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
inst_5 : P.IsRootSystem
i j : ι
⊢ P.reflectionPerm i = P.reflectionPerm j ↔ P.reflection i = P.reflection j
have refine : ∀ (h : P.reflectionPerm i = P.reflectionPerm j), P.reflection i = P.reflection j
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| 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
inst_5 : P.IsRootSystem
i j : ι
h : P.reflectionPerm i = P.reflectionPerm j
⊢ P.reflection i = P.reflection j
have h₁ : ∀ (x : M), Eq (α := M) ((P.reflection i : (a : M) → M) x : M) ((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 : ι
h : P.IsOrthogonal i j
⊢ P.reflection i * P.reflection j = P.reflection j * P.reflection i
have h₁ : ∀ (x : M),
  Eq (α := M) ((P.reflection i * P.reflection j : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i : (a : M) → M) x : M)
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
i j : ι
h : P.IsOrthogonal i j
x : M
⊢ Eq (α := M) ((P.reflection i * P.reflection j : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i : (a : M) → M) x : M)
have h₁ : P.pairing i j = 0 ∧ P.pairing j i = 0
Tactic: replace h : P.pairing i j = 0 ∧ P.pairing j i = 0 := by simpa [IsOrthogonal] using h
Cleared hypotheses: h