awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 :
  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))))
⊢ Eq.{u_4 + 1} (α := N) ((P₁.coroot : (a : ι) → N) i : N) ((P₂.coroot : (a : ι) → N) i : N)

Tactic:
apply P₁.injOn_dualMap_subtype_span_root_coroot (mem_range_self i) (hc ▸ mem_range_self i)

Premises used: Set.mem_range_self, RootPairing.injOn_dualMap_subtype_span_root_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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))
apply : 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))))

Tactic:
apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)

Premises used: Set.finite_range, RootPairing.root, Module.Dual.eq_of_preReflection_mapsTo', DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : ι
⊢ 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:
Submodule.subset_span (mem_range_self i)

Premises used: Set.mem_range_self, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : ι
⊢ 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:
exact Submodule.subset_span (mem_range_self i)

Premises used: Set.mem_range_self, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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_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:
P₁.coroot_root_two i

Premises used: RootPairing.coroot_root_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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_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:
exact P₁.coroot_root_two i

Premises used: RootPairing.coroot_root_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : ι
⊢ 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:
P₁.mapsTo_reflection_root i

Premises used: RootPairing.mapsTo_reflection_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : ι
⊢ 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:
exact P₁.mapsTo_reflection_root i

Premises used: RootPairing.mapsTo_reflection_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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_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:
hr ▸ he ▸ P₂.coroot_root_two i

Premises used: Eq.rec, RootPairing.coroot_root_two, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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_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:
exact hr ▸ he ▸ P₂.coroot_root_two i
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : ι
⊢ 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:
hr ▸ he ▸ P₂.mapsTo_reflection_root i

Premises used: RootPairing.mapsTo_reflection_root, Eq.rec, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : ι
⊢ 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:
exact hr ▸ he ▸ P₂.mapsTo_reflection_root i
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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)
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)
⊢ 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)

Tactic:
set α := root i

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
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)
⊢ let β : M := (root : (a : ι) → M) j;
  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)

Tactic:
set β := root j

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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)
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)
⊢ 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 α' := coroot i

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
hk :
  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
    ((preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α') : (a : M) → M) β : M)
set :
  let β' : N := (coroot : (a : ι) → N) j;
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) k : N)
    ((preReflection α' ((p : (a : M) → N →ₗ[R] R) α) : (a : N) → N) β' : N)
⊢ 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 j

Premises used: DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
hk :
  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
    ((preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α') : (a : M) → M) β : M)
β' : N := (coroot : (a : ι) → N) j
⊢ let sα : End R M := preReflection α ((p.flip : (a : N) → M →ₗ[R] R) α');
  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M) ((sα : (a : M) → M) β : M)

Tactic:
set sα := preReflection α (p.flip α')

Premises used: Module.preReflection, LinearMap.flip, DFunLike.coe