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 : 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) α)
hij : preReflection ((sα : (a : M) → M) β) ((p.flip : (a : N) → M →ₗ[R] R) ((sα' : (a : N) → N) β')) = sα ∘ₗ sβ ∘ₗ sα
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : 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)
hkl :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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
β' : 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α
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : 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)
hkl :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
this : IsAddTorsionFree M
⊢ InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑p.flip : (a : N) → M →ₗ[R] R) (⇑coroot : (a : ι) → N)))

Tactic:
have := injOn_dualMap_subtype_span_range_range (finite_range root)
    (c := p.flip ∘ coroot) hp hr
-- 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
β' : 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α
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : 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)
hkl :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
this_1 : IsAddTorsionFree M
this :
  InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑p.flip : (a : N) → M →ₗ[R] R) (⇑coroot : (a : ι) → N)))
rw :
  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))
⊢ MapsTo.{u_3, u_3} (α := M) (β := M)
    (⇑(preReflection ((root : (a : ι) → M) k)
            (comp (β := N) (⇑p.flip : (a : N) → M →ₗ[R] R) (⇑coroot : (a : ι) → N) l) :
          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:
rw [comp_apply, hl, hk, hij]

Premises used: Function.comp_apply
-- 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
β' : 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α
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : 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)
hkl :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
this_1 : IsAddTorsionFree M
this :
  InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑p.flip : (a : N) → M →ₗ[R] R) (⇑coroot : (a : ι) → N)))
⊢ 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:
(hr i).comp <| (hr j).comp (hr i)

Premises used: Set.MapsTo.comp
-- 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
β' : 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α
l : ι
hl :
  Eq.{u_4 + 1} (α := N) ((coroot : (a : ι) → N) l : 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)
hkl :
  Eq.{u_2 + 1} (α := R)
    ((((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) l) : M →ₗ[R] R) : (a : M) → R)
        ((root : (a : ι) → M) k : M) :
      R)
    (2 : R)
this_1 : IsAddTorsionFree M
this :
  InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑p.flip : (a : N) → M →ₗ[R] R) (⇑coroot : (a : ι) → N)))
⊢ 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:
exact (hr i).comp <| (hr j).comp (hr i)

Premises used: Set.MapsTo.comp
-- 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
P : RootPairing ι R M 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 : ι
simp :
  HSub.hSub (α := M) ((root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) i : N) :
          R)
        ((root : (a : ι) → M) i : M)) =
    (root : (a : ι) → M) ((sorry () : (a : ι) → ι) j : ι)
⊢ HSub.hSub (α := M) ((root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) i : N) :
          R)
        ((root : (a : ι) → M) i : M)) =
    (root : (a : ι) → M) ((sorry : (a : ι) → ι) j : ι)

Tactic:
simp [(exist_eq_reflection_of_mapsTo p root coroot i j hr).choose_spec, preReflection_apply]

Premises used: Exists.choose_spec, Module.preReflection_apply, _private.0.RootPairing.exist_eq_reflection_of_mapsTo
-- 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
P : RootPairing ι R M 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 : ι
⊢ HSub.hSub (α := N) ((coroot : (a : ι) → N) j : N)
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) j : N) :
          R)
        ((coroot : (a : ι) → N) i : N)) =
    (coroot : (a : ι) → N) ((sorry : (a : ι) → ι) j : ι)

Tactic:
(coroot_eq_coreflection_of_root_eq' p root coroot hp hr hc ?_).symm

Premises used: _private.0.RootPairing.coroot_eq_coreflection_of_root_eq', 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
P : RootPairing ι R M 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 : ι
refine :
  Eq (α := M) ((root : (a : ι) → M) ((sorry : (a : ι) → ι) j : ι) : 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)
⊢ HSub.hSub (α := N) ((coroot : (a : ι) → N) j : N)
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
        ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
            ((coroot : (a : ι) → N) j : N) :
          R)
        ((coroot : (a : ι) → N) i : N)) =
    (coroot : (a : ι) → N) ((sorry : (a : ι) → ι) j : ι)

Tactic:
refine (coroot_eq_coreflection_of_root_eq' p root coroot hp hr hc ?_).symm

Premises used: _private.0.RootPairing.coroot_eq_coreflection_of_root_eq', 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
inst_9 : P₁.IsRootSystem
inst_10 : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
this :
  ∀ (P₁ P₂ : RootPairing ι R M N) [P₁.IsRootSystem] [P₂.IsRootSystem],
    P₁.toLinearMap = P₂.toLinearMap →
      P₁.root = P₂.root →
        Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
          (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
⊢ Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))

Tactic:
have h₁ := this P₁ P₂ he hr
-- 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
inst_9 : P₁.IsRootSystem
inst_10 : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
this :
  ∀ (P₁ P₂ : RootPairing ι R M N) [P₁.IsRootSystem] [P₂.IsRootSystem],
    P₁.toLinearMap = P₂.toLinearMap →
      P₁.root = P₂.root →
        Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
          (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
h₁ :
  Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
⊢ Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))

Tactic:
have h₂ := this P₂ P₁ he.symm hr.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
inst_9 : P₁.IsRootSystem
inst_10 : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
this :
  ∀ (P₁ P₂ : RootPairing ι R M N) [P₁.IsRootSystem] [P₂.IsRootSystem],
    P₁.toLinearMap = P₂.toLinearMap →
      P₁.root = P₂.root →
        Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
          (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
h₁ :
  Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
h₂ :
  Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
⊢ P₁ = P₂

Tactic:
RootPairing.ext he hr (le_antisymm h₁ h₂)

Premises used: RootPairing.ext, le_antisymm
-- 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
inst_9 : P₁.IsRootSystem
inst_10 : P₂.IsRootSystem
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
this :
  ∀ (P₁ P₂ : RootPairing ι R M N) [P₁.IsRootSystem] [P₂.IsRootSystem],
    P₁.toLinearMap = P₂.toLinearMap →
      P₁.root = P₂.root →
        Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
          (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
h₁ :
  Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
h₂ :
  Subset.{u_4} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
⊢ P₁ = P₂

Tactic:
exact RootPairing.ext he hr (le_antisymm h₁ h₂)

Premises used: RootPairing.ext, le_antisymm