awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Field R
inst_4 : CharZero R
inst_5 : Module R M
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsRootSystem
inst_8 : P.IsCrystallographic
inst_9 : P.IsReduced
_i_1 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
this : InvolutiveNeg ι := P.indexNeg
⊢ Nonempty.{u_1 + 1} P.Base

Tactic:
exact ⟨Base.mk' P (baseOf P.root (f : M →+ ℚ)) (P.linearIndepOn_root_baseOf f hf)
    (fun i ↦ mem_or_neg_mem_closure_baseOf P.root (f : M →+ ℚ) i (hf i) (by simp))⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
⊢ ∃ (k : ι),
    Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
      (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
            (a : M) → M)
          ((root : (a : ι) → M) j : M) :
        M)

Tactic:
h i (mem_range_self j)

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.range
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
⊢ Exists.choose (p := fun (k : ι) ↦
      Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
        (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                End R M) :
              (a : M) → M)
            ((root : (a : ι) → M)
                (⋯.choose (p := fun (k : ι) ↦
                  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
                    (((preReflection ((root : (a : ι) → M) i)
                              ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                            End R M) :
                          (a : M) → M)
                        ((root : (a : ι) → M) j : M) :
                      M))) :
              M) :
          M))
      ⋯ =
    j

Tactic:
root.injective ?_

Premises used: Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
refine :
  Eq.{u_3 + 1} (α := M)
    ((root : (a : ι) → M)
        (Exists.choose (p := fun (k : ι) ↦
          Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
            (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                    End R M) :
                  (a : M) → M)
                ((root : (a : ι) → M)
                    (⋯.choose (p := fun (k : ι) ↦
                      Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
                        (((preReflection ((root : (a : ι) → M) i)
                                  ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                                End R M) :
                              (a : M) → M)
                            ((root : (a : ι) → M) j : M) :
                          M))) :
                  M) :
              M))
          ⋯) :
      M)
    ((root : (a : ι) → M) j : M)
⊢ Exists.choose (p := fun (k : ι) ↦
      Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
        (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                End R M) :
              (a : M) → M)
            ((root : (a : ι) → M)
                (⋯.choose (p := fun (k : ι) ↦
                  Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
                    (((preReflection ((root : (a : ι) → M) i)
                              ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                            End R M) :
                          (a : M) → M)
                        ((root : (a : ι) → M) j : M) :
                      M))) :
              M) :
          M))
      ⋯ =
    j

Tactic:
refine root.injective ?_

Premises used: Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
rw :
  Eq.{u_3 + 1} (α := M)
    (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
          (a : M) → M)
        (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                End R M) :
              (a : M) → M)
            ((root : (a : ι) → M) j : M) :
          M) :
      M)
    ((root : (a : ι) → M) j : M)
⊢ Eq.{u_3 + 1} (α := M)
    ((root : (a : ι) → M)
        (Exists.choose (p := fun (k : ι) ↦
          Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
            (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                    End R M) :
                  (a : M) → M)
                ((root : (a : ι) → M)
                    (⋯.choose (p := fun (k : ι) ↦
                      Eq.{u_3 + 1} (α := M) ((root : (a : ι) → M) k : M)
                        (((preReflection ((root : (a : ι) → M) i)
                                  ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                                End R M) :
                              (a : M) → M)
                            ((root : (a : ι) → M) j : M) :
                          M))) :
                  M) :
              M))
          ⋯) :
      M)
    ((root : (a : ι) → M) j : M)

Tactic:
rw [(exist_eq_reflection_of_mapsTo p root coroot i _ h).choose_spec,
    (exist_eq_reflection_of_mapsTo p root coroot i j h).choose_spec]

Premises used: Exists.choose_spec, _private.0.RootPairing.exist_eq_reflection_of_mapsTo
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 : M →ₗ[R] N →ₗ[R] R
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h :
  ∀ (i : ι),
    MapsTo.{u_3, u_3} (α := M) (β := M)
      (⇑(preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
        (a : M) → M)
      (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M)) (range.{u_3, u_1 + 1} (ι := ι) (⇑root : (a : ι) → M))
hp :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := R)
      ((((p : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R) ((coroot : (a : ι) → N) i : N) :
        R)
      (2 : R)
⊢ Eq.{u_3 + 1} (α := M)
    (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) : End R M) :
          (a : M) → M)
        (((preReflection ((root : (a : ι) → M) i) ((p.flip : (a : N) → M →ₗ[R] R) ((coroot : (a : ι) → N) i)) :
                End R M) :
              (a : M) → M)
            ((root : (a : ι) → M) j : M) :
          M) :
      M)
    ((root : (a : ι) → M) j : M)

Tactic:
apply involutive_preReflection (x := root i) (hp i)

Premises used: Module.involutive_preReflection
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 M
⊢ InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑P.flip : (a : N) → M →ₗ[R] R) (⇑P.coroot : (a : ι) → N)))

