awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          HDiv.hDiv (α := R) (β := R) (2 : R)
            ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
Tactic: have hg₀ (i : ι) : g (P.coroot i) ≠ 0 := by
    obtain ⟨q, hq₀, hq⟩ := aux i
    simp [g, coroot_eq_polarizationEquiv_apply_root, ← hq, Rat.cast_smul_eq_qsmul, hq₀.ne', hf₀ i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i_1 : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          HDiv.hDiv (α := R) (β := R) (2 : R)
            ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
i : ι
⊢ LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
have obtain : ∀ (q : ℚ) (hq₀ : 0 < q)
  (hq :
    (↑q : R) =
      HDiv.hDiv (α := R) (β := R) (2 : R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)),
  LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
Tactic: obtain ⟨q, hq₀, hq⟩ := aux i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (hypothesis)
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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          HDiv.hDiv (α := R) (β := R) (2 : R)
            ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have hg : ∀ (i : ι),
  LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
    LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
Tactic: have hg (i : ι) : 0 < g (P.coroot i) ↔ 0 < f (P.root i) := by
    obtain ⟨q, hq₀, hq⟩ := aux i
    simp [g, coroot_eq_polarizationEquiv_apply_root, ← hq, Rat.cast_smul_eq_qsmul, hq₀]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
i : ι
_i_1 : InvolutiveNeg ι := P.indexNeg
_i_2 : Fintype ι := Fintype.ofFinite ι
_i_3 : Module ℚ M := compHom M (algebraMap ℚ R)
_i : Module ℚ N := compHom N (algebraMap ℚ R)
f : Dual ℚ M
hf' : ∀ i ∈ s, Eq (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (1 : ℚ)
hf : s = baseOf (⇑P.root : (a : ι) → M) (↑f : M →+ ℚ)
hf₀ : ∀ (i : ι), Ne (α := ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ) (0 : ℚ)
aux :
  ∀ (i : ι),
    ∃ (q : ℚ),
      0 < q ∧
        (↑q : R) =
          HDiv.hDiv (α := R) (β := R) (2 : R)
            ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) i : M) :
              R)
g : Dual ℚ N := f ∘ₗ (↑(LinearEquiv.restrictScalars ℚ P.PolarizationEquiv.symm) : N →ₗ[ℚ] M)
hg₀ : ∀ (i : ι), Ne (α := ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) (0 : ℚ)
hg :
  ∀ (i : ι),
    LT.lt (α := ℚ) (0 : ℚ) ((g : (a : N) → ℚ) ((P.coroot : (a : ι) → N) i : N) : ℚ) ↔
      LT.lt (α := ℚ) (0 : ℚ) ((f : (a : M) → ℚ) ((P.root : (a : ι) → M) i : M) : ℚ)
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      ((P.coroot : (a : ι) → N) i : N) ∨
    Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N) (AddSubmonoid.closure ((⇑P.coroot : (a : ι) → N) '' s))
      (-(P.coroot : (a : ι) → N) i : N)
have rw : Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N)
    (AddSubmonoid.closure
      (image.{u_1, u_4} (α := ι) (⇑P.coroot : (a : ι) → N) (baseOf (⇑P.coroot : (a : ι) → N) (↑g : N →+ ℚ))))
    ((P.coroot : (a : ι) → N) i : N) ∨
  Membership.mem.{u_4, u_4} (α := N) (γ := AddSubmonoid N)
    (AddSubmonoid.closure
      (image.{u_1, u_4} (α := ι) (⇑P.coroot : (a : ι) → N) (baseOf (⇑P.coroot : (a : ι) → N) (↑g : N →+ ℚ))))
    (-(P.coroot : (a : ι) → N) i : N)
Tactic: rw [hf, P.baseOf_root_eq_baseOf_coroot f hf₀ g hg₀ (fun i ↦ (hg i).symm)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.BaseExists (goal)
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
s : Set ι
hli : LinearIndepOn.{u_1, u_2, u_3} R (M := M) (⇑P.root : (a : ι) → M) s
hsp :
  ∀ (i : ι),
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        ((P.root : (a : ι) → M) i : M) ∨
      Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M) (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' s))
        (-(P.root : (a : ι) → M) i : M)
⊢ LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) (↑(⋯.toFinset (s := s)) : Set ι)
have have : ∀ (this : Fintype ι),
  LinearIndepOn.{u_1, u_2, u_4} R (M := N) (⇑P.coroot : (a : ι) → N) (↑(sorry.toFinset (s := s)) : Set ι)
Tactic: have : Fintype ι := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : 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
have 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)
                  (sorry.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))
        sorry) :
    M)
  ((root : (a : ι) → M) j : M)
Tactic: refine root.injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : 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)
    ((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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
⊢ InjOn (α := N) (β := 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))))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))
have 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)))
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
have h : ∀ (i j : ι), Eq (α := ι) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι)
have 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)
Tactic: refine P₁.root.injective ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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 : ι
| ((P₁.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
have rw : ((P₂.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
Tactic: rw [hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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.{u_3 + 1} (α := M) ((P₁.root : (a : ι) → M) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P₁.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
have 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)
Tactic: conv_rhs => rw [hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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.{u_3 + 1} (α := M) ((P₁.root : (a : ι) → M) ((P₁.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P₂.root : (a : ι) → M) ((P₂.reflectionPerm i : (a : ι) → ι) j : ι) : M)
have 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))
Tactic: simp only [root_reflectionPerm, reflection_apply, coroot']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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))
⊢ P₁ = P₂
have hp : ∀ (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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
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
⊢ P₁ = P₂
have suffices : P₁.coroot = P₂.coroot
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