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
ι₂ : 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
f : P.Aut
x : ι
⊢ Eq (α := ι) ((((↑f : P.Hom P) * (↑(symm P P f) : P.Hom P)).indexEquiv : (a : ι) → ι) x : ι)
    ((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 :
          (a : ι) → ι)
        x :
      ι)

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
f : P.Aut
weightMap :
  ∀ (x : M),
    Eq (α := M) ((((↑(symm P P f) : P.Hom P) * (↑f : P.Hom P)).weightMap : (a : M) → M) x : 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 :
            (a : M) → M)
          x :
        M)
coweightMap :
  ∀ (x : N),
    Eq (α := N) ((((↑(symm P P f) : P.Hom P) * (↑f : P.Hom P)).coweightMap : (a : N) → N) x : 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 :
            (a : N) → N)
          x :
        N)
indexEquiv :
  ∀ (x : ι),
    Eq (α := ι) ((((↑(symm P P f) : P.Hom P) * (↑f : P.Hom P)).indexEquiv : (a : ι) → ι) x : ι)
      ((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 :
            (a : ι) → ι)
          x :
        ι)
⊢ (↑(symm P P f) : P.Hom P) * (↑f : P.Hom P) = 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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
f : P.Aut
x : M
⊢ Eq (α := M) ((((↑(symm P P f) : P.Hom P) * (↑f : P.Hom P)).weightMap : (a : M) → M) x : 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 :
          (a : M) → M)
        x :
      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
f : P.Aut
x : N
⊢ Eq (α := N) ((((↑(symm P P f) : P.Hom P) * (↑f : P.Hom P)).coweightMap : (a : N) → N) x : 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 :
          (a : N) → N)
        x :
      N)

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
f : P.Aut
x : ι
⊢ Eq (α := ι) ((((↑(symm P P f) : P.Hom P) * (↑f : P.Hom P)).indexEquiv : (a : ι) → ι) x : ι)
    ((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 :
          (a : ι) → ι)
        x :
      ι)

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
f : P.Endˣ
⊢ Bijective (α := M) (β := M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
bijective_iff_has_inverse.mpr ?_

Premises used: Iff.mpr, Function.bijective_iff_has_inverse
-- 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
f : P.Endˣ
refine :
  ∃ (g : M → M),
    LeftInverse g (⇑(↑f : P.End).weightMap : (a : M) → M) ∧ RightInverse g (⇑(↑f : P.End).weightMap : (a : M) → M)
⊢ Bijective (α := M) (β := M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
refine bijective_iff_has_inverse.mpr ?_

Premises used: Iff.mpr, Function.bijective_iff_has_inverse
-- 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
f : P.Endˣ
h :
  LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M) ∧
    RightInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)
⊢ ∃ (g : M → M),
    LeftInverse g (⇑(↑f : P.End).weightMap : (a : M) → M) ∧ RightInverse g (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
use f.inv.weightMap

Premises used: RootPairing.Hom.weightMap, Units.inv
-- 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
f : P.Endˣ
h : LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)
h₁ : RightInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)
⊢ LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M) ∧
    RightInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
constructor
-- 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
f : P.Endˣ
⊢ LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
leftInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.leftInverse_iff_comp
-- 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
f : P.Endˣ
h :
  Eq (α := M → M) (Function.comp (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M))
    _root_.id
⊢ LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
refine leftInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.leftInverse_iff_comp
-- 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
f : P.Endˣ
h : Eq (α := M → M) (⇑(f.inv.weightMap ∘ₗ (↑f : P.End).weightMap) : (a : M) → M) _root_.id
⊢ Eq (α := M → M) (Function.comp (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M))
    _root_.id

Tactic:
simp only [← @LinearMap.coe_comp]

Premises used: LinearMap.coe_comp
-- 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
f : P.Endˣ
h : Eq (α := M → M) (⇑(f.inv * (↑f : P.End)).weightMap : (a : M) → M) _root_.id
h₁ :
  Eq.{u_3 + 1} (α := 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) :
      (a : M) → M)
    _root_.id
