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
P : RootPairing ι R M N
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : M
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)

Tactic:
exact LinearMap.congr_fun hfg x

Premises used: LinearMap.congr_fun
-- 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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : N
⊢ Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : N)

Tactic:
LinearEquiv.injective P.flip.toPerfPair ?_

Premises used: RootPairing.flip, RootPairing.toLinearMap, LinearMap.toPerfPair, LinearEquiv.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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : N
coweightMap :
  Eq (α := Module.Dual R M)
    ((P.flip.toPerfPair : (a : N) → Module.Dual R M) ((f.coweightMap : (a : N) → N) x) : Module.Dual R M)
    ((P.flip.toPerfPair : (a : N) → Module.Dual R M) ((g.coweightMap : (a : N) → N) x) : Module.Dual R M)
⊢ Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : N)

Tactic:
refine LinearEquiv.injective P.flip.toPerfPair ?_

Premises used: RootPairing.flip, RootPairing.toLinearMap, LinearMap.toPerfPair, LinearEquiv.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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : N
coweightMap :
  Eq (α := Module.Dual R M)
    ((f.weightMap.dualMap : (a : Module.Dual R M) → Module.Dual R M)
        ((P.flip.toPerfPair : (a : N) → Module.Dual R M) x) :
      Module.Dual R M)
    ((g.weightMap.dualMap : (a : Module.Dual R M) → Module.Dual R M)
        ((P.flip.toPerfPair : (a : N) → Module.Dual R M) x) :
      Module.Dual R M)
⊢ Eq (α := Module.Dual R M)
    ((P.flip.toPerfPair : (a : N) → Module.Dual R M) ((f.coweightMap : (a : N) → N) x) : Module.Dual R M)
    ((P.flip.toPerfPair : (a : N) → Module.Dual R M) ((g.coweightMap : (a : N) → N) x) : Module.Dual R M)

Tactic:
simp_rw [← weight_coweight_transpose_apply]

Premises used: RootPairing.Hom.weight_coweight_transpose_apply
-- 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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : N
⊢ Eq (α := Module.Dual R M)
    ((f.weightMap.dualMap : (a : Module.Dual R M) → Module.Dual R M)
        ((P.flip.toPerfPair : (a : N) → Module.Dual R M) x) :
      Module.Dual R M)
    ((g.weightMap.dualMap : (a : Module.Dual R M) → Module.Dual R M)
        ((P.flip.toPerfPair : (a : N) → Module.Dual R M) x) :
      Module.Dual R M)

Tactic:
congrFun (congrArg DFunLike.coe (congrArg LinearMap.dualMap hfg)) (P.flip.toPerfPair x)

Premises used: congrArg, RootPairing.flip, RootPairing.toLinearMap, LinearMap.toPerfPair, congrFun, DFunLike.coe, LinearMap.dualMap
-- 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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : N
⊢ Eq (α := Module.Dual R M)
    ((f.weightMap.dualMap : (a : Module.Dual R M) → Module.Dual R M)
        ((P.flip.toPerfPair : (a : N) → Module.Dual R M) x) :
      Module.Dual R M)
    ((g.weightMap.dualMap : (a : Module.Dual R M) → Module.Dual R M)
        ((P.flip.toPerfPair : (a : N) → Module.Dual R M) x) :
      Module.Dual R M)

Tactic:
exact congrFun (congrArg DFunLike.coe (congrArg LinearMap.dualMap hfg)) (P.flip.toPerfPair x)

Premises used: congrArg, RootPairing.flip, RootPairing.toLinearMap, LinearMap.toPerfPair, congrFun, DFunLike.coe, LinearMap.dualMap
-- 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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : ι
⊢ Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)

Tactic:
Embedding.injective P.root ?_

Premises used: RootPairing.root, Function.Embedding.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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : ι
indexEquiv :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((f.indexEquiv : (a : ι) → ι) x : ι) : M)
    ((P.root : (a : ι) → M) ((g.indexEquiv : (a : ι) → ι) x : ι) : M)
⊢ Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)

Tactic:
refine Embedding.injective P.root ?_

Premises used: RootPairing.root, Function.Embedding.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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : ι
indexEquiv :
  Eq (α := M) ((f.weightMap : (a : M) → M) ((P.root : (a : ι) → M) x : M) : M)
    ((g.weightMap : (a : M) → M) ((P.root : (a : ι) → M) x : M) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((f.indexEquiv : (a : ι) → ι) x : ι) : M)
    ((P.root : (a : ι) → M) ((g.indexEquiv : (a : ι) → ι) x : ι) : M)

