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
ι₂_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_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)

Premises used: RootPairing.Hom.indexEquiv, RootPairing.Equiv.toHom, Equiv.symm, 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
ι₂_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_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

Premises used: Equiv.apply_symm_apply, Function.comp_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
ι₂_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₂)
    (((↑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₂)
⊢ 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 [← this]
-- 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
ι₂_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
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)
⊢ 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 : ι) → ι₂))

Tactic:
ext i
-- 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
ι₂_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 : ι
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₂)
⊢ 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:
simp only [LinearEquiv.coe_coe, comp_apply, Equiv.symm_symm]

Premises used: Equiv.symm_symm, Function.comp_apply, LinearEquiv.coe_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
ι₂_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 (α := ι₂ → 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
-- 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
ι₂_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 : ι₂) → ι))
⊢ ∀ (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

Premises used: funext_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂_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_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)

Premises used: RootPairing.Hom.indexEquiv, RootPairing.Equiv.toHom, 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
ι₂_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_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

Premises used: Equiv.symm_apply_apply, Function.comp_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
ι₂_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)
    (((↑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)
⊢ 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 [← this]
-- 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
ι₂_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
simp : Bijective.{u_9 + 1, u_3 + 1} (α := M₂) (β := M) (⇑(weightEquiv P Q f).symm : (a : M₂) → M)
⊢ Bijective.{u_9 + 1, u_3 + 1} (α := M₂) (β := M) (⇑(↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M) : (a : M₂) → M)

Tactic:
simp only [LinearEquiv.coe_coe]

Premises used: LinearEquiv.coe_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
ι₂_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 : (a : M₂) → M)

Tactic:
LinearEquiv.bijective (weightEquiv P Q f).symm

Premises used: LinearEquiv.symm, LinearEquiv.bijective, RootPairing.Equiv.weightEquiv
-- 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
ι₂_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 : (a : M₂) → M)

Tactic:
exact LinearEquiv.bijective (weightEquiv P Q f).symm

Premises used: LinearEquiv.symm, LinearEquiv.bijective, RootPairing.Equiv.weightEquiv
-- 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
ι₂_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
simp : Bijective.{u_4 + 1, u_10 + 1} (α := N) (β := N₂) (⇑(coweightEquiv P Q f).symm : (a : N) → N₂)
⊢ Bijective.{u_4 + 1, u_10 + 1} (α := N) (β := N₂) (⇑(↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂) : (a : N) → N₂)

Tactic:
simp only [LinearEquiv.coe_coe]

Premises used: LinearEquiv.coe_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
ι₂_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 : (a : N) → N₂)

Tactic:
LinearEquiv.bijective (coweightEquiv P Q f).symm

Premises used: LinearEquiv.symm, LinearEquiv.bijective, RootPairing.Equiv.coweightEquiv
-- 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
ι₂_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 : (a : N) → N₂)

Tactic:
exact LinearEquiv.bijective (coweightEquiv P Q f).symm

Premises used: LinearEquiv.symm, LinearEquiv.bijective, RootPairing.Equiv.coweightEquiv
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_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
⊢ (↑(symm P Q f) : Q.Hom P).weightMap = (↑(weightEquiv P Q f).symm : M₂ →ₗ[R] M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_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
⊢ (↑(symm P Q f) : Q.Hom P).coweightMap = (↑(coweightEquiv P Q f).symm : N →ₗ[R] N₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_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
⊢ (↑(symm P Q f) : Q.Hom P).indexEquiv = (↑f : P.Hom Q).indexEquiv.symm

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
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)
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 :
        ι)
⊢ symm P P e * e = 1

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
m : M
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)
⊢ 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:
rw [← weightEquiv_apply]

Premises used: RootPairing.Equiv.weightEquiv_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
ι₂ : 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) ((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:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
e : P.Equiv P
m : N
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)
⊢ 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:
rw [← coweightEquiv_apply]

Premises used: RootPairing.Equiv.coweightEquiv_apply