awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
hk :
  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
    ((preReflection α ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : (a : M) → M) β : M)
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) α) : End R N) : (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
have set : let α' : N := (coroot : (a : ι) → N) i;
∀
  (hk :
    Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
      ((preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α') : (a : M) → M) β : M)),
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) ((coroot : (a : ι) → N) j : N) : N)
Tactic: set α' := coroot i
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
⊢ preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
have h : ∀ (x : M),
  Eq (α := M)
    (((preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) : End R M) :
          (a : M) → M)
        x :
      M)
    ((sα ∘ₗ sβ ∘ₗ sα : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
x : M
⊢ Eq (α := M)
    (((preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) : End R M) :
          (a : M) → M)
        x :
      M)
    ((sα ∘ₗ sβ ∘ₗ sα : (a : M) → M) x : M)
have hpi : Eq.{u_2 + 1} (α := R)
  ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
      ((root : (a : ι) → M) i : M) :
    R)
  (2 : R)
Tactic: have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β' : N)
have hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
Tactic: have hij : preReflection (sα β) (p.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα := by
    ext
    have hpi : (p.flip (coroot i)) (root i) = 2 := by simp [hp i]
    simp [α, β, α', β', sα, sβ, sα', ← preReflection_preReflection β (p.flip β') hpi,
      preReflection_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β' : N)
have a : Eq (α := Dual R M) ((p.flip.toPerfPair : (a : N) → Dual R M) ((coroot : (a : ι) → N) k) : Dual R M)
  ((p.flip.toPerfPair : (a : N) → Dual R M) ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β') :
    Dual R M)
Tactic: apply p.flip.toPerfPair.injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ Eq (α := Dual R M) ((p.flip.toPerfPair : (a : N) → Dual R M) ((coroot : (a : ι) → N) k) : Dual R M)
    ((p.flip.toPerfPair : (a : N) → Dual R M) ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β') :
      Dual R M)
have a : Eq.{u_2 + 1} (α := R)
  ((((p.flip.toPerfPair : (a : N) → Dual R M) ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β') :
          Dual R M) :
        (a : M) → R)
      ((root : (a : ι) → M) k : M) :
    R)
  (2 : R)
Tactic: apply Dual.eq_of_preReflection_mapsTo (finite_range root) hsp (hp k) (hs k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
a :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip.toPerfPair : (a : N) → Dual R M) ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β') :
            Dual R M) :
          (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
⊢ Eq (α := Dual R M) ((p.flip.toPerfPair : (a : N) → Dual R M) ((coroot : (a : ι) → N) k) : Dual R M)
    ((p.flip.toPerfPair : (a : N) → Dual R M) ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β') :
      Dual R M)
have a₁ : MapsTo.{u_3, u_3} (α := M) (β := M)
  (⇑(preReflection ((root : (a : ι) → M) k)
          ((p.flip.toPerfPair : (a : N) → Dual R M)
            ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β')) :
        End R M) :
    (a : M) → M)
  (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
Tactic: apply Dual.eq_of_preReflection_mapsTo (finite_range root) hsp (hp k) (hs k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ Eq.{u_2 + 1} (α := R)
    ((((p.flip.toPerfPair : (a : N) → Dual R M) ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β') :
            Dual R M) :
          (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
have a : 2 -
      HMul.hMul (α := R) (β := R)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) i : N) :
          R)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) j : N) :
          R) -
    HMul.hMul (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (HSub.hSub (α := R)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) j : N) :
          R)
        (HMul.hMul (α := R) (β := R) (2 : R)
          ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
              ((coroot : (a : ι) → N) j : N) :
            R))) =
  2