Tactic:
simp_rw [← root_weightMap_apply]

Premises used: RootPairing.Hom.root_weightMap_apply
-- 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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : ι
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) ((P.root : (a : ι) → M) x : M) : M)
    ((g.weightMap : (a : M) → M) ((P.root : (a : ι) → M) x : M) : M)

Tactic:
congrFun (congrArg DFunLike.coe hfg) (P.root x)

Premises used: congrArg, RootPairing.root, congrFun, DFunLike.coe
-- 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
f g : P.End
hfg :
  Eq.{u_3 + 1} (α := Module.End R M) ((weightHom P : (a : P.End) → Module.End R M) f : Module.End R M)
    ((weightHom P : (a : P.End) → Module.End R M) g : Module.End R M)
x : ι
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) ((P.root : (a : ι) → M) x : M) : M)
    ((g.weightMap : (a : M) → M) ((P.root : (a : ι) → M) x : M) : M)

Tactic:
exact congrFun (congrArg DFunLike.coe hfg) (P.root x)

Premises used: congrArg, RootPairing.root, congrFun, DFunLike.coe
-- 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
⊢ Eq.{u_4 + 1} (α := (N →ₗ[R] N)ᵐᵒᵖ)
    (MulOpposite.op
      (coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P) 1))
    1

Tactic:
simp only [MulOpposite.op_eq_one_iff, coweightMap_one, Module.End.one_eq_id]

Premises used: MulOpposite.op_eq_one_iff, Module.End.one_eq_id, RootPairing.Hom.coweightMap_one
-- 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 h : P.End
⊢ MulOpposite.op (g * h).coweightMap = MulOpposite.op g.coweightMap * MulOpposite.op h.coweightMap

Tactic:
simp only [← MulOpposite.op_mul, coweightMap_mul, Module.End.mul_eq_comp]

Premises used: RootPairing.Hom.coweightMap_mul, Module.End.mul_eq_comp, MulOpposite.op_mul
-- 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
f g : P.End
hfg :
  Eq.{u_4 + 1} (α := (N →ₗ[R] N)ᵐᵒᵖ) ((coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) f : (N →ₗ[R] N)ᵐᵒᵖ)
    ((coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) g : (N →ₗ[R] N)ᵐᵒᵖ)
weightMap : ∀ (x : M), Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
coweightMap : ∀ (x : N), Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : N)
indexEquiv : ∀ (x : ι), Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
⊢ f = g

Tactic:
ext x
-- 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : M
weightMap :
  ∀ (hfg : f.coweightMap = g.coweightMap) (x : M),
    Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)

Tactic:
rw [MulOpposite.op_inj] at hfg

Premises used: MulOpposite.op_inj
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
⊢ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ f.coweightMap =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ g.coweightMap

Tactic:
have h := congrArg (LinearMap.comp (M₃ := Module.Dual R M) (σ₂₃ := .id R) P.flip.toPerfPair) hfg
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ f.coweightMap =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ g.coweightMap
⊢ f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)

Tactic:
rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h

Premises used: RootPairing.Hom.weight_coweight_transpose
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)
⊢ Module.IsReflexive R M

Tactic:
haveI : Module.IsReflexive R M := .of_isPerfPair P.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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)
this : Module.IsReflexive R M
⊢ f.weightMap = g.weightMap

Tactic:
(Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
        ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))

Premises used: Module.dualMap_dualMap_eq_iff, congrArg, LinearEquiv.eq_comp_toLinearMap_iff, Iff.mp, RootPairing.Hom.weightMap, LinearMap.dualMap
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)
this : Module.IsReflexive R M
⊢ f.weightMap = g.weightMap

Tactic:
refine (Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
        ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp h))

Premises used: Module.dualMap_dualMap_eq_iff, congrArg, LinearEquiv.eq_comp_toLinearMap_iff, Iff.mp, RootPairing.Hom.weightMap, LinearMap.dualMap
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)
⊢ f.weightMap = g.weightMap

Tactic:
have : f.weightMap = g.weightMap := by
      haveI : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
      refine (Module.dualMap_dualMap_eq_iff R M).mp (congrArg LinearMap.dualMap
        ((LinearEquiv.eq_comp_toLinearMap_iff f.weightMap.dualMap g.weightMap.dualMap).mp 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)
this : f.weightMap = g.weightMap
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)

