awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_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₂)
⊢ Eq (α := ι → M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂) (⇑P.root : (a : ι) → M))
    (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂) (⇑e : (a : ι) → ι₂))
have h : ∀ (x : ι),
  Eq.{u_6 + 1} (α := M₂)
    (Function.comp.{u_1 + 1, u_3 + 1, u_6 + 1} (β := M) (⇑(↑f : M →ₗ[R] M₂) : (a : M) → M₂) (⇑P.root : (a : ι) → M) x)
    (Function.comp.{u_1 + 1, u_5 + 1, u_6 + 1} (β := ι₂) (⇑Q.root : (a : ι₂) → M₂) (⇑e : (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
ι₂ : 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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
⊢ Eq (α := ι₂ → N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂))
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι))
have h : ∀ (i : ι₂),
  Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂) i)
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.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
ι₂ : 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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
⊢ Eq.{u_4 + 1} (α := N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂) i)
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i)
have h : Eq.{u_7 + 1} (α := N₂) ((Q.coroot : (a : ι₂) → N₂) i : N₂)
  ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
      (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
    N₂)
Tactic: rw [LinearEquiv.coe_coe, comp_apply, ← LinearEquiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
| ((Q.coroot : (a : ι₂) → N₂) i : N₂)
have rw : (((RootPairing.map (P := P) e f g).coroot : (a : ι₂) → N₂) i : N₂)
Tactic: rw [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
ι₂ : 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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
this : Q = RootPairing.map (P := P) e f g
i : ι₂
⊢ Eq.{u_7 + 1} (α := N₂) ((Q.coroot : (a : ι₂) → N₂) i : N₂)
    ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
        (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
      N₂)
have h : Eq.{u_7 + 1} (α := N₂) (((RootPairing.map (P := P) e f g).coroot : (a : ι₂) → N₂) i : N₂)
  ((LinearEquiv.symm (Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : (a : N) → N₂)
      (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι) i) :
    N₂)
Tactic: conv_lhs => rw [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
ι₂ : 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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
⊢ Eq (α := ι₂ → N)
    (Function.comp.{u_5 + 1, u_7 + 1, u_4 + 1} (β := N₂)
      (⇑(↑(Q.flip.toPerfPair ≪≫ₗ (f.dualMap ≪≫ₗ P.flip.toPerfPair.symm)) : N₂ →ₗ[R] N) : (a : N₂) → N)
      (⇑Q.coroot : (a : ι₂) → N₂))
    (Function.comp.{u_5 + 1, u_1 + 1, u_4 + 1} (β := ι) (⇑P.coroot : (a : ι) → N) (⇑e.symm : (a : ι₂) → ι))
have suffices : Q = RootPairing.map (P := P) e f g
Tactic: suffices Q = P.map e f g by
      ext i
      rw [LinearEquiv.coe_coe, comp_apply, ← LinearEquiv.eq_symm_apply]
      conv_lhs => rw [this]
      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
ι₂ : 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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
⊢ Q = RootPairing.map (P := P) e f g
have he : Q.toLinearMap = (RootPairing.map (P := P) e f g).toLinearMap
Tactic: apply IsRootSystem.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_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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
he : Q.toLinearMap = (RootPairing.map (P := P) e f g).toLinearMap
⊢ Q = RootPairing.map (P := P) e f g
have hr : Q.root = (RootPairing.map (P := P) e f g).root
Tactic: apply IsRootSystem.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_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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
⊢ Q.toLinearMap = (RootPairing.map (P := P) e f g).toLinearMap
have he : ∀ (x : M₂) (x_1 : N₂),
  Eq.{u_2 + 1} (α := R) ((((Q.toLinearMap : (a : M₂) → N₂ →ₗ[R] R) x : N₂ →ₗ[R] R) : (a : N₂) → R) x_1 : R)
    (((((RootPairing.map (P := P) e f g).toLinearMap : (a : M₂) → N₂ →ₗ[R] R) x : N₂ →ₗ[R] R) : (a : N₂) → R) x_1 : R)
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_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₂)
g : N ≃ₗ[R] N₂ := P.flip.toPerfPair ≪≫ₗ (f.symm.dualMap ≪≫ₗ Q.flip.toPerfPair.symm)
⊢ Q.root = (RootPairing.map (P := P) e f g).root
have hr : ∀ (x : ι₂),
  Eq.{u_6 + 1} (α := M₂) ((Q.root : (a : ι₂) → M₂) x : M₂)
    (((RootPairing.map (P := P) e f g).root : (a : ι₂) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
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
⊢ (↑f : P.Hom P) * (↑(symm P P f) : P.Hom P) = 1
have weightMap : ∀ (x : M),
  Eq (α := M) ((((↑f : P.Hom P) * (↑(symm P 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: 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Aut
weightMap :
  ∀ (x : M),
    Eq (α := M) ((((↑f : P.Hom P) * (↑(symm P 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)
⊢ (↑f : P.Hom P) * (↑(symm P P f) : P.Hom P) = 1
have coweightMap : ∀ (x : N),
  Eq (α := N) ((((↑f : P.Hom P) * (↑(symm P 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: 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Aut
weightMap :
  ∀ (x : M),
    Eq (α := M) ((((↑f : P.Hom P) * (↑(symm P 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) ((((↑f : P.Hom P) * (↑(symm P 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)
⊢ (↑f : P.Hom P) * (↑(symm P P f) : P.Hom P) = 1
have indexEquiv : ∀ (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: 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_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f : P.Aut
⊢ (↑(symm P P f) : P.Hom P) * (↑f : P.Hom P) = 1
have 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)
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_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)
⊢ (↑(symm P P f) : P.Hom P) * (↑f : P.Hom P) = 1
have 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)
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_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)
⊢ (↑(symm P P f) : P.Hom P) * (↑f : P.Hom P) = 1
have 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 :
      ι)
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_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)
have refine : ∃ (g : M → M),
  LeftInverse g (⇑(↑f : P.End).weightMap : (a : M) → M) ∧ RightInverse g (⇑(↑f : P.End).weightMap : (a : M) → M)
Tactic: refine bijective_iff_has_inverse.mpr ?_
-- 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
f : P.Endˣ
⊢ ∃ (g : M → M),
    LeftInverse g (⇑(↑f : P.End).weightMap : (a : M) → M) ∧ RightInverse g (⇑(↑f : P.End).weightMap : (a : M) → M)
have 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)
Tactic: use f.inv.weightMap
-- 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
f : P.Endˣ
⊢ 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)
have h : LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)
Tactic: constructor
-- 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
f : P.Endˣ
h : LeftInverse (α := 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)
have h₁ : RightInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)
Tactic: constructor
-- 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
f : P.Endˣ
⊢ LeftInverse (α := M) (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M)
have h : Eq (α := M → M) (Function.comp (β := M) (⇑f.inv.weightMap : (a : M) → M) (⇑(↑f : P.End).weightMap : (a : M) → M))
  _root_.id
Tactic: refine leftInverse_iff_comp.mpr ?_