awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
weightMap :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := M₂) (((f.comp (id P)).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) (((f.comp (id P)).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)
⊢ f.comp (id P) = f
have indexEquiv : ∀ (x : ι),
  Eq.{u_5 + 1} (α := ι₂) (((f.comp (id P)).indexEquiv : (a : ι) → ι₂) x : ι₂) ((f.indexEquiv : (a : ι) → ι₂) x : ι₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
⊢ (id Q).comp f = f
have weightMap : ∀ (x : M),
  Eq.{u_6 + 1} (α := M₂) ((((id Q).comp f).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
weightMap :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := M₂) ((((id Q).comp f).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)
⊢ (id Q).comp f = f
have coweightMap : ∀ (x : N₂),
  Eq.{u_4 + 1} (α := N) ((((id Q).comp f).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
weightMap :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := M₂) ((((id Q).comp f).weightMap : (a : M) → M₂) x : M₂) ((f.weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) ((((id Q).comp f).coweightMap : (a : N₂) → N) x : N) ((f.coweightMap : (a : N₂) → N) x : N)
⊢ (id Q).comp f = f
have indexEquiv : ∀ (x : ι),
  Eq.{u_5 + 1} (α := ι₂) ((((id Q).comp f).indexEquiv : (a : ι) → ι₂) x : ι₂) ((f.indexEquiv : (a : ι) → ι₂) x : ι₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
ι₃ : Type u_11
M₃ : Type u_12
N₃ : Type u_13
inst_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : Module R N₃
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
P₃ : RootPairing ι₃ R M₃ N₃
h : P₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom P₁
⊢ (h.comp g).comp f = h.comp (g.comp f)
have weightMap : ∀ (x : M),
  Eq.{u_12 + 1} (α := M₃) ((((h.comp g).comp f).weightMap : (a : M) → M₃) x : M₃)
    (((h.comp (g.comp f)).weightMap : (a : M) → M₃) x : M₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
ι₃ : Type u_11
M₃ : Type u_12
N₃ : Type u_13
inst_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : Module R N₃
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
P₃ : RootPairing ι₃ R M₃ N₃
h : P₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom P₁
weightMap :
  ∀ (x : M),
    Eq.{u_12 + 1} (α := M₃) ((((h.comp g).comp f).weightMap : (a : M) → M₃) x : M₃)
      (((h.comp (g.comp f)).weightMap : (a : M) → M₃) x : M₃)
⊢ (h.comp g).comp f = h.comp (g.comp f)
have coweightMap : ∀ (x : N₃),
  Eq.{u_4 + 1} (α := N) ((((h.comp g).comp f).coweightMap : (a : N₃) → N) x : N)
    (((h.comp (g.comp f)).coweightMap : (a : N₃) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
ι₃ : Type u_11
M₃ : Type u_12
N₃ : Type u_13
inst_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
inst_13 : AddCommGroup M₃
inst_14 : Module R M₃
inst_15 : AddCommGroup N₃
inst_16 : Module R N₃
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
P₃ : RootPairing ι₃ R M₃ N₃
h : P₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom P₁
weightMap :
  ∀ (x : M),
    Eq.{u_12 + 1} (α := M₃) ((((h.comp g).comp f).weightMap : (a : M) → M₃) x : M₃)
      (((h.comp (g.comp f)).weightMap : (a : M) → M₃) x : M₃)
coweightMap :
  ∀ (x : N₃),
    Eq.{u_4 + 1} (α := N) ((((h.comp g).comp f).coweightMap : (a : N₃) → N) x : N)
      (((h.comp (g.comp f)).coweightMap : (a : N₃) → N) x : N)
⊢ (h.comp g).comp f = h.comp (g.comp f)
have indexEquiv : ∀ (x : ι),
  Eq.{u_11 + 1} (α := ι₃) ((((h.comp g).comp f).indexEquiv : (a : ι) → ι₃) x : ι₃)
    (((h.comp (g.comp f)).indexEquiv : (a : ι) → ι₃) x : ι₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Eq.{u_3 + 1} (α := Module.End R M)
    (weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P) 1) 1
have h : ∀ (x : M),
  Eq (α := M)
    ((weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P) 1 :
          (a : M) → M)
        x :
      M)
    ((1 : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
g h : P.End
⊢ (g * h).weightMap = g.weightMap * h.weightMap
have h₁ : ∀ (x : M), Eq (α := M) (((g * h).weightMap : (a : M) → M) x : M) ((g.weightMap * h.weightMap : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
⊢ f = g
have weightMap : ∀ (x : M), Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
weightMap : ∀ (x : M), Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
⊢ f = g
have coweightMap : ∀ (x : N), Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
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)
⊢ f = g
have indexEquiv : ∀ (x : ι), Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
have 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)
Tactic: refine LinearEquiv.injective P.flip.toPerfPair ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
    ((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)
have 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)
Tactic: simp_rw [← weight_coweight_transpose_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι)
have indexEquiv : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((f.indexEquiv : (a : ι) → ι) x : ι) : M)
  ((P.root : (a : ι) → M) ((g.indexEquiv : (a : ι) → ι) x : ι) : M)
Tactic: refine Embedding.injective P.root ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((f.indexEquiv : (a : ι) → ι) x : ι) : M)
    ((P.root : (a : ι) → M) ((g.indexEquiv : (a : ι) → ι) x : ι) : M)
have 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)
Tactic: simp_rw [← root_weightMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)ᵐᵒᵖ)
⊢ f = g
have weightMap : ∀ (x : M), Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
⊢ f = g
have coweightMap : ∀ (x : N), Eq (α := N) ((f.coweightMap : (a : N) → N) x : N) ((g.coweightMap : (a : N) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
⊢ f = g
have indexEquiv : ∀ (x : ι), Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : M
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
have weightMap : ∀ (hfg : f.coweightMap = g.coweightMap) (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
Cleared hypotheses: hfg, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : M
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
have h : (↑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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
have 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)
Tactic: rw [← f.weight_coweight_transpose, ← g.weight_coweight_transpose] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
have this : Module.IsReflexive R M
Tactic: haveI : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
⊢ Eq (α := M) ((f.weightMap : (a : M) → M) x : M) ((g.weightMap : (a : M) → M) x : M)
have this : 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))
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
f g : P.End
hfg : MulOpposite.op f.coweightMap = MulOpposite.op g.coweightMap
x : ι
⊢ Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
have indexEquiv : ∀ (hfg : f.coweightMap = g.coweightMap) (x : ι),
  Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
Tactic: rw [MulOpposite.op_inj] at hfg
Cleared hypotheses: hfg, x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
f g : P.End
hfg : f.coweightMap = g.coweightMap
x : ι
⊢ Eq (α := ι) ((f.indexEquiv : (a : ι) → ι) x : ι) ((g.indexEquiv : (a : ι) → ι) x : ι)
have indexEquiv : let y : ι := (f.indexEquiv : (a : ι) → ι) x;
∀ (hy : y = (f.indexEquiv : (a : ι) → ι) x), y = (g.indexEquiv : (a : ι) → ι) x
Tactic: set y := f.indexEquiv x with hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
⊢ y = (g.indexEquiv : (a : ι) → ι) x
have 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)
Tactic: have : f.coweightMap (P.coroot y) = g.coweightMap (P.coroot y) := by
      exact congrFun (congrArg DFunLike.coe hfg) (P.coroot y)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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)
⊢ y = (g.indexEquiv : (a : ι) → ι) x
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι) : ι)
⊢ y = (g.indexEquiv : (a : ι) → ι) x
have this₁ : x = (g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι)
Tactic: rw [Equiv.symm_apply_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι)
⊢ y = (g.indexEquiv : (a : ι) → ι) x
have indexEquiv : y = (g.indexEquiv : (a : ι) → ι) ((g.indexEquiv.symm : (a : ι) → ι) ((f.indexEquiv : (a : ι) → ι) x : ι) : ι)
Tactic: rw [this, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ 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
have 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 : ι)
Tactic: ext