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 : ι
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)

Tactic:
simp [reflection_apply, coreflection_apply, mul_comm (f <| P.coroot i)]

Premises used: 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 : ι
⊢ (P.flip.toPerfPair.conj : (a : End R N) → End R (Dual R M)) (↑(P.coreflection i) : N →ₗ[R] N) =
    (↑(P.reflection i) : M →ₗ[R] M).dualMap

Tactic:
P.flip.toPerfPair_conj_reflection i

Premises used: RootPairing.flip, LinearMap.mk₂'ₛₗ, LinearMap.flip, RootPairing.toPerfPair_conj_reflection
-- 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 : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₃ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₄ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₅ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₆ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) (-(P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₇ :
  -(((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₈ rw₉ : -P.pairing i j = -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j

Tactic:
rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]

Premises used: RootPairing.pairing, RootPairing.root'_coroot_eq_pairing, two_smul, RootPairing.root', sub_add_cancel_left, RootPairing.reflectionPerm_root, RootPairing.pairing_same, LinearMap.map_neg₂
-- 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 : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₂ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₃ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₄ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₅ : (P.root' i : (a : N) → R) (-(P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₆ : -(P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₇ rw₈ : -P.pairing i j = -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j

Tactic:
rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]

Premises used: RootPairing.pairing, RootPairing.root_coroot_eq_pairing, two_smul, RootPairing.reflectionPerm_coroot, sub_add_cancel_left, map_neg, RootPairing.pairing_same
-- 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_1 j i : ι
a :
  Eq.{u_3 + 1} (α := M)
    ((P.root : (a : ι) → M)
        ((P.reflectionPerm ((P.reflectionPerm i : (a : ι) → ι) i) : (a : ι) → ι)
            ((P.reflectionPerm i : (a : ι) → ι) i : ι) :
          ι) :
      M)
    ((P.root : (a : ι) → M) i : M)
⊢ (P.reflectionPerm ((P.reflectionPerm i : (a : ι) → ι) i) : (a : ι) → ι) ((P.reflectionPerm i : (a : ι) → ι) i : ι) = i

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_1 j i : ι
a :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)))) -
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M) +
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
          (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))))) =
    (P.root : (a : ι) → M) i
⊢ Eq.{u_3 + 1} (α := M)
    ((P.root : (a : ι) → M)
        ((P.reflectionPerm ((P.reflectionPerm i : (a : ι) → ι) i) : (a : ι) → ι)
            ((P.reflectionPerm i : (a : ι) → ι) i : ι) :
          ι) :
      M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
simp only [root_reflectionPerm, reflection_apply, LinearMap.flip_apply, root_coroot_eq_pairing,
      pairing_same, map_sub, coroot_reflectionPerm, coreflection_apply_self, map_neg, neg_smul,
      sub_neg_eq_add, map_smul, smul_add]

Premises used: neg_smul, map_sub, RootPairing.root_coroot_eq_pairing, LinearMap.flip_apply, map_neg, RootPairing.coreflection_apply_self, RootPairing.pairing_same, RootPairing.reflection_apply, RootPairing.coroot_reflectionPerm, smul_add, sub_neg_eq_add, RootPairing.root_reflectionPerm, map_smul
-- 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_1 j i : ι
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) i : M)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)))) -
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M) +
        HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
          (HSMul.hSMul.{u_2, u_3, u_3} (α := R) 2
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))))) =
    (P.root : (a : ι) → M) i

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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
⊢ IsReflexive R M

Tactic:
have := Module.IsReflexive.of_isPerfPair P.toLinearMap
-- 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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
contra : i = -i
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simpa using congr_arg P.root contra

Premises used: congr_arg, RootPairing.root, 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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
contra : i = -i
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
replace contra : P.root i = -P.root i := by simpa using congr_arg P.root contra
-- 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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsDomain R
this : IsReflexive R M
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) i : M)
⊢ False

Tactic:
simp [eq_neg_iff_add_eq_zero, ← two_smul R, NeZero.out, P.ne_zero i] at contra