Tactic: simp [map_sub, α, β, α', β', sα, hk, preReflection_apply, hp i, hp j,
      mul_comm (p α β')]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
p : M →ₗ[R] N →ₗ[R] R
inst_9 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j k : ι
α : M := (root : (a : ι) → M) i
β : M := (root : (a : ι) → M) j
α' : N := (coroot : (a : ι) → N) i
β' : N := (coroot : (a : ι) → N) j
sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α')
hk : Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)
sβ : End R M := preReflection β ((p.flip : (a : N) → M →ₗ[R] R) β')
sα' : End R N := preReflection α' ((p : (a : M) → N →ₗ[R] R) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
⊢ MapsTo.{u_3, u_3} (α := M) (β := M)
    (⇑(preReflection ((root : (a : ι) → M) k)
            ((p.flip.toPerfPair : (a : N) → Dual R M)
              ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β')) :
          End R M) :
      (a : M) → M)
    (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
have a : MapsTo (α := M) (β := M) (⇑(sα ∘ₗ sβ ∘ₗ sα) : (a : M) → M) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
  (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
Tactic: rw [hk, LinearMap.toLinearMap_toPerfPair, hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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 : P.IsRootSystem
k : Type u_5
inst_7 : Field k
inst_8 : CharZero k
inst_9 : Module k M
inst_10 : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst_11 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := k)
      ((((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i) : N →ₗ[k] k) : (a : N) → k) ((coroot : (a : ι) → N) i : N) :
        k)
      (2 : k)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[k] k) ((coroot : (a : ι) → N) i)) : End k M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule k M) (span k (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j : ι
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i)) : End k N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
have h : Eq (α := N) ((coroot : (a : ι) → N) sorry : N)
  (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i)) : End k N) :
        (a : N) → N)
      ((coroot : (a : ι) → N) j : N) :
    N)
Tactic: use RootPairing.equiv_of_mapsTo p root coroot i hs hp j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (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 : P.IsRootSystem
k : Type u_5
inst_7 : Field k
inst_8 : CharZero k
inst_9 : Module k M
inst_10 : Module k N
p : M →ₗ[k] N →ₗ[k] k
inst_11 : p.IsPerfPair
root : ι ↪ M
coroot : ι ↪ N
hp :
  ∀ (i : ι),
    Eq.{u_5 + 1} (α := k)
      ((((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i) : N →ₗ[k] k) : (a : N) → k) ((coroot : (a : ι) → N) i : N) :
        k)
      (2 : k)
hs :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[k] k) ((coroot : (a : ι) → N) i)) : End k M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hsp : Eq.{u_3 + 1} (α := Submodule k M) (span k (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))) ⊤
i j : ι
⊢ Eq (α := N) ((coroot : (a : ι) → N) sorry : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[k] k) ((root : (a : ι) → M) i)) : End k N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
have h : Eq (α := M) ((root : (a : ι) → M) sorry : M)
  (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[k] k) ((coroot : (a : ι) → N) i)) : End k M) :
        (a : M) → M)
      ((root : (a : ι) → M) j : M) :
    M)
Tactic: refine (coroot_eq_coreflection_of_root_eq_of_span_eq_top p root coroot hp hs hsp ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.CartanMatrix (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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsValuedIn S
B : P.InvariantForm
b : P.Base
inst_9 : DecidableEq ι
⊢ HMul.hMul (α := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R)
      ((cartanMatrixIn S b).map (⇑(algebraMap S R) : (a : S) → R))
      (Matrix.diagonal fun (i : ↥b.support) ↦
        (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑i : ι)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (↑i : ι) : M)) =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) 2
      ((LinearMap.BilinForm.toMatrix b.toWeightBasis :
            (a : LinearMap.BilinForm R M) → Matrix (↥b.support) (↥b.support) R)
          B.form :
        Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R)
have a : ∀ (i j : ↥b.support),
  HMul.hMul (α := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) (β :=
      Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) ((cartanMatrixIn S b).map (⇑(algebraMap S R) : (a : S) → R))
      (Matrix.diagonal fun (i : ↥b.support) ↦
        (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) (↑i : ι)) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) (↑i : ι) : M))
      i j =
    HSMul.hSMul (α := R) (β := Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R) 2
      ((LinearMap.BilinForm.toMatrix b.toWeightBasis :
            (a : LinearMap.BilinForm R M) → Matrix (↥b.support) (↥b.support) R)
          B.form :
        Matrix.{u_1, u_1, u_2} (↥b.support) (↥b.support) R)
      i j
Tactic: ext