awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
H :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) : M)
    ((P.root : (a : ι) → M) ((1 : (a : ι) → ι) j : ι) : M)
⊢ Eq (α := ι) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) ((1 : (a : ι) → ι) j : ι)

Tactic:
apply P.root.injective

Premises used: RootPairing.root, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) : M)
    ((P.root : (a : ι) → M) ((1 : (a : ι) → ι) j : ι) : M)

Tactic:
simp only [sq, Equiv.Perm.mul_apply, root_reflectionPerm, reflection_same, Equiv.Perm.one_apply]

Premises used: RootPairing.reflection_same, sq, Equiv.Perm.one_apply, Equiv.Perm.mul_apply, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.reflectionPerm i)⁻¹ = P.reflectionPerm i

Tactic:
(mul_eq_one_iff_eq_inv.mp <| P.reflectionPerm_sq i).symm

Premises used: RootPairing.reflectionPerm_sq, mul_eq_one_iff_eq_inv, Iff.mp, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
a :
  Eq.{u_3 + 1} (α := M)
    ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : ι) : M)
    ((P.root : (a : ι) → M) j : M)
⊢ (P.reflectionPerm i : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) j : ι) = j

Tactic:
apply P.root.injective

Premises used: RootPairing.root, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
⊢ Eq.{u_3 + 1} (α := M)
    ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : ι) : M)
    ((P.root : (a : ι) → M) j : M)

Tactic:
simp only [root_reflectionPerm, reflection_same]

Premises used: RootPairing.reflection_same, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
h : ∀ (x : ι), (⇑(P.reflectionPerm i) : (a : ι) → ι)^[2] x = id x
⊢ Eq (α := ι → ι) (⇑(P.reflectionPerm i) : (a : ι) → ι)^[2] id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (⇑(P.reflectionPerm i) : (a : ι) → ι)^[2] x = id x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.reflectionPerm i).symm = P.reflectionPerm i

Tactic:
Involutive.symm_eq_self_of_involutive (P.reflectionPerm i) <| P.reflectionPerm_involutive i

Premises used: RootPairing.reflectionPerm_involutive, Function.Involutive.symm_eq_self_of_involutive, RootPairing.reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ BijOn (α := M) (β := M) (⇑(P.reflection i) : (a : M) → M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))

Tactic:
Module.bijOn_reflection_of_mapsTo _ <| P.mapsTo_reflection_root i

Premises used: Module.bijOn_reflection_of_mapsTo, RootPairing.mapsTo_reflection_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Eq (α := Set M)
    (image (α := M) (⇑(P.reflection i) : (a : M) → M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))

Tactic:
(P.bijOn_reflection_root i).image_eq

Premises used: RootPairing.bijOn_reflection_root, Set.BijOn.image_eq
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)

Tactic:
(P.reflectionPerm_coroot i j).symm

Premises used: RootPairing.reflectionPerm_coroot, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
⊢ Membership.mem (α := N) (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)

Tactic:
P.coroot_reflectionPerm i j ▸ mem_range_self (P.reflectionPerm i j)

Premises used: Set.mem_range_self, Eq.rec, RootPairing.reflectionPerm, DFunLike.coe, RootPairing.coroot_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
⊢ Membership.mem (α := N) (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)

Tactic:
exact P.coroot_reflectionPerm i j ▸ mem_range_self (P.reflectionPerm i j)
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
f : N
⊢ (P.coreflection i : (a : N) → N) f =
    f - HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) ((P.root' i : (a : N) → R) f : R) ((P.coroot : (a : ι) → N) i : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
⊢ (P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) =
    HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
      (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N))

Tactic:
rfl

Premises used: RootPairing.pairing, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Eq (α := N) ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) i : N) : N) (-(P.coroot : (a : ι) → N) i : N)

Tactic:
Module.reflection_apply_self (P.flip.coroot_root_two i)

Premises used: Module.reflection_apply_self, RootPairing.flip, RootPairing.coroot_root_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
⊢ (P.coreflection i : (a : N) → N) ((P.coreflection i : (a : N) → N) x : N) = x

Tactic:
Module.involutive_reflection (P.flip.coroot_root_two i) x

Premises used: RootPairing.flip, Module.involutive_reflection, RootPairing.coroot_root_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.coreflection i)⁻¹ = P.coreflection i

Tactic:
rfl