Premises used: RootPairing.ne_zero, two_smul, NeZero.out, eq_neg_iff_add_eq_zero
-- 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 : i = (P.reflectionPerm j : (a : ι) → ι) j
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)

Tactic:
simp [h]
-- 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 : ι
refine :
  ∀ (h : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
      ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M) ↔
    i = (P.reflectionPerm j : (a : ι) → ι) j

Tactic:
refine ⟨fun h ↦ P.root.injective ?_, fun h ↦ by simp [h]⟩
-- 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) i : M) (-(P.root : (a : ι) → M) j : M)
rw :
  Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    ((P.reflection j : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)
rw₁ : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) (-(P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M)
    ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M)

Tactic:
rw [root_reflectionPerm, reflection_apply_self, h]

Premises used: RootPairing.reflection_apply_self, 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 : ι
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N) (-(P.coroot : (a : ι) → N) j : N) ↔
    i = (P.reflectionPerm j : (a : ι) → ι) j

Tactic:
P.flip.root_eq_neg_iff

Premises used: RootPairing.flip, RootPairing.root_eq_neg_iff
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) ↔
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x

Tactic:
⟨this x, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
refine :
  ∀ (h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) ↔
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x

Tactic:
refine ⟨this x, fun h ↦ ?_⟩
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (- -x)

Tactic:
rw [← neg_neg x] at h

Premises used: neg_neg
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (- -x)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x)

Tactic:
this (-x) h

Premises used: Neg.neg
-- 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
x : M
this :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (- -x)
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x)

Tactic:
exact this (-x) h

Premises used: Neg.neg
-- 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
x : M
suffices :
  ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) →
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-x) ↔
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x

Tactic:
suffices ∀ x : M, -x ∈ range P.root → x ∈ range P.root by
    refine ⟨this x, fun h ↦ ?_⟩
    rw [← neg_neg x] at h
    exact this (-x) h
-- 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
x y : M
this :
  ∀ (i : ι) (hi : (P.root : (a : ι) → M) i = -y),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (-y) →
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y

Tactic:
⟨i, hi⟩
-- 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
x y : M
i : ι
hi : (P.root : (a : ι) → M) i = -y
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι) = y

Tactic:
simp [neg_eq_iff_eq_neg.mpr hi]

Premises used: Iff.mpr, neg_eq_iff_eq_neg
-- 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
x y : M
i : ι
hi : (P.root : (a : ι) → M) i = -y
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y

Tactic:
exact ⟨P.reflectionPerm i i, by simp [neg_eq_iff_eq_neg.mpr hi]⟩
-- 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
x : N
⊢ Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (-x) ↔
    Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) x

Tactic:
P.flip.neg_mem_range_root_iff

Premises used: Set.Mem, RootPairing.flip, RootPairing.neg_mem_range_root_iff
-- 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.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι) : M)
    (-(P.root : (a : ι) → M) i : M)

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 : ι
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
    (-(P.coroot : (a : ι) → N) i : N)

Tactic:
P.flip.neg_root_mem i

Premises used: Set.Mem, RootPairing.flip, RootPairing.neg_root_mem
-- 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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
⊢ t * P.pairing i j = 2

Tactic:
simpa using ((P.coroot' j).congr_arg h).symm

Premises used: LinearMap.congr_arg, 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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
⊢ t * P.pairing i j = 2

Tactic:
have hij : t * P.pairing i j = 2 := by simpa using ((P.coroot' j).congr_arg h).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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
⊢ Eq.{u_2 + 1} (α := R) ((P.root' i : (a : N) → R) (HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)) : R)
    (2 : R)

Tactic:
simp [hij]
-- 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
inst_5 : Finite ι
inst_6 : IsAddTorsionFree N
i j : ι
t : R
h : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
hij : t * P.pairing i j = 2
⊢ Eq.{u_2 + 1} (α := R) ((P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R) (2 : R)

Tactic:
simp