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
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)
⊢ 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

Premises used: RootPairing.Equiv.coweightHom_toLinearMap
-- 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
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)))
h' : (↑g : P.Hom P) = (↑g' : P.Hom P)
⊢ g = g'

Tactic:
Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')

Premises used: RootPairing.Hom.indexEquiv, congrArg, RootPairing.Equiv.ext, RootPairing.Hom.weightMap
-- 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
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)))
h' : (↑g : P.Hom P) = (↑g' : P.Hom P)
⊢ g = g'

Tactic:
exact Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')

Premises used: RootPairing.Hom.indexEquiv, congrArg, RootPairing.Equiv.ext, RootPairing.Hom.weightMap
-- 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
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)))
suffices : (↑g : P.Hom P) = (↑g' : P.Hom P)
⊢ g = g'

Tactic:
suffices h' : g.toHom = g'.toHom by
    exact Equiv.ext (congrArg Hom.weightMap h') h (congrArg Hom.indexEquiv h')
-- 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
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)))
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)ᵐᵒᵖ)
⊢ (↑g : P.Hom P) = (↑g' : P.Hom P)

Tactic:
apply Hom.coweightHom_injective P

Premises used: RootPairing.Hom.coweightHom_injective
-- 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
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)))
⊢ 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:
MulOpposite.unop_inj.mp h

Premises used: Iff.mp, MulOpposite.unop_inj
-- 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
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)))
⊢ 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:
exact MulOpposite.unop_inj.mp h

Premises used: Iff.mp, MulOpposite.unop_inj
-- 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
P : RootPairing ι R M N
g : P.Aut
⊢ MulOpposite.unop ((coweightHom P : (a : P.Aut) → (N ≃ₗ[R] N)ᵐᵒᵖ) g) = coweightEquiv P P g

Tactic:
rfl

Premises used: RootPairing.Equiv.coweightEquiv, MulOpposite.unop, LinearEquiv.trans, rfl, LinearEquiv.ofBijective
-- 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
P : RootPairing ι R M N
g : P.Aut
⊢ coweightEquiv P P g⁻¹ = (coweightEquiv P P g)⁻¹

Tactic:
LinearEquiv.toLinearMap_inj.mp rfl

Premises used: LinearEquiv.toLinearMap_inj, Iff.mp, 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
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 : ι)
⊢ 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

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
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:
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
x y : P.Aut
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 : ι)
⊢ (↑(x * y) : P.Hom P).indexEquiv = (↑x : P.Hom P).indexEquiv * (↑y : P.Hom P).indexEquiv

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
x y : P.Aut
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:
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
P : RootPairing ι R M N
g : P.Aut
⊢ (↑g⁻¹ : P.Hom P).indexEquiv = ((indexHom P : (a : P.Aut) → ι ≃ ι) g)⁻¹

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_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 : ι
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)
⊢ (↑(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)

Tactic:
ext f x
-- 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
i : ι
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:
simpa [reflection_apply, coreflection_apply] using mul_comm ..

Premises used: RootPairing.coreflection_apply, mul_comm, RootPairing.reflection_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
i : ι
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)
⊢ 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 : ι) → ι))

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
i 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:
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
i : ι
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)
⊢ 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 : ι) → ι))

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
i 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:
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
i : ι
simp : Bijective (α := M) (β := M) (⇑(P.reflection i) : (a : M) → M)
⊢ Bijective (α := M) (β := M) (⇑(↑(P.reflection i) : 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
ι₂ : 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) : (a : M) → M)

Tactic:
LinearEquiv.bijective (P.reflection i)

Premises used: LinearEquiv.bijective, RootPairing.reflection
-- 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
i : ι
⊢ Bijective (α := M) (β := M) (⇑(P.reflection i) : (a : M) → M)

Tactic:
exact LinearEquiv.bijective (P.reflection i)

Premises used: LinearEquiv.bijective, RootPairing.reflection
-- 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
i : ι
simp : Bijective (α := N) (β := N) (⇑(P.coreflection i) : (a : N) → N)
⊢ Bijective (α := N) (β := N) (⇑(↑(P.coreflection i) : 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
ι₂ : 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) : (a : N) → N)

Tactic:
LinearEquiv.bijective (P.coreflection i)

Premises used: RootPairing.coreflection, LinearEquiv.bijective
-- 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
i : ι
⊢ Bijective (α := N) (β := N) (⇑(P.coreflection i) : (a : N) → N)

Tactic:
exact LinearEquiv.bijective (P.coreflection i)

Premises used: RootPairing.coreflection, LinearEquiv.bijective
-- 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
P : RootPairing ι R M N
i : ι
⊢ weightEquiv P P (reflection P i) = P.reflection i

Tactic:
LinearEquiv.toLinearMap_inj.mp rfl

Premises used: LinearEquiv.toLinearMap_inj, Iff.mp, 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
P : RootPairing ι R M N
i : ι
⊢ coweightEquiv P P (reflection P i) = P.coreflection i

Tactic:
LinearEquiv.toLinearMap_inj.mp rfl

Premises used: LinearEquiv.toLinearMap_inj, Iff.mp, 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
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i) : P.Hom P).indexEquiv = P.reflectionPerm i

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
P : RootPairing ι R M N
i : ι
⊢ (reflection P i)⁻¹ = reflection P i

Tactic:
Equiv.ext ?_ ?_ ?_

Premises used: RootPairing.Equiv.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
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
refine_3 : (↑(reflection P i)⁻¹ : P.Hom P).indexEquiv = (↑(reflection P i) : P.Hom P).indexEquiv
⊢ (reflection P i)⁻¹ = reflection P i

Tactic:
refine Equiv.ext ?_ ?_ ?_

Premises used: RootPairing.Equiv.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
P : RootPairing ι R M N
i : ι
x : M
⊢ Eq (α := M) (((↑(reflection P i)⁻¹ : P.Hom P).weightMap : (a : M) → M) x : M)
    (((↑(reflection P i) : P.Hom P).weightMap : (a : M) → M) x : M)

Tactic:
simp [← 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
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹ : P.Hom P).weightMap = (↑(reflection P i) : P.Hom P).weightMap

Tactic:
exact LinearMap.ext_iff.mpr (fun x => by simp [← weightEquiv_apply])

Premises used: Iff.mpr, LinearMap.ext_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
P : RootPairing ι R M N
i : ι
x : N
⊢ Eq (α := N) (((↑(reflection P i)⁻¹ : P.Hom P).coweightMap : (a : N) → N) x : N)
    (((↑(reflection P i) : P.Hom P).coweightMap : (a : N) → N) x : N)

Tactic:
simp [← coweightEquiv_apply]

Premises used: RootPairing.Equiv.coweightEquiv_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
P : RootPairing ι R M N
i : ι
⊢ (↑(reflection P i)⁻¹ : P.Hom P).coweightMap = (↑(reflection P i) : P.Hom P).coweightMap

Tactic:
exact LinearMap.ext_iff.mpr (fun x => by simp [← coweightEquiv_apply])

Premises used: Iff.mpr, LinearMap.ext_iff