Premises used: RootPairing.coreflection, LinearEquiv.symm, Module.preReflection, Module.reflection, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ HPow.hPow (β := ℕ) (P.coreflection i) 2 = 1

Tactic:
mul_eq_one_iff_eq_inv.mpr rfl

Premises used: Iff.mpr, mul_eq_one_iff_eq_inv, npowRec, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ BijOn (α := N) (β := N) (⇑(P.coreflection i) : (a : N) → N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))

Tactic:
bijOn_reflection_root P.flip i

Premises used: RootPairing.flip, RootPairing.bijOn_reflection_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Eq (α := Set N)
    (image (α := N) (⇑(P.coreflection i) : (a : N) → N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))

Tactic:
(P.bijOn_coreflection_coroot i).image_eq

Premises used: Set.BijOn.image_eq, RootPairing.bijOn_coreflection_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ P.coreflection i = P.flip.reflection i

Tactic:
rfl

Premises used: RootPairing.coreflection, RootPairing.reflection, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
h :
  ∀ (x : M),
    Eq (α := M) ((P.reflection ((P.reflectionPerm j : (a : ι) → ι) i) : (a : M) → M) x : M)
      ((P.reflection j * P.reflection i * P.reflection j : (a : M) → M) x : M)
⊢ P.reflection ((P.reflectionPerm j : (a : ι) → ι) i) = P.reflection j * P.reflection i * P.reflection j

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
x : M
h :
  x -
      HSub.hSub (α := R)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
          (HMul.hMul (β := R) (P.pairing j i)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
              R)) •
        HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    x -
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
            ((P.root : (a : ι) → M) j : M) -
        HSMul.hSMul (β := M)
          (HSub.hSub (α := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
            (HMul.hMul (α := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
                R)
              (P.pairing j i)))
          ((P.root : (a : ι) → M) i : M) -
      HSMul.hSMul (β := M)
        (HSub.hSub (α := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
            (HMul.hMul (α := R) (β := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
                R)
              (2 : R)) -
          HSub.hSub (α := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) :
                R)
              (HMul.hMul (α := R)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) j : N) :
                  R)
                (P.pairing j i)) *
            P.pairing i j)
        ((P.root : (a : ι) → M) j : M)
⊢ Eq (α := M) ((P.reflection ((P.reflectionPerm j : (a : ι) → ι) i) : (a : M) → M) x : M)
    ((P.reflection j * P.reflection i * P.reflection j : (a : M) → M) x : M)

Tactic:
simp [reflection_apply, coreflection_apply]

Premises used: RootPairing.coreflection_apply, RootPairing.reflection_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
x : M
⊢ x -
      HSub.hSub (α := R)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
          (HMul.hMul (β := R) (P.pairing j i)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
              R)) •
        HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
          (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    x -
          HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
            ((P.root : (a : ι) → M) j : M) -
        HSMul.hSMul (β := M)
          (HSub.hSub (α := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
            (HMul.hMul (α := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
                R)
              (P.pairing j i)))
          ((P.root : (a : ι) → M) i : M) -
      HSMul.hSMul (β := M)
        (HSub.hSub (α := R)
            ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
            (HMul.hMul (α := R) (β := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) :
                R)
              (2 : R)) -
          HSub.hSub (α := R)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) :
                R)
              (HMul.hMul (α := R)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) j : N) :
                  R)
                (P.pairing j i)) *
            P.pairing i j)
        ((P.root : (a : ι) → M) j : M)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
h :
  ∀ (n : N) (m : M),
    Eq.{u_2 + 1} (α := R)
      (((((↑(P.reflection i).dualMap : Dual R M →ₗ[R] Dual R M) ∘ₗ P.flip : (a : N) → M →ₗ[R] R) n : M →ₗ[R] R) :
            (a : M) → R)
          m :
        R)
      ((((P.flip ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) m : R)
⊢ (↑(P.reflection i).dualMap : Dual R M →ₗ[R] Dual R M) ∘ₗ P.flip = P.flip ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N)

Tactic:
ext n m
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
n : N
m : M
⊢ Eq.{u_2 + 1} (α := R)
    (((((↑(P.reflection i).dualMap : Dual R M →ₗ[R] Dual R M) ∘ₗ P.flip : (a : N) → M →ₗ[R] R) n : M →ₗ[R] R) :
          (a : M) → R)
        m :
      R)
    ((((P.flip ∘ₗ (↑(P.coreflection i) : N →ₗ[R] N) : (a : N) → M →ₗ[R] R) n : M →ₗ[R] R) : (a : M) → R) m : R)

Tactic:
simp [map_sub, coreflection_apply, reflection_apply, mul_comm (P.toLinearMap m (P.coroot i))]

Premises used: map_sub, RootPairing.toLinearMap, RootPairing.coreflection_apply, mul_comm, RootPairing.coroot, RootPairing.reflection_apply, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j k : ι
hk :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) k : M)
    ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)
