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 : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
f g : P.Aut
huv :
  ∀ (x : M),
    Eq (α := M)
      (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                    inv_val := ⋯ : P.Endˣ } :
                P.End).weightMap :
            (a : M) → M)
          x :
        M)
      (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                    { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
                P.End).weightMap :
            (a : M) → M)
          x :
        M)
⊢ { val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯, inv_val := ⋯ } =
    { val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
      { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }
have huv₁ : ∀ (x : N),
  Eq (α := N)
    (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := sorry,
                  inv_val := sorry : P.Endˣ } :
              P.End).coweightMap :
          (a : N) → N)
        x :
      N)
    (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := sorry, inv_val := sorry : P.Endˣ } *
                  { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := sorry, inv_val := sorry : P.Endˣ }) :
              P.End).coweightMap :
          (a : N) → N)
        x :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_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 g : P.Aut
huv :
  ∀ (x : M),
    Eq (α := M)
      (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                    inv_val := ⋯ : P.Endˣ } :
                P.End).weightMap :
            (a : M) → M)
          x :
        M)
      (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                    { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
                P.End).weightMap :
            (a : M) → M)
          x :
        M)
huv₁ :
  ∀ (x : N),
    Eq (α := N)
      (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯,
                    inv_val := ⋯ : P.Endˣ } :
                P.End).coweightMap :
            (a : N) → N)
          x :
        N)
      (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
                    { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }) :
                P.End).coweightMap :
            (a : N) → N)
          x :
        N)
⊢ { val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := ⋯, inv_val := ⋯ } =
    { val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ } *
      { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := ⋯, inv_val := ⋯ : P.Endˣ }
have huv₂ : ∀ (x : ι),
  Eq (α := ι)
    (((↑{ val := (↑f : P.Hom P).comp (↑g : P.Hom P), inv := (↑(symm P P (comp f g)) : P.Hom P), val_inv := sorry,
                  inv_val := sorry : P.Endˣ } :
              P.End).indexEquiv :
          (a : ι) → ι)
        x :
      ι)
    (((↑({ val := (↑f : P.Hom P), inv := (↑(symm P P f) : P.Hom P), val_inv := sorry, inv_val := sorry : P.Endˣ } *
                  { val := (↑g : P.Hom P), inv := (↑(symm P P g) : P.Hom P), val_inv := sorry, inv_val := sorry : P.Endˣ }) :
              P.End).indexEquiv :
          (a : ι) → ι)
        x :
      ι)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : 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
