awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
⊢ P₁.coroot = P₂.coroot
have this : IsAddTorsionFree M
Tactic: have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
⊢ P₁.coroot = P₂.coroot
have h : ∀ (i : ι), Eq.{u_4 + 1} (α := N) ((P₁.coroot : (a : ι) → N) i : N) ((P₂.coroot : (a : ι) → N) i : N)
Tactic: ext i
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
⊢ Eq.{u_4 + 1} (α := N) ((P₁.coroot : (a : ι) → N) i : N) ((P₂.coroot : (a : ι) → N) i : N)
have h : Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
  ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) ∘ₗ P₁.flip :
        (a : N) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
      ((P₁.coroot : (a : ι) → N) i) :
    Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
  ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) ∘ₗ P₁.flip :
        (a : N) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
      ((P₂.coroot : (a : ι) → N) i) :
    Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
Tactic: apply P₁.injOn_dualMap_subtype_span_root_coroot (mem_range_self i) (hc ▸ mem_range_self i)
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
⊢ Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
have h : Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
  (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))) ((P₁.root : (a : ι) → M) i : M)
Tactic: apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
h :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))) ((P₁.root : (a : ι) → M) i : M)
⊢ Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
have h₁ : Eq.{u_2 + 1} (α := R)
  ((((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
      ((P₁.root : (a : ι) → M) i : M) :
    R)
  (2 : R)
Tactic: apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
h :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))) ((P₁.root : (a : ι) → M) i : M)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
        ((P₁.root : (a : ι) → M) i : M) :
      R)
    (2 : R)
⊢ Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
have h₂ : MapsTo.{u_3, u_3} (α := M) (β := M)
  (⇑(preReflection ((P₁.root : (a : ι) → M) i) ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
        End R M) :
    (a : M) → M)
  (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))
Tactic: apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
h :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))) ((P₁.root : (a : ι) → M) i : M)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
        ((P₁.root : (a : ι) → M) i : M) :
      R)
    (2 : R)
h₂ :
  MapsTo.{u_3, u_3} (α := M) (β := M)
    (⇑(preReflection ((P₁.root : (a : ι) → M) i) ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
          End R M) :
      (a : M) → M)
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))
⊢ Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
have h₃ : Eq.{u_2 + 1} (α := R)
  ((((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
      ((P₁.root : (a : ι) → M) i : M) :
    R)
  (2 : R)
Tactic: apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
h :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))) ((P₁.root : (a : ι) → M) i : M)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
        ((P₁.root : (a : ι) → M) i : M) :
      R)
    (2 : R)
h₂ :
  MapsTo.{u_3, u_3} (α := M) (β := M)
    (⇑(preReflection ((P₁.root : (a : ι) → M) i) ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
          End R M) :
      (a : M) → M)
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))
h₃ :
  Eq.{u_2 + 1} (α := R)
    ((((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
        ((P₁.root : (a : ι) → M) i : M) :
      R)
    (2 : R)
⊢ Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
have h₄ : MapsTo.{u_3, u_3} (α := M) (β := M)
  (⇑(preReflection ((P₁.root : (a : ι) → M) i) ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
        End R M) :
    (a : M) → M)
  (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))
Tactic: apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
-- 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₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
i : ι
h :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))) ((P₁.root : (a : ι) → M) i : M)
h₁ :
  Eq.{u_2 + 1} (α := R)
    ((((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
        ((P₁.root : (a : ι) → M) i : M) :
      R)
    (2 : R)
h₂ :
  MapsTo.{u_3, u_3} (α := M) (β := M)
    (⇑(preReflection ((P₁.root : (a : ι) → M) i) ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
          End R M) :
      (a : M) → M)
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))
h₃ :
  Eq.{u_2 + 1} (α := R)
    ((((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i) : Dual R M) : (a : M) → R)
        ((P₁.root : (a : ι) → M) i : M) :
      R)
    (2 : R)
h₄ :
  MapsTo.{u_3, u_3} (α := M) (β := M)
    (⇑(preReflection ((P₁.root : (a : ι) → M) i) ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
          End R M) :
      (a : M) → M)
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))
⊢ Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₁.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑P₁.root : (a : ι) → M))))
        ((P₁.flip : (a : N) → Dual R M) ((P₂.coroot : (a : ι) → N) i)) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P₁.root : (a : ι) → M))))
have apply : M
Tactic: apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
-- 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)
hr :
  ∀ (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))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
i j k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
    (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
          (a : M) → M)
        ((root : (a : ι) → M) j : M) :
      M)
⊢ Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    (((preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
          (a : N) → N)
        ((coroot : (a : ι) → N) j : N) :
      N)
have set : let α : M := (root : (a : ι) → M) i;
∀
  (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)
          ((root : (a : ι) → M) j : 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)
Tactic: set α := root 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)
hr :
  ∀ (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))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
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)
hr :
  ∀ (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))
hc :
  ∀ (i : ι),
    MapsTo.{u_4, u_4} (α := N) (β := N)
      (⇑(preReflection ((coroot : (a : ι) → N) i) ((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i)) : End R N) :
        (a : N) → N)
      (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N)) (range.{u_4, u_1 + 1} (ι := ι) (⇑coroot : (a : ι) → N))
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