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
ι₂_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
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)
have h : Eq.{u_3 + 1} (α := M) (((weightEquiv P Q f).symm : (a : M₂) → M) ((Q.root : (a : ι₂) → M₂) i : M₂) : M)
  ((P.root : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι) : M)
Tactic: simp only [LinearEquiv.coe_coe, comp_apply]
-- 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
i : ι₂
⊢ Eq.{u_3 + 1} (α := M) (((weightEquiv P Q f).symm : (a : M₂) → M) ((Q.root : (a : ι₂) → M₂) i : M₂) : M)
    ((P.root : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι) : M)
have this : Eq (α := ι → M₂)
  (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M) (⇑(↑f : P.Hom Q).weightMap : (a : M) → M₂)
    (⇑P.root : (a : ι) → M))
  (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂)
    (⇑(↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂))
Tactic: have := f.root_weightMap
-- 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
i : ι₂
this :
  ∀ (x : ι),
    Eq.{u_9 + 1} (α := M₂)
      (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (β := M) (⇑(↑f : P.Hom Q).weightMap : (a : M) → M₂)
        (⇑P.root : (a : ι) → M) x)
      (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂)
        (⇑(↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) x)
⊢ Eq.{u_3 + 1} (α := M) (((weightEquiv P Q f).symm : (a : M₂) → M) ((Q.root : (a : ι₂) → M₂) i : M₂) : M)
    ((P.root : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι) : M)
have this₁ : Eq.{u_9 + 1} (α := M₂)
  (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (α := ι) (β := M) (⇑(↑f : P.Hom Q).weightMap : (a : M) → M₂)
    ((⇑P.root : (a : ι) → M) : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι))
  (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (α := ι) (β := ι₂) (⇑Q.root : (a : ι₂) → M₂)
    ((⇑(↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) : (a : ι) → ι₂)
    (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι))
Tactic: specialize this (f.indexEquiv.symm i)
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
ι₂_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
i : ι₂
this :
  Eq.{u_9 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_9 + 1} (α := ι) (β := M) (⇑(↑f : P.Hom Q).weightMap : (a : M) → M₂)
      ((⇑P.root : (a : ι) → M) : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι))
    (Function.comp.{u_1 + 1, u_8 + 1, u_9 + 1} (α := ι) (β := ι₂) (⇑Q.root : (a : ι₂) → M₂)
      ((⇑(↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) : (a : ι) → ι₂)
      (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι))
⊢ Eq.{u_3 + 1} (α := M) (((weightEquiv P Q f).symm : (a : M₂) → M) ((Q.root : (a : ι₂) → M₂) i : M₂) : M)
    ((P.root : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι) : M)
have this₁ : Eq.{u_9 + 1} (α := M₂)
  (((↑f : P.Hom Q).weightMap : (a : M) → M₂)
      ((P.root : (a : ι) → M) (((↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) i : ι) : M) :
    M₂)
  ((Q.root : (a : ι₂) → M₂) i : M₂)
Tactic: simp only [comp_apply, Equiv.apply_symm_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
ι₂_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 (α := ι → N₂)
    (Function.comp.{u_1 + 1, u_4 + 1, u_10 + 1} (β := N) (⇑(↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) : (a : N) → N₂)
      (⇑P.coroot : (a : ι) → N))
    (Function.comp.{u_1 + 1, u_8 + 1, u_10 + 1} (β := ι₂) (⇑Q.coroot : (a : ι₂) → N₂)
      (⇑(↑f : P.Hom Q).indexEquiv.symm.symm : (a : ι) → ι₂))
have h : ∀ (i : ι),
  Eq.{u_10 + 1} (α := N₂)
    (Function.comp.{u_1 + 1, u_4 + 1, u_10 + 1} (β := N) (⇑(↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) : (a : N) → N₂)
      (⇑P.coroot : (a : ι) → N) i)
    (Function.comp.{u_1 + 1, u_8 + 1, u_10 + 1} (β := ι₂) (⇑Q.coroot : (a : ι₂) → N₂)
      (⇑(↑f : P.Hom Q).indexEquiv.symm.symm : (a : ι) → ι₂) i)
Tactic: ext i
-- 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
i : ι
⊢ Eq.{u_10 + 1} (α := N₂)
    (Function.comp.{u_1 + 1, u_4 + 1, u_10 + 1} (β := N) (⇑(↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) : (a : N) → N₂)
      (⇑P.coroot : (a : ι) → N) i)
    (Function.comp.{u_1 + 1, u_8 + 1, u_10 + 1} (β := ι₂) (⇑Q.coroot : (a : ι₂) → N₂)
      (⇑(↑f : P.Hom Q).indexEquiv.symm.symm : (a : ι) → ι₂) i)
have h : Eq.{u_10 + 1} (α := N₂) (((coweightEquiv P Q f).symm : (a : N) → N₂) ((P.coroot : (a : ι) → N) i : N) : N₂)
  ((Q.coroot : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂) : N₂)
Tactic: simp only [LinearEquiv.coe_coe, comp_apply, Equiv.symm_symm]
-- 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
i : ι
⊢ Eq.{u_10 + 1} (α := N₂) (((coweightEquiv P Q f).symm : (a : N) → N₂) ((P.coroot : (a : ι) → N) i : N) : N₂)
    ((Q.coroot : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂) : N₂)
have this : Eq (α := ι₂ → N)
  (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(↑f : P.Hom Q).coweightMap : (a : N₂) → N)
    (⇑Q.coroot : (a : ι₂) → N₂))
  (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
    (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι))
Tactic: have := f.coroot_coweightMap
-- 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
i : ι
this :
  Eq (α := ι₂ → N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(↑f : P.Hom Q).coweightMap : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂))
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι))
⊢ Eq.{u_10 + 1} (α := N₂) (((coweightEquiv P Q f).symm : (a : N) → N₂) ((P.coroot : (a : ι) → N) i : N) : N₂)
    ((Q.coroot : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂) : N₂)
have this₁ : ∀ (x : ι₂),
  Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(↑f : P.Hom Q).coweightMap : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂) x)
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
      (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) x)
Tactic: rw [funext_iff] 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
ι₂_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
i : ι
this :
  ∀ (x : ι₂),
    Eq.{u_4 + 1} (α := N)
      (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (β := N₂) (⇑(↑f : P.Hom Q).coweightMap : (a : N₂) → N)
        (⇑Q.coroot : (a : ι₂) → N₂) x)
      (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N)
        (⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) x)
⊢ Eq.{u_10 + 1} (α := N₂) (((coweightEquiv P Q f).symm : (a : N) → N₂) ((P.coroot : (a : ι) → N) i : N) : N₂)
    ((Q.coroot : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂) : N₂)
have this₁ : Eq.{u_4 + 1} (α := N)
  (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (α := ι₂) (β := N₂) (⇑(↑f : P.Hom Q).coweightMap : (a : N₂) → N)
    ((⇑Q.coroot : (a : ι₂) → N₂) : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂))
  (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (α := ι₂) (β := ι) (⇑P.coroot : (a : ι) → N)
    ((⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) : (a : ι₂) → ι)
    (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂))
Tactic: specialize this (f.indexEquiv i)
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
ι₂_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
i : ι
this :
  Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_8 + 1, u_10 + 1, u_4 + 1} (α := ι₂) (β := N₂) (⇑(↑f : P.Hom Q).coweightMap : (a : N₂) → N)
      ((⇑Q.coroot : (a : ι₂) → N₂) : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂))
    (Function.comp.{u_8 + 1, u_1 + 1, u_4 + 1} (α := ι₂) (β := ι) (⇑P.coroot : (a : ι) → N)
      ((⇑(↑f : P.Hom Q).indexEquiv.symm : (a : ι₂) → ι) : (a : ι₂) → ι)
      (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂))
⊢ Eq.{u_10 + 1} (α := N₂) (((coweightEquiv P Q f).symm : (a : N) → N₂) ((P.coroot : (a : ι) → N) i : N) : N₂)
    ((Q.coroot : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂) : N₂)
have this₁ : Eq.{u_4 + 1} (α := N)
  (((↑f : P.Hom Q).coweightMap : (a : N₂) → N)
      ((Q.coroot : (a : ι₂) → N₂) (((↑f : P.Hom Q).indexEquiv : (a : ι) → ι₂) i : ι₂) : N₂) :
    N)
  ((P.coroot : (a : ι) → N) i : N)
Tactic: simp only [comp_apply, 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
ι₂_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
⊢ Bijective.{u_9 + 1, u_3 + 1} (α := M₂) (β := M) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)
have simp : Bijective.{u_9 + 1, u_3 + 1} (α := M₂) (β := M) (⇑(weightEquiv P Q f).symm : (a : M₂) → M)
Tactic: simp only [LinearEquiv.coe_coe]
-- 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
⊢ Bijective.{u_4 + 1, u_10 + 1} (α := N) (β := N₂) (⇑(↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) : (a : N) → N₂)
have simp : Bijective.{u_4 + 1, u_10 + 1} (α := N) (β := N₂) (⇑(coweightEquiv P Q f).symm : (a : N) → N₂)
Tactic: simp only [LinearEquiv.coe_coe]
-- 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
⊢ symm P P e * e = 1
have weightMap : ∀ (m : M),
  Eq (α := M) (((↑(symm P P e * e) : P.Hom P).weightMap : (a : M) → M) m : M)
    ((Hom.weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P)
            (↑1 : P.Hom P) :
          (a : M) → M)
        m :
      M)
