awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Endˣ
⊢ (fun (f : P.Aut) ↦ { val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ })
      ((fun (f : P.Endˣ) ↦
          let __src := (↑f : P.End);
          { toHom := __src, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ : P.Equiv P })
        f) =
    f

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
huv :
  ∀ (x : M),
    Eq (α := M)
      (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                    inv_val := ⋯ : P.Endˣ } :
                P.End).weightMap :
            (a : M) → M)
          x :
        M)
      (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                    { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
                P.End).weightMap :
            (a : M) → M)
          x :
        M)
huv₁ :
  ∀ (x : N),
    Eq (α := N)
      (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                    inv_val := ⋯ : P.Endˣ } :
                P.End).coweightMap :
            (a : N) → N)
          x :
        N)
      (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                    { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
                P.End).coweightMap :
            (a : N) → N)
          x :
        N)
huv₂ :
  ∀ (x : ι),
    Eq (α := ι)
      (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                    inv_val := ⋯ : P.Endˣ } :
                P.End).indexEquiv :
            (a : ι) → ι)
          x :
        ι)
      (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                    { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
                P.End).indexEquiv :
            (a : ι) → ι)
          x :
        ι)
⊢ { val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯, inv_val := ⋯ } =
    { val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
      { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x : M
⊢ Eq (α := M)
    (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                  inv_val := ⋯ : P.Endˣ } :
              P.End).weightMap :
          (a : M) → M)
        x :
      M)
    (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                  { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
              P.End).weightMap :
          (a : M) → M)
        x :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x : N
⊢ Eq (α := N)
    (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                  inv_val := ⋯ : P.Endˣ } :
              P.End).coweightMap :
          (a : N) → N)
        x :
      N)
    (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                  { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
              P.End).coweightMap :
          (a : N) → N)
        x :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
x : ι
⊢ Eq (α := ι)
    (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                  inv_val := ⋯ : P.Endˣ } :
              P.End).indexEquiv :
          (a : ι) → ι)
        x :
      ι)
    (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                  { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
              P.End).indexEquiv :
          (a : ι) → ι)
        x :
      ι)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g : P.Aut