h₂ : Eq.{u_3 + 1} (α := M → M) (⇑LinearMap.id : (a : M) → M) _root_.id
h₃ h₄ : Eq.{u_3 + 1} (α := M → M) _root_.id _root_.id
⊢ Eq (α := M → M) (⇑(f.inv.weightMap ∘ₗ (↑f : P.End).weightMap) : (a : M) → M) _root_.id

Tactic:
rw [← Hom.weightMap_mul, f.inv_val, Hom.weightMap_one, LinearMap.id_coe]

Premises used: LinearMap.id_coe, Units.inv_val, RootPairing.Hom.weightMap_one, RootPairing.Hom.weightMap_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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
f : P.Endˣ
⊢ RightInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
rightInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.rightInverse_iff_comp
-- 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
f : P.Endˣ
h :
  Eq (α := M → M) (Function.comp (β := M) (⇑(↑f : P.End).weightMap : (a : M) → M) (⇑f.inv.weightMap : (a : M) → M))
    _root_.id
⊢ RightInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)

Tactic:
refine rightInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.rightInverse_iff_comp
-- 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
f : P.Endˣ
h : Eq (α := M → M) (⇑((↑f : P.End).weightMap ∘ₗ f.inv.weightMap) : (a : M) → M) _root_.id
⊢ Eq (α := M → M) (Function.comp (β := M) (⇑(↑f : P.End).weightMap : (a : M) → M) (⇑f.inv.weightMap : (a : M) → M))
    _root_.id

Tactic:
simp only [← @LinearMap.coe_comp]

Premises used: LinearMap.coe_comp
-- 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
f : P.Endˣ
h : Eq (α := M → M) (⇑((↑f : P.End) * f.inv).weightMap : (a : M) → M) _root_.id
h₁ :
  Eq.{u_3 + 1} (α := 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) :
      (a : M) → M)
    _root_.id
h₂ : Eq.{u_3 + 1} (α := M → M) (⇑LinearMap.id : (a : M) → M) _root_.id
h₃ h₄ : Eq.{u_3 + 1} (α := M → M) _root_.id _root_.id
⊢ Eq (α := M → M) (⇑((↑f : P.End).weightMap ∘ₗ f.inv.weightMap) : (a : M) → M) _root_.id

Tactic:
rw [← Hom.weightMap_mul, f.val_inv, Hom.weightMap_one, LinearMap.id_coe]

Premises used: LinearMap.id_coe, RootPairing.Hom.weightMap_one, RootPairing.Hom.weightMap_mul, Units.val_inv
-- 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
f : P.Endˣ
⊢ Bijective (α := N) (β := N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
bijective_iff_has_inverse.mpr ?_

Premises used: Iff.mpr, Function.bijective_iff_has_inverse
-- 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
f : P.Endˣ
refine :
  ∃ (g : N → N),
    LeftInverse g (⇑(↑f : P.End).coweightMap : (a : N) → N) ∧ RightInverse g (⇑(↑f : P.End).coweightMap : (a : N) → N)
⊢ Bijective (α := N) (β := N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
refine bijective_iff_has_inverse.mpr ?_

Premises used: Iff.mpr, Function.bijective_iff_has_inverse
-- 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
f : P.Endˣ
h :
  LeftInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N) ∧
    RightInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)
⊢ ∃ (g : N → N),
    LeftInverse g (⇑(↑f : P.End).coweightMap : (a : N) → N) ∧ RightInverse g (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
use f.inv.coweightMap

Premises used: Units.inv, RootPairing.Hom.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
ι₂ : 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
f : P.Endˣ
h : LeftInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)
h₁ : RightInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)
⊢ LeftInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N) ∧
    RightInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
constructor
-- 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
f : P.Endˣ
⊢ LeftInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
leftInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.leftInverse_iff_comp
-- 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
f : P.Endˣ
h :
  Eq (α := N → N) (Function.comp (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N))
    _root_.id