Tactic: ext 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
ι₂ : 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
e : P.Equiv P
weightMap :
  ∀ (m : M),
    Eq (α := M) (((↑(symm P P e * e) : P.Hom P).weightMap : (a : M) → M) m : M)
      ((Hom.weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P)
              (↑1 : P.Hom P) :
            (a : M) → M)
          m :
        M)
⊢ symm P P e * e = 1
have coweightMap : ∀ (m : N),
  Eq (α := N) (((↑(symm P P e * e) : P.Hom P).coweightMap : (a : N) → N) m : N)
    ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P)
            (↑1 : P.Hom P) :
          (a : N) → N)
        m :
      N)
Tactic: ext 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
ι₂ : 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
e : P.Equiv P
weightMap :
  ∀ (m : M),
    Eq (α := M) (((↑(symm P P e * e) : P.Hom P).weightMap : (a : M) → M) m : M)
      ((Hom.weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P)
              (↑1 : P.Hom P) :
            (a : M) → M)
          m :
        M)
coweightMap :
  ∀ (m : N),
    Eq (α := N) (((↑(symm P P e * e) : P.Hom P).coweightMap : (a : N) → N) m : N)
      ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P)
              (↑1 : P.Hom P) :
            (a : N) → N)
          m :
        N)
⊢ symm P P e * e = 1
have indexEquiv : ∀ (m : ι),
  Eq (α := ι) (((↑(symm P P e * e) : P.Hom P).indexEquiv : (a : ι) → ι) m : ι)
    ((Hom.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 : P.Hom P) :
          (a : ι) → ι)
        m :
      ι)
Tactic: ext 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
ι₂ : 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
e : P.Equiv P
m : M
⊢ Eq (α := M) (((↑(symm P P e * e) : P.Hom P).weightMap : (a : M) → M) m : M)
    ((Hom.weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P)
            (↑1 : P.Hom P) :
          (a : M) → M)
        m :
      M)
have weightMap : Eq (α := M) ((weightEquiv P P (symm P P e * e) : (a : M) → M) m : M)
  ((Hom.weightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (N := N) (ι₂ := ι) (N₂ := N) (P := P) (Q := P)
          (↑1 : P.Hom P) :
        (a : 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
m : N
⊢ Eq (α := N) (((↑(symm P P e * e) : P.Hom P).coweightMap : (a : N) → N) m : N)
    ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P)
            (↑1 : P.Hom P) :
          (a : N) → N)
        m :
      N)
have coweightMap : Eq (α := N) ((coweightEquiv P P (symm P P e * e) : (a : N) → N) m : N)
  ((Hom.coweightMap.{u_1, u_2, u_3, u_4, u_1, u_3, u_4} (ι := ι) (M := M) (ι₂ := ι) (M₂ := M) (P := P) (Q := P)
          (↑1 : P.Hom P) :
        (a : N) → N)
      m :
    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
ι₂ : 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_1 : RootPairing ι₂ R M₂ N₂
inst_9 : IsDomain R
inst_10 : CharZero R
inst_11 : Module.IsTorsionFree R M₂
inst_12 : Finite ι₂
P : RootPairing ι R M N
inst_13 : P.IsRootSystem
Q : RootPairing ι₂ R M₂ N₂
inst_14 : Q.IsRootSystem
f : M ≃ₗ[R] M₂
e : ι ≃ ι₂
hf :
  ∀ (i : ι),
    Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
      ((Q.root : (a : ι₂) → M₂) ((e : (a : ι) → ι₂) i : ι₂) : M₂)
⊢ (↑f : M →ₗ[R] M₂).dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ
      (↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N)
have h : ∀ (x : N₂) (x_1 : M),
  Eq.{u_2 + 1} (α := R)
    (((((↑f : M →ₗ[R] M₂).dualMap ∘ₗ (↑Q.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) : (a : N₂) → Module.Dual R M) x :
            Module.Dual R M) :
          (a : M) → R)
        x_1 :
      R)
    (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ
                  (↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) :
                (a : N₂) → Module.Dual R M)
              x :
            Module.Dual R M) :
          (a : M) → R)
        x_1 :
      R)
Tactic: ext