Tactic:
congrFun (congrArg DFunLike.coe this) x

Premises used: congrArg, congrFun, DFunLike.coe
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
h :
  f.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    g.weightMap.dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M)
this : f.weightMap = g.weightMap
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)

Tactic:
exact congrFun (congrArg DFunLike.coe this) x

Premises used: congrArg, congrFun, DFunLike.coe
-- 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : N
⊢ Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : 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
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : ι
indexEquiv :
  ∀ (hfg : f.coweightMap = g.coweightMap) (x : ι),
    Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
⊢ Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)

Tactic:
rw [MulOpposite.op_inj] at hfg

Premises used: MulOpposite.op_inj
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
indexEquiv :
  let y : ι := (f.indexEquiv : (a : ι) → ι) x;
  ∀ (hy : y = (f.indexEquiv : (a : ι) → ι) x), y = (g.indexEquiv : (a : ι) → ι) x
⊢ Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)

Tactic:
set y := f.indexEquiv x with hy

Premises used: RootPairing.Hom.indexEquiv, DFunLike.coe
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := (f.indexEquiv : (a : ι) → ι) x
hy : y = (f.indexEquiv : (a : ι) → ι) x
⊢ Eq (α := N) ((f.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)
    ((g.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)

Tactic:
congrFun (congrArg DFunLike.coe hfg) (P.coroot y)

Premises used: congrArg, congrFun, RootPairing.coroot, DFunLike.coe
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := (f.indexEquiv : (a : ι) → ι) x
hy : y = (f.indexEquiv : (a : ι) → ι) x
⊢ Eq (α := N) ((f.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)
    ((g.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)

Tactic:
exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)

Premises used: congrArg, congrFun, RootPairing.coroot, DFunLike.coe
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := (f.indexEquiv : (a : ι) → ι) x
hy : y = (f.indexEquiv : (a : ι) → ι) x
⊢ Eq (α := N) ((f.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)
    ((g.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)

Tactic:
have : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y) := by
      exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := (f.indexEquiv : (a : ι) → ι) x
hy : y = (f.indexEquiv : (a : ι) → ι) x
this :
  Eq (α := N) ((f.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)
    ((g.coweightMap : (a : N) → N) ((P.coroot : (a : ι) → N) y : N) : N)
⊢ Eq (α := ι) ((f.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι) : ι)
    ((g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι) : ι)

Tactic:
rw [coroot_coweightMap_apply, coroot_coweightMap_apply, Embedding.apply_eq_iff_eq, hy] at this

Premises used: Function.Embedding.apply_eq_iff_eq, RootPairing.Hom.coroot_coweightMap_apply
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := (f.indexEquiv : (a : ι) → ι) x
hy : y = (f.indexEquiv : (a : ι) → ι) x
this :
  Eq (α := ι) ((f.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι) : ι)
    ((g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι) : ι)
⊢ x = (g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι)

Tactic:
rw [Equiv.symm_apply_apply] at this

Premises used: Equiv.symm_apply_apply
-- 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
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
y : ι := (f.indexEquiv : (a : ι) → ι) x
hy : y = (f.indexEquiv : (a : ι) → ι) x
this : x = (g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι)
indexEquiv :
  y = (g.indexEquiv : (a : ι) → ι) ((g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι) : ι)
indexEquiv₁ indexEquiv₂ : y = (f.indexEquiv : (a : ι) → ι) x
⊢ y = (g.indexEquiv : (a : ι) → ι) x

Tactic:
rw [this, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- 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
H :
  ∀ (x : ι),
    Eq (α := ι)
      ((indexEquiv.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (R := R) (M := M) (N := N) (M₂ := M) (N₂ := N) (P := P) (Q := P)
              1 :
            (a : ι) → ι)
          x :
        ι)
      ((1 : (a : ι) → ι) x : ι)
⊢ Eq.{u_1 + 1} (α := ι ≃ ι)
    (indexEquiv.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (R := R) (M := M) (N := N) (M₂ := M) (N₂ := N) (P := P) (Q := 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
P : RootPairing ι R M N
x : ι
⊢ Eq (α := ι)
    ((indexEquiv.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (R := R) (M := M) (N := N) (M₂ := M) (N₂ := N) (P := P) (Q := P)
            1 :
          (a : ι) → ι)
        x :
      ι)
    ((1 : (a : ι) → ι) x : ι)

Tactic:
simp