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
P : RootPairing ι R M N
x y : P.End
⊢ (x * y).indexEquiv = x.indexEquiv * y.indexEquiv
have H : ∀ (x_1 : ι),
  Eq (α := ι) (((x * y).indexEquiv : (a : ι) → ι) x_1 : ι) ((x.indexEquiv * y.indexEquiv : (a : ι) → ι) x_1 : ι)
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
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₂
e : P.Equiv Q
m : M₂
⊢ ((↑e : P.Hom Q).weightMap : (a : M) → M₂) (((weightEquiv P Q e).symm : (a : M₂) → M) m : M) = m
have rw : (weightEquiv P Q e : (a : M) → M₂) (((weightEquiv P Q e).symm : (a : M₂) → M) m : M) = m
Tactic: rw [← weightEquiv_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
ι₂ : 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₂
e : P.Equiv Q
n : N
⊢ ((↑e : P.Hom Q).coweightMap : (a : N₂) → N) (((coweightEquiv P Q e).symm : (a : N) → N₂) n : N₂) = n
have rw : (coweightEquiv P Q e : (a : N₂) → N) (((coweightEquiv P Q e).symm : (a : N) → N₂) n : N₂) = n
Tactic: rw [← coweightEquiv_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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective.{u_3 + 1, u_12 + 1} (α := M) (β := M₂) (⇑((↑g : P₁.Hom P₂).comp (↑f : P.Hom P₁)).weightMap : (a : M) → M₂)
have simp : Bijective.{u_3 + 1, u_12 + 1} (α := M) (β := M₂)
  (Function.comp.{u_3 + 1, u_9 + 1, u_12 + 1} (β := M₁) (⇑(↑g : P₁.Hom P₂).weightMap : (a : M₁) → M₂)
    (⇑(↑f : P.Hom P₁).weightMap : (a : M) → M₁))
Tactic: simp only [Hom.comp, LinearMap.coe_comp]
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q : RootPairing ι₂_1 R M₂_1 N₂_1
ι₁ : Type u_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
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₂
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ Bijective.{u_13 + 1, u_4 + 1} (α := N₂) (β := N) (⇑((↑g : P₁.Hom P₂).comp (↑f : P.Hom P₁)).coweightMap : (a : N₂) → N)
have simp : Bijective.{u_13 + 1, u_4 + 1} (α := N₂) (β := N)
  (Function.comp.{u_13 + 1, u_10 + 1, u_4 + 1} (β := N₁) (⇑(↑f : P.Hom P₁).coweightMap : (a : N₁) → N)
    (⇑(↑g : P₁.Hom P₂).coweightMap : (a : N₂) → N₁))
Tactic: simp only [Hom.comp, LinearMap.coe_comp]
-- 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_8
M₂ : Type u_9
N₂ : Type u_10
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.Equiv Q
⊢ f.comp (id P) = f
have weightMap : ∀ (x : M),
  Eq.{u_9 + 1} (α := M₂) (((↑(f.comp (id P)) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
    (((↑f : P.Hom Q).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_8
M₂ : Type u_9
N₂ : Type u_10
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.Equiv Q
weightMap :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M₂) (((↑(f.comp (id P)) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
      (((↑f : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
⊢ f.comp (id P) = f
have coweightMap : ∀ (x : N₂),
  Eq.{u_4 + 1} (α := N) (((↑(f.comp (id P)) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
    (((↑f : P.Hom Q).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_8
M₂ : Type u_9
N₂ : Type u_10
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.Equiv Q
weightMap :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M₂) (((↑(f.comp (id P)) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
      (((↑f : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) (((↑(f.comp (id P)) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
      (((↑f : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
⊢ f.comp (id P) = f
have indexEquiv : ∀ (x : ι),
  Eq.{u_8 + 1} (α := ι₂) (((↑(f.comp (id P)) : P.Hom Q).indexEquiv : (a : ι) → ι₂) x : ι₂)
    (((↑f : P.Hom Q).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_8
M₂ : Type u_9
N₂ : Type u_10
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.Equiv Q
⊢ (id Q).comp f = f
have weightMap : ∀ (x : M),
  Eq.{u_9 + 1} (α := M₂) (((↑((id Q).comp f) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
    (((↑f : P.Hom Q).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_8
M₂ : Type u_9
N₂ : Type u_10
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.Equiv Q
weightMap :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M₂) (((↑((id Q).comp f) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
      (((↑f : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
⊢ (id Q).comp f = f
have coweightMap : ∀ (x : N₂),
  Eq.{u_4 + 1} (α := N) (((↑((id Q).comp f) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
    (((↑f : P.Hom Q).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_8
M₂ : Type u_9
N₂ : Type u_10
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.Equiv Q
weightMap :
  ∀ (x : M),
    Eq.{u_9 + 1} (α := M₂) (((↑((id Q).comp f) : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
      (((↑f : P.Hom Q).weightMap : (a : M) → M₂) x : M₂)
coweightMap :
  ∀ (x : N₂),
    Eq.{u_4 + 1} (α := N) (((↑((id Q).comp f) : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
      (((↑f : P.Hom Q).coweightMap : (a : N₂) → N) x : N)
⊢ (id Q).comp f = f
have indexEquiv : ∀ (x : ι),
  Eq.{u_8 + 1} (α := ι₂) (((↑((id Q).comp f) : P.Hom Q).indexEquiv : (a : ι) → ι₂) x : ι₂)
    (((↑f : P.Hom Q).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_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
ι₃ : Type u_14
M₃ : Type u_15
N₃ : Type u_16
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₂.Equiv P₃
g : P₁.Equiv P₂
f : P.Equiv P₁
⊢ (h.comp g).comp f = h.comp (g.comp f)
have weightMap : ∀ (x : M),
  Eq.{u_15 + 1} (α := M₃) (((↑((h.comp g).comp f) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
    (((↑(h.comp (g.comp f)) : P.Hom P₃).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_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
ι₃ : Type u_14
M₃ : Type u_15
N₃ : Type u_16
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₂.Equiv P₃
g : P₁.Equiv P₂
f : P.Equiv P₁
weightMap :
  ∀ (x : M),
    Eq.{u_15 + 1} (α := M₃) (((↑((h.comp g).comp f) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
      (((↑(h.comp (g.comp f)) : P.Hom P₃).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) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)
    (((↑(h.comp (g.comp f)) : P.Hom P₃).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_8
M₁ : Type u_9
N₁ : Type u_10
ι₂ : Type u_11
M₂ : Type u_12
N₂ : Type u_13
ι₃ : Type u_14
M₃ : Type u_15
N₃ : Type u_16
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₂.Equiv P₃
g : P₁.Equiv P₂
f : P.Equiv P₁
weightMap :
  ∀ (x : M),
    Eq.{u_15 + 1} (α := M₃) (((↑((h.comp g).comp f) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
      (((↑(h.comp (g.comp f)) : P.Hom P₃).weightMap : (a : M) → M₃) x : M₃)
coweightMap :
  ∀ (x : N₃),
    Eq.{u_4 + 1} (α := N) (((↑((h.comp g).comp f) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)
      (((↑(h.comp (g.comp f)) : P.Hom P₃).coweightMap : (a : N₃) → N) x : N)
⊢ (h.comp g).comp f = h.comp (g.comp f)
have indexEquiv : ∀ (x : ι),
  Eq.{u_14 + 1} (α := ι₃) (((↑((h.comp g).comp f) : P.Hom P₃).indexEquiv : (a : ι) → ι₃) x : ι₃)
    (((↑(h.comp (g.comp f)) : P.Hom P₃).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
x y : P.Equiv P
⊢ weightEquiv P P (x.comp y) = weightEquiv P P y ≪≫ₗ weightEquiv P P x
have h : ∀ (x_1 : M),
  Eq (α := M) ((weightEquiv P P (x.comp y) : (a : M) → M) x_1 : M)
    ((weightEquiv P P y ≪≫ₗ weightEquiv P P x : (a : M) → M) x_1 : 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
x y : P.Equiv P
⊢ coweightEquiv P P (x.comp y) = coweightEquiv P P x ≪≫ₗ coweightEquiv P P y
have h : ∀ (x_1 : N),
  Eq (α := N) ((coweightEquiv P P (x.comp y) : (a : N) → N) x_1 : N)
    ((coweightEquiv P P x ≪≫ₗ coweightEquiv P P y : (a : N) → N) x_1 : 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ (↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂)
have h : ∀ (n : N) (m : M₂),
  Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
Tactic: ext n m
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
have h : Eq.{u_2 + 1} (α := R)
  (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
              (a : N) → Module.Dual R M₂)
            n :
          Module.Dual R M₂) :
        (a : M₂) → R)
      m :
    R)
  (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
              (a : N) → Module.Dual R M₂)
            n :
          Module.Dual R M₂) :
        (a : M₂) → R)
      ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
    R)
Tactic: nth_rw 2 [show m = (weightEquiv P Q f) ((weightEquiv P Q f).symm m) by
      exact (LinearEquiv.symm_apply_eq (weightEquiv P Q f)).mp rfl]
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)
have h : Eq.{u_2 + 1} (α := R)
  (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
              (a : N) → Module.Dual R M₂)
            ((coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)) :
          Module.Dual R M₂) :
        (a : M₂) → R)
      m :
    R)
  (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
              (a : N) → Module.Dual R M₂)
            n :
          Module.Dual R M₂) :
        (a : M₂) → R)
      ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
    R)
Tactic: nth_rw 1 [show n = (coweightEquiv P Q f) ((coweightEquiv P Q f).symm n) by
      exact (LinearEquiv.symm_apply_eq (coweightEquiv P Q f)).mp rfl]
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              ((coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)) :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)
have this : (↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
  (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap
Tactic: have := f.weight_coweight_transpose
-- 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
n : N
m : M₂
this :
  (↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M₂)
              ((coweightEquiv P Q f : (a : N₂) → N) (((coweightEquiv P Q f).symm : (a : N) → N₂) n : N₂)) :
            Module.Dual R M₂) :
          (a : M₂) → R)
        m :
      R)
    (((((↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) ∘ₗ (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) :
                (a : N) → Module.Dual R M₂)
              n :
            Module.Dual R M₂) :
          (a : M₂) → R)
        ((weightEquiv P Q f : (a : M) → M₂) (((weightEquiv P Q f).symm : (a : M₂) → M) m : M) : M₂) :
      R)
have this₁ : ∀ (m : N₂) (n : M),
  Eq.{u_2 + 1} (α := R)
    (((((↑f : P.Hom Q).weightMap.dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → M →ₗ[R] R) m :
            M →ₗ[R] R) :
          (a : M) → R)
        n :
      R)
    (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑f : P.Hom Q).coweightMap : (a : N₂) → M →ₗ[R] R) m :
            M →ₗ[R] R) :
          (a : M) → R)
        n :
      R)
Tactic: rw [LinearMap.ext_iff₂] 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
ι₂_1 : Type u_5
M₂_1 : Type u_6
N₂_1 : Type u_7
inst_5 : AddCommGroup M₂_1
inst_6 : Module R M₂_1
inst_7 : AddCommGroup N₂_1
inst_8 : Module R N₂_1
P_1 : RootPairing ι R M N
Q_1 : RootPairing ι₂_1 R M₂_1 N₂_1
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Equiv Q
⊢ Eq (α := ι₂ → M)
    (Function.comp.{u_8 + 1, u_9 + 1, u_3 + 1} (β := M₂) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)
      (⇑Q.root : (a : ι₂) → M₂))
    (Function.comp.{u_8 + 1, u_1 + 1, u_3 + 1} (β := ι) (⇑P.root : (a : ι) → M)
      (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι))
have h : ∀ (i : ι₂),
  Eq.{u_3 + 1} (α := M)
    (Function.comp.{u_8 + 1, u_9 + 1, u_3 + 1} (β := M₂) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)
      (⇑Q.root : (a : ι₂) → M₂) i)
    (Function.comp.{u_8 + 1, u_1 + 1, u_3 + 1} (β := ι) (⇑P.root : (a : ι) → M)
      (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i)
Tactic: ext i