⊢ (↑((toEndUnit P : (a : P.Aut) → P.Endˣ) g) : P.End) = (↑g : P.Hom P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g : P.Aut
⊢ Units.inv ((toEndUnit P : (a : P.Aut) → P.Endˣ) g) = (↑(symm P P g) : P.Hom P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
h : ∀ (x : M), Eq (α := M) ((weightEquiv P P 1 : (a : M) → M) x : M) ((1 : (a : M) → M) x : M)
⊢ weightEquiv P P 1 = 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
x : M
⊢ Eq (α := M) ((weightEquiv P P 1 : (a : M) → M) x : M) ((1 : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
x y : P.Aut
h :
  ∀ (x_1 : M),
    Eq (α := M) ((weightEquiv P P (x * y) : (a : M) → M) x_1 : M)
      ((weightEquiv P P x * weightEquiv P P y : (a : M) → M) x_1 : M)
⊢ weightEquiv P P (x * y) = weightEquiv P P x * weightEquiv P P y

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
x y : P.Aut
x_1 : M
⊢ Eq (α := M) ((weightEquiv P P (x * y) : (a : M) → M) x_1 : M)
    ((weightEquiv P P x * weightEquiv P P y : (a : M) → M) x_1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g : P.Aut
⊢ Eq.{u_3 + 1} (α := M →ₗ[R] M) (↑((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) g) : M →ₗ[R] M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
⊢ Injective (α := P.Aut) (β := M ≃ₗ[R] M) (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M)

Tactic:
Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
refine :
  ∀ (g g' : P.Aut)
    (hgg' :
      Eq.{u_3 + 1} (α := M →ₗ[R] M)
        (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
        (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')),
    g = g'
⊢ Injective (α := P.Aut) (β := M ≃ₗ[R] M) (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M)

Tactic:
refine Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h : Eq.{u_3 + 1} (α := M →ₗ[R] M) (↑((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) g) : M →ₗ[R] M)
  (↑((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) g') : M →ₗ[R] M) :=
  hgg'
⊢ Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)

Tactic:
rw [weightHom_toLinearMap, weightHom_toLinearMap] at h

Premises used: RootPairing.Equiv.weightHom_toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h :
  Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
h' : (↑g : P.Hom P) = (↑g' : P.Hom P)
⊢ g = g'

Tactic:
Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')

Premises used: RootPairing.Hom.indexEquiv, congrArg, RootPairing.Equiv.ext, RootPairing.Hom.coweightMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h :
  Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
h' : (↑g : P.Hom P) = (↑g' : P.Hom P)
⊢ g = g'

Tactic:
exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')

Premises used: RootPairing.Hom.indexEquiv, congrArg, RootPairing.Equiv.ext, RootPairing.Hom.coweightMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h :
  Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
suffices : (↑g : P.Hom P) = (↑g' : P.Hom P)
⊢ g = g'

Tactic:
suffices h' : g.toHom = g'.toHom by
    exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h :
  Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
⊢ (↑g : P.Hom P) = (↑g' : P.Hom P)

Tactic:
Hom.weightHom_injective P hgg'

Premises used: RootPairing.Hom.weightHom_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h :
  Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
⊢ (↑g : P.Hom P) = (↑g' : P.Hom P)

Tactic:
exact Hom.weightHom_injective P hgg'

Premises used: RootPairing.Hom.weightHom_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g : P.Aut
⊢ weightEquiv P P g⁻¹ = (weightEquiv P P g)⁻¹

Tactic:
LinearEquiv.toLinearMap_inj.mp rfl

Premises used: LinearEquiv.toLinearMap_inj, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
simp : coweightEquiv P P 1 = 1
⊢ MulOpposite.op (coweightEquiv P P 1) = 1

Tactic:
simp only [MulOpposite.op_eq_one_iff]

Premises used: MulOpposite.op_eq_one_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
⊢ coweightEquiv P P 1 = 1

Tactic:
LinearEquiv.toLinearMap_inj.mp rfl

Premises used: LinearEquiv.toLinearMap_inj, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
⊢ coweightEquiv P P 1 = 1

Tactic:
exact LinearEquiv.toLinearMap_inj.mp rfl

Premises used: LinearEquiv.toLinearMap_inj, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
simp :
  ∀ (x y : P.Aut),
    MulOpposite.op (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) =
      MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)
⊢ ∀ (x y : P.Aut),
    MulOpposite.op (coweightEquiv P P (x * y)) =
      MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)

Tactic:
simp only [mul_eq_comp, coweightEquiv_comp_toLin]

Premises used: RootPairing.Equiv.coweightEquiv_comp_toLin, RootPairing.Equiv.mul_eq_comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
⊢ ∀ (x y : P.Aut),
    MulOpposite.op (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) =
      MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)

Tactic:
fun x y ↦ rfl

Premises used: RootPairing.Equiv.coweightEquiv, MulOpposite.unop, LinearEquiv.trans, rfl, LinearEquiv.ofBijective
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
⊢ ∀ (x y : P.Aut),
    MulOpposite.op (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) =
      MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)

Tactic:
exact fun x y ↦ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g : P.Aut
⊢ Eq.{u_4 + 1} (α := N →ₗ[R] N) (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g)) : N →ₗ[R] N)
    (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g : P.Hom P)))

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
⊢ Injective (α := P.Aut) (β := (N ≃ₗ[R] N)ᵐᵒᵖ) (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)

Tactic:
Injective.of_comp (f := fun a => MulOpposite.op a) fun g g' hgg' => ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
refine :
  ∀ (g g' : P.Aut)
    (hgg' :
      Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
        (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
        (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')),
    g = g'
⊢ Injective (α := P.Aut) (β := (N ≃ₗ[R] N)ᵐᵒᵖ) (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)

Tactic:
refine Injective.of_comp (f := fun a => MulOpposite.op a) fun g g' hgg' => ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')
⊢ Eq.{u_4 + 1} (α := N →ₗ[R] N) (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g)) : N →ₗ[R] N)
    (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g')) : N →ₗ[R] N)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
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
g g' : P.Aut
hgg' :
  Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')
⊢ Eq.{u_4 + 1} (α := N →ₗ[R] N) (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g)) : N →ₗ[R] N)
    (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g')) : N →ₗ[R] N)

Tactic:
have h : (MulOpposite.unop (coweightHom P g)).toLinearMap =
      (MulOpposite.unop (coweightHom P g')).toLinearMap := by
    simp_all