Tactic:
have := injOn_dualMap_subtype_span_range_range (finite_range P.root)
    (c := P.toLinearMap.flip ∘ P.coroot) P.root_coroot_two P.mapsTo_reflection_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 M
this :
  InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑P.flip : (a : N) → M →ₗ[R] R) (⇑P.coroot : (a : ι) → N)))
i j : ι
hij :
  Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) ∘ₗ P.flip :
          (a : N) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
        ((P.coroot : (a : ι) → N) i) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) ∘ₗ P.flip :
          (a : N) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
        ((P.coroot : (a : ι) → N) j) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N) ((P.coroot : (a : ι) → N) j : N)

Tactic:
P.flip.toPerfPair.injective <| this (mem_range_self i) (mem_range_self j) hij

Premises used: Set.mem_range_self, RootPairing.flip, RootPairing.toLinearMap, LinearMap.toPerfPair, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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 M
this :
  InjOn (α := Dual R M) (β := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (⇑(LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))) :
      (a : Dual R M) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
    (range (ι := ι) (comp (β := N) (⇑P.flip : (a : N) → M →ₗ[R] R) (⇑P.coroot : (a : ι) → N)))
i j : ι
hij :
  Eq (α := Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) ∘ₗ P.flip :
          (a : N) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
        ((P.coroot : (a : ι) → N) i) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) ∘ₗ P.flip :
          (a : N) → Dual R ↥(span R (range (⇑P.root : (a : ι) → M))))
        ((P.coroot : (a : ι) → N) j) :
      Dual.{u_2, u_3} R ↥(span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N) ((P.coroot : (a : ι) → N) j : N)

Tactic:
exact P.flip.toPerfPair.injective <| this (mem_range_self i) (mem_range_self j) hij

Premises used: Set.mem_range_self, RootPairing.flip, RootPairing.toLinearMap, LinearMap.toPerfPair, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
h : ∀ (i j : ι), Eq (α := ι) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι)
⊢ P₁.reflectionPerm = P₂.reflectionPerm

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
i j : ι
⊢ Eq (α := ι) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι)

Tactic:
P₁.root.injective ?_

Premises used: RootPairing.root, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
i j : ι
h :
  Eq.{u_3 + 1} (α := M) ((P₁.root : (a : ι) → M) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P₁.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
⊢ Eq (α := ι) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι)

Tactic:
refine P₁.root.injective ?_

Premises used: RootPairing.root, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
i j : ι
rw : ((P₂.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
| ((P₁.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)

Tactic:
rw [hr]
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
i j : ι
h :
  Eq.{u_3 + 1} (α := M) ((P₁.root : (a : ι) → M) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P₂.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P₁.root : (a : ι) → M) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P₁.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)

Tactic:
conv_rhs => rw [hr]
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
i j : ι
h :
  HSub.hSub (α := M) ((P₁.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P₁.flip : (a : N) → M →ₗ[R] R) ((P₁.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
            ((P₁.root : (a : ι) → M) j : M) :
          R)
        ((P₁.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P₂.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P₂.flip : (a : N) → M →ₗ[R] R) ((P₂.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
            ((P₂.root : (a : ι) → M) j : M) :
          R)
        ((P₂.root : (a : ι) → M) i : M))
⊢ Eq.{u_3 + 1} (α := M) ((P₁.root : (a : ι) → M) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P₂.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)

Tactic:
simp only [root_reflectionPerm, reflection_apply, coroot']

Premises used: RootPairing.coroot', RootPairing.reflection_apply, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hc' : P₁.coroot = P₂.coroot
i j : ι
⊢ HSub.hSub (α := M) ((P₁.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P₁.flip : (a : N) → M →ₗ[R] R) ((P₁.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
            ((P₁.root : (a : ι) → M) j : M) :
          R)
        ((P₁.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P₂.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P₂.flip : (a : N) → M →ₗ[R] R) ((P₂.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
            ((P₂.root : (a : ι) → M) j : M) :
          R)
        ((P₂.root : (a : ι) → M) i : M))

Tactic:
simp only [hr, he, hc']
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
⊢ ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm

Tactic:
have hp (hc' : P₁.coroot = P₂.coroot) : P₁.reflectionPerm = P₂.reflectionPerm := by
    ext i j
    refine P₁.root.injective ?_
    conv_rhs => rw [hr]
    simp only [root_reflectionPerm, reflection_apply, coroot']
    simp only [hr, he, hc']
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
suffices : P₁.coroot = P₂.coroot
⊢ P₁ = P₂

Tactic:
suffices P₁.coroot = P₂.coroot by
    obtain ⟨p₁⟩ := P₁; obtain ⟨p₂⟩ := P₂
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : IsAddTorsionFree M
h : ∀ (i : ι), Eq.{u_4 + 1} (α := N) ((P₁.coroot : (a : ι) → N) i : N) ((P₂.coroot : (a : ι) → N) i : N)
⊢ P₁.coroot = P₂.coroot

Tactic:
ext i