⊢ LeftInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
refine leftInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.leftInverse_iff_comp
-- 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
f : P.Endˣ
h : Eq (α := N → N) (⇑(f.inv.coweightMap ∘ₗ (↑f : P.End).coweightMap) : (a : N) → N) _root_.id
⊢ Eq (α := N → N) (Function.comp (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N))
    _root_.id

Tactic:
simp only [← @LinearMap.coe_comp]

Premises used: LinearMap.coe_comp
-- 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
f : P.Endˣ
h : Eq (α := N → N) (⇑((↑f : P.End) * f.inv).coweightMap : (a : N) → N) _root_.id
h₁ :
  Eq.{u_4 + 1} (α := N → 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) :
      (a : N) → N)
    _root_.id
h₂ : Eq.{u_4 + 1} (α := N → N) (⇑LinearMap.id : (a : N) → N) _root_.id
h₃ h₄ : Eq.{u_4 + 1} (α := N → N) _root_.id _root_.id
⊢ Eq (α := N → N) (⇑(f.inv.coweightMap ∘ₗ (↑f : P.End).coweightMap) : (a : N) → N) _root_.id

Tactic:
rw [← Hom.coweightMap_mul, f.val_inv, Hom.coweightMap_one, LinearMap.id_coe]

Premises used: RootPairing.Hom.coweightMap_mul, LinearMap.id_coe, RootPairing.Hom.coweightMap_one, Units.val_inv
-- 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
f : P.Endˣ
⊢ RightInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
rightInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.rightInverse_iff_comp
-- 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
f : P.Endˣ
h :
  Eq (α := N → N) (Function.comp (β := N) (⇑(↑f : P.End).coweightMap : (a : N) → N) (⇑f.inv.coweightMap : (a : N) → N))
    _root_.id
⊢ RightInverse (α := N) (β := N) (⇑f.inv.coweightMap : (a : N) → N) (⇑(↑f : P.End).coweightMap : (a : N) → N)

Tactic:
refine rightInverse_iff_comp.mpr ?_

Premises used: Iff.mpr, Function.rightInverse_iff_comp
-- 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
f : P.Endˣ
h : Eq (α := N → N) (⇑((↑f : P.End).coweightMap ∘ₗ f.inv.coweightMap) : (a : N) → N) _root_.id
⊢ Eq (α := N → N) (Function.comp (β := N) (⇑(↑f : P.End).coweightMap : (a : N) → N) (⇑f.inv.coweightMap : (a : N) → N))
    _root_.id

Tactic:
simp only [← @LinearMap.coe_comp]

Premises used: LinearMap.coe_comp
-- 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
f : P.Endˣ
h : Eq (α := N → N) (⇑(f.inv * (↑f : P.End)).coweightMap : (a : N) → N) _root_.id
h₁ :
  Eq.{u_4 + 1} (α := N → 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) :
      (a : N) → N)
    _root_.id
h₂ : Eq.{u_4 + 1} (α := N → N) (⇑LinearMap.id : (a : N) → N) _root_.id
h₃ h₄ : Eq.{u_4 + 1} (α := N → N) _root_.id _root_.id
⊢ Eq (α := N → N) (⇑((↑f : P.End).coweightMap ∘ₗ f.inv.coweightMap) : (a : N) → N) _root_.id

Tactic:
rw [← Hom.coweightMap_mul, f.inv_val, Hom.coweightMap_one, LinearMap.id_coe]

Premises used: RootPairing.Hom.coweightMap_mul, LinearMap.id_coe, Units.inv_val, RootPairing.Hom.coweightMap_one
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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
f : P.Aut
⊢ (fun (f : P.Endˣ) ↦
        let __src := (↑f : P.End);
        { toHom := __src, bijective_weightMap := ⋯, bijective_coweightMap := ⋯ : P.Equiv P })
      ((fun (f : P.Aut) ↦
          { val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ })
        f) =
    f

Tactic:
simp