⊢ weightEquiv P P 1 = 1
have h : ∀ (x : M), Eq (α := M) ((weightEquiv P P 1 : (a : M) → M) x : M) ((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
x y : P.Aut
⊢ weightEquiv P P (x * y) = weightEquiv P P x * weightEquiv P P y
have h : ∀ (x_1 : M),
  Eq (α := M) ((weightEquiv P P (x * y) : (a : M) → M) x_1 : M)
    ((weightEquiv P P x * weightEquiv P P y : (a : M) → M) x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Injective (α := P.Aut) (β := M ≃ₗ[R] M) (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M)
have refine : ∀ (g g' : P.Aut)
  (hgg' :
    Eq.{u_3 + 1} (α := M →ₗ[R] M)
      (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
      (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')),
  g = g'
Tactic: refine Injective.of_comp (f := LinearEquiv.toLinearMap) fun g g' hgg' => ?_
-- 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
P : RootPairing ι R M N
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h : Eq.{u_3 + 1} (α := M →ₗ[R] M) (↑((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) g) : M →ₗ[R] M)
  (↑((weightHom P : (a : P.Aut) → M ≃ₗ[R] M) g') : M →ₗ[R] M) :=
  hgg'
⊢ g = g'
have h₁ : Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
  ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
Tactic: rw [weightHom_toLinearMap, weightHom_toLinearMap] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' :
  Eq.{u_3 + 1} (α := M →ₗ[R] M)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g)
    (Function.comp (β := M ≃ₗ[R] M) LinearEquiv.toLinearMap (⇑(weightHom P) : (a : P.Aut) → M ≃ₗ[R] M) g')
h :
  Eq.{u_3 + 1} (α := M →ₗ[R] M) ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g : P.Hom P) : Module.End R M)
    ((Hom.weightHom P : (a : P.End) → Module.End R M) (↑g' : P.Hom P) : Module.End R M)
⊢ g = g'
have suffices : (↑g : P.Hom P) = (↑g' : P.Hom P)
Tactic: suffices h' : g.toHom = g'.toHom by
    exact Equiv.ext hgg' (congrArg Hom.coweightMap h') (congrArg Hom.indexEquiv h')
-- 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
⊢ MulOpposite.op (coweightEquiv P P 1) = 1
have simp : coweightEquiv P P 1 = 1
Tactic: simp only [MulOpposite.op_eq_one_iff]
-- 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
⊢ ∀ (x y : P.Aut),
    MulOpposite.op (coweightEquiv P P (x * y)) =
      MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)
have simp : ∀ (x y : P.Aut),
  MulOpposite.op (coweightEquiv P P x ≪≫ₗ coweightEquiv P P y) =
    MulOpposite.op (coweightEquiv P P x) * MulOpposite.op (coweightEquiv P P y)
Tactic: simp only [mul_eq_comp, coweightEquiv_comp_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Injective (α := P.Aut) (β := (N ≃ₗ[R] N)ᵐᵒᵖ) (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)
have refine : ∀ (g g' : P.Aut)
  (hgg' :
    Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
      (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
      (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')),
  g = g'
Tactic: refine Injective.of_comp (f := fun a => MulOpposite.op a) fun g g' hgg' => ?_
-- 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
P : RootPairing ι R M N
g g' : P.Aut
hgg' :
  Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')
⊢ g = g'
have h : Eq.{u_4 + 1} (α := N →ₗ[R] N) (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g)) : N →ₗ[R] N)
  (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g')) : N →ₗ[R] N)
Tactic: have h : (MulOpposite.unop (coweightHom P g)).toLinearMap =
      (MulOpposite.unop (coweightHom P g')).toLinearMap := by
    simp_all
-- 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
P : RootPairing ι R M N
g g' : P.Aut
hgg' :
  Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')
h :
  Eq.{u_4 + 1} (α := N →ₗ[R] N) (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g)) : N →ₗ[R] N)
    (↑(MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g')) : N →ₗ[R] N)
⊢ g = g'
have h₁ : Eq.{u_4 + 1} (α := N →ₗ[R] N) (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g : P.Hom P)))
  (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g' : P.Hom P)))
Tactic: rw [coweightHom_toLinearMap, coweightHom_toLinearMap] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' :
  Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')
h :
  Eq.{u_4 + 1} (α := N →ₗ[R] N) (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g : P.Hom P)))
    (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g' : P.Hom P)))
⊢ g = g'
have suffices : (↑g : P.Hom P) = (↑g' : P.Hom P)
Tactic: suffices h' : g.toHom = g'.toHom by
    exact Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
g g' : P.Aut
hgg' :
  Eq.{u_4 + 1} (α := (N ≃ₗ[R] N)ᵐᵒᵖᵐᵒᵖ)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g)
    (((fun (a : (N ≃ₗ[R] N)ᵐᵒᵖ) ↦ MulOpposite.op a) ∘ (⇑(coweightHom P) : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ)) g')
h :
  Eq.{u_4 + 1} (α := N →ₗ[R] N) (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g : P.Hom P)))
    (MulOpposite.unop ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g' : P.Hom P)))
⊢ (↑g : P.Hom P) = (↑g' : P.Hom P)
have a : Eq.{u_4 + 1} (α := (N →ₗ[R] N)ᵐᵒᵖ) ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g : P.Hom P) : (N →ₗ[R] N)ᵐᵒᵖ)
  ((Hom.coweightHom P : (a : P.End) → (N →ₗ[R] N)ᵐᵒᵖ) (↑g' : P.Hom P) : (N →ₗ[R] N)ᵐᵒᵖ)
Tactic: apply Hom.coweightHom_injective P
-- 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
⊢ Eq.{u_1 + 1} (α := ι ≃ ι)
    (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))
    1
have H : ∀ (x : ι),
  Eq (α := ι)
    ((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 : ι) → ι)
        x :
      ι)
    ((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
x y : P.Aut
⊢ (↑(x * y) : P.Hom P).indexEquiv = (↑x : P.Hom P).indexEquiv * (↑y : P.Hom P).indexEquiv
have H : ∀ (x_1 : ι),
  Eq (α := ι) (((↑(x * y) : P.Hom P).indexEquiv : (a : ι) → ι) x_1 : ι)
    (((↑x : P.Hom P).indexEquiv * (↑y : P.Hom P).indexEquiv : (a : ι) → ι) x_1 : ι)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P_1 : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
P : RootPairing ι R M N
i : ι
⊢ (↑(P.reflection i) : M →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N)
have h : ∀ (f : N) (x : M),
  Eq.{u_2 + 1} (α := R)
    (((((↑(P.reflection i) : M →ₗ[R] M).dualMap ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) :
                (a : N) → Module.Dual R M)
              f :
            Module.Dual R M) :
          (a : M) → R)
        x :
      R)
    (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → Module.Dual R M)
              f :
            Module.Dual R M) :
          (a : M) → R)
        x :
      R)
Tactic: ext f x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_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
i : ι
⊢ Eq (α := ι → M) (Function.comp (β := M) (⇑(↑(P.reflection i) : M →ₗ[R] M) : (a : M) → M) (⇑P.root : (a : ι) → M))
    (Function.comp (β := ι) (⇑P.root : (a : ι) → M) (⇑(P.reflectionPerm i) : (a : ι) → ι))
have h : ∀ (x : ι),
  Eq (α := M) (Function.comp (β := M) (⇑(↑(P.reflection i) : M →ₗ[R] M) : (a : M) → M) (⇑P.root : (a : ι) → M) x)
    (Function.comp (β := ι) (⇑P.root : (a : ι) → M) (⇑(P.reflectionPerm i) : (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
i : ι
⊢ Eq (α := ι → N) (Function.comp (β := N) (⇑(↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → N) (⇑P.coroot : (a : ι) → N))
    (Function.comp (β := ι) (⇑P.coroot : (a : ι) → N) (⇑(P.reflectionPerm i).symm : (a : ι) → ι))
have h : ∀ (x : ι),
  Eq (α := N) (Function.comp (β := N) (⇑(↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → N) (⇑P.coroot : (a : ι) → N) x)
    (Function.comp (β := ι) (⇑P.coroot : (a : ι) → N) (⇑(P.reflectionPerm i).symm : (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
i : ι
⊢ Bijective (α := M) (β := M) (⇑(↑(P.reflection i) : M →ₗ[R] M) : (a : M) → M)
have simp : Bijective (α := M) (β := M) (⇑(P.reflection i) : (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
ι₂ : 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
i : ι
⊢ Bijective (α := N) (β := N) (⇑(↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → N)
have simp : Bijective (α := N) (β := N) (⇑(P.coreflection i) : (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
P : RootPairing ι R M N
i : ι
⊢ (reflection P i)⁻¹ = reflection P i
have refine_1 : (↑(reflection P i)⁻¹ : P.Hom P).weightMap = (↑(reflection P i) : P.Hom P).weightMap
Tactic: refine Equiv.ext ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
refine_1 : (↑(reflection P i)⁻¹ : P.Hom P).weightMap = (↑(reflection P i) : P.Hom P).weightMap
⊢ (reflection P i)⁻¹ = reflection P i
have refine_2 : (↑(reflection P i)⁻¹ : P.Hom P).coweightMap = (↑(reflection P i) : P.Hom P).coweightMap
Tactic: refine Equiv.ext ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i : ι
refine_1 : (↑(reflection P i)⁻¹ : P.Hom P).weightMap = (↑(reflection P i) : P.Hom P).weightMap
refine_2 : (↑(reflection P i)⁻¹ : P.Hom P).coweightMap = (↑(reflection P i) : P.Hom P).coweightMap
⊢ (reflection P i)⁻¹ = reflection P i
have refine_3 : (↑(reflection P i)⁻¹ : P.Hom P).indexEquiv = (↑(reflection P i) : P.Hom P).indexEquiv
Tactic: refine Equiv.ext ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
x y : N
⊢ w • (x + y) = w • x + w • y
have change : (unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) (x + y) =
  HAdd.hAdd (α := N) (β := N) ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) x : N)
    ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) y : N)
Tactic: change unop (coweightHom P _) (x + y) = unop (coweightHom P _) x + unop (coweightHom P _) y
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
w : P.Autᵐᵒᵖ
t : R
x : N
⊢ w • t • x = t • w • x
have change : (unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) (t • x) =
  HSMul.hSMul (β := N) t ((unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) (unop w)) : (a : N) → N) x : N)
Tactic: change unop (coweightHom P (unop w)) (t • x) = t • unop (coweightHom P (unop w)) x
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Irreducible (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Nontrivial M
⊢ Ne.{u_3 + 1} (α := ↥P.invtRootSubmodule) ⊥ ⊤
have rw : ¬Eq.{u_3 + 1} (α := Submodule R M) (↑⊥ : Submodule R M) (↑⊤ : Submodule R M)
Tactic: rw [ne_eq, Subtype.ext_iff]