⊢ k = (P.reflectionPerm i : (a : ι) → ι) j

Tactic:
rw [← P.root_reflectionPerm, EmbeddingLike.apply_eq_iff_eq] at hk

Premises used: EmbeddingLike.apply_eq_iff_eq, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j k : ι
hk : k = (P.reflectionPerm i : (a : ι) → ι) j
rw :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
    ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
    ((P.coroot : (a : ι) → N) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) k : N)
    ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) j : N) : N)

Tactic:
rw [← P.coroot_reflectionPerm, hk]

Premises used: RootPairing.coroot_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
h :
  ∀ (y : M),
    Eq.{u_2 + 1} (α := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) j) : (a : M) → R) y : R)
      ((P.coroot' j ∘ₗ (↑(P.reflection i) : M →ₗ[R] M) : (a : M) → R) y : R)
⊢ P.coroot' ((P.reflectionPerm i : (a : ι) → ι) j) = P.coroot' j ∘ₗ (↑(P.reflection i) : M →ₗ[R] M)

Tactic:
ext y
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
y : M
⊢ Eq.{u_2 + 1} (α := R) ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) j) : (a : M) → R) y : R)
    ((P.coroot' j ∘ₗ (↑(P.reflection i) : M →ₗ[R] M) : (a : M) → R) y : R)

Tactic:
simp [coreflection_apply_coroot, reflection_apply, map_sub, mul_comm]

Premises used: map_sub, mul_comm, RootPairing.reflection_apply, RootPairing.coreflection_apply_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j : ι
y : M
⊢ Eq.{u_2 + 1} (α := R) ((P.coroot' j : (a : M) → R) ((P.reflection i : (a : M) → M) y : M) : R)
    ((P.coroot' ((P.reflectionPerm i : (a : ι) → ι) j) : (a : M) → R) y : R)

Tactic:
(LinearMap.congr_fun P.coroot'_reflectionPerm y).symm

Premises used: LinearMap.congr_fun, Eq.symm, RootPairing.coroot'_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j k : ι
simp :
  Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N) :
      R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M)) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) k : N) :
      R)
⊢ P.pairing j ((P.reflectionPerm i : (a : ι) → ι) k) = P.pairing ((P.reflectionPerm i : (a : ι) → ι) j) k

Tactic:
simp only [pairing, root', coroot_reflectionPerm, root_reflectionPerm]

Premises used: RootPairing.pairing, RootPairing.root', RootPairing.coroot_reflectionPerm, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 j k : ι
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
        ((P.coreflection i : (a : N) → N) ((P.coroot : (a : ι) → N) k : N) : N) :
      R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M)) :
            N →ₗ[R] R) :
          (a : N) → R)
        ((P.coroot : (a : ι) → N) k : N) :
      R)

Tactic:
simp [coreflection_apply_coroot, reflection_apply_root, mul_comm]

Premises used: mul_comm, RootPairing.coreflection_apply_coroot, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
h :
  ∀ (f : Dual R N) (n : N),
    Eq.{u_2 + 1} (α := R)
      ((((((P.toPerfPair.conj : (a : End R M) → End R (Dual R N)) (↑(P.reflection i) : M →ₗ[R] M) : End R (Dual R N)) :
                  (a : Dual R N) → Dual R N)
                f :
              Dual R N) :
            (a : N) → R)
          n :
        R)
      (((((↑(P.coreflection i) : N →ₗ[R] N).dualMap : (a : Dual R N) → Dual R N) f : Dual R N) : (a : N) → R) n : R)
⊢ (P.toPerfPair.conj : (a : End R M) → End R (Dual R N)) (↑(P.reflection i) : M →ₗ[R] M) =
    (↑(P.coreflection i) : N →ₗ[R] N).dualMap

Tactic:
ext f n