awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
⊢ ∃ (f : ↥b.support → ℤ),
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
      (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have this : Membership.mem.{u_4, u_4} (α := N) (γ := Submodule ℤ N) (span ℤ ((⇑P.coroot : (a : ι) → N) '' (↑b.support : Set ι)))
  ((P.coroot : (a : ι) → N) j : N)
Tactic: have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
this :
  Membership.mem.{u_4, u_4} (α := N) (γ := Submodule ℤ N) (span ℤ ((⇑P.coroot : (a : ι) → N) '' (↑b.support : Set ι)))
    ((P.coroot : (a : ι) → N) j : N)
⊢ ∃ (f : ↥b.support → ℤ),
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
      (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have this₁ : ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℤ),
  Eq.{u_4 + 1} (α := N)
    (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
    ((P.coroot : (a : ι) → N) j : N)
Tactic: rw [image_eq_range, mem_span_range_iff_exists_fun] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
this :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℤ),
    Eq.{u_4 + 1} (α := N)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
      ((P.coroot : (a : ι) → N) j : N)
⊢ ∃ (f : ↥b.support → ℤ),
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
      (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have refine : ∀ (f : ↥b.support → ℤ)
  (hf :
    Eq.{u_4 + 1} (α := N)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (f i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
      ((P.coroot : (a : ι) → N) j : N)),
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
Tactic: refine this.imp fun f hf ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
this :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℤ),
    Eq.{u_4 + 1} (α := N)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
      ((P.coroot : (a : ι) → N) j : N)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) (∑ i : ↥b.support, HSMul.hSMul (β := N) (f i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
    ((P.coroot : (a : ι) → N) j : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have simp_rw : Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
  (∑ x : ↥b.support,
      t • HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N) :
    N)
Tactic: simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
this :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℤ),
    Eq.{u_4 + 1} (α := N)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
      ((P.coroot : (a : ι) → N) j : N)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) (∑ i : ↥b.support, HSMul.hSMul (β := N) (f i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
    ((P.coroot : (a : ι) → N) j : N)
simp_rw :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ x : ↥b.support,
        t • HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N) :
      N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have simp_rw₁ : (P.coroot : (a : ι) → N) i =
  HSMul.hSMul (β := N) t
    (∑ x : ↥b.support,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N))
Tactic: simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
this :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℤ),
    Eq.{u_4 + 1} (α := N)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
      ((P.coroot : (a : ι) → N) j : N)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) (∑ i : ↥b.support, HSMul.hSMul (β := N) (f i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
    ((P.coroot : (a : ι) → N) j : N)
simp_rw :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ x : ↥b.support,
        t • HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N) :
      N)
simp_rw₁ :
  (P.coroot : (a : ι) → N) i =
    HSMul.hSMul (β := N) t
      (∑ x : ↥b.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N))
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have simp_rw₂ : (P.coroot : (a : ι) → N) i =
  HSMul.hSMul (β := N) t (∑ x : ↥b.support, HSMul.hSMul (β := N) (f x) ((P.coroot : (a : ι) → N) (↑x : ι) : N))
Tactic: simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
this :
  ∃ (c : (↑(↑b.support : Set ι) : Type u_1) → ℤ),
    Eq.{u_4 + 1} (α := N)
      (∑ i : (↑(↑b.support : Set ι) : Type u_1), HSMul.hSMul (β := N) (c i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
      ((P.coroot : (a : ι) → N) j : N)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) (∑ i : ↥b.support, HSMul.hSMul (β := N) (f i) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
    ((P.coroot : (a : ι) → N) j : N)
simp_rw :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ x : ↥b.support,
        t • HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N) :
      N)
simp_rw₁ :
  (P.coroot : (a : ι) → N) i =
    HSMul.hSMul (β := N) t
      (∑ x : ↥b.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N))
simp_rw₂ :
  (P.coroot : (a : ι) → N) i =
    HSMul.hSMul (β := N) t (∑ x : ↥b.support, HSMul.hSMul (β := N) (f x) ((P.coroot : (a : ι) → N) (↑x : ι) : N))
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
have simp_rw₃ : (P.coroot : (a : ι) → N) i = HSMul.hSMul (β := N) t ((P.coroot : (a : ι) → N) j : N)
Tactic: simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
⊢ ∃ (z : ℤ), (↑z : R) * t = 1
have obtain : ∀ (f : ↥b.support → ℤ)
  (hf :
    Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
      (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)),
  ∃ (z : ℤ), (↑z : R) * t = 1
Tactic: obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i := by
    have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
    rw [image_eq_range, mem_span_range_iff_exists_fun] at this
    refine this.imp fun f hf ↦ ?_
    simp only [Finset.coe_sort_coe] at hf
    simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
⊢ ∃ (z : ℤ), (↑z : R) * t = 1
have h₁ : (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
Tactic: use f ⟨i, h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
have rw : ∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) =
  HSMul.hSMul (β := N) t
    (∑ i : ↥b.support,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f i) : R) ((P.coroot : (a : ι) → N) (↑i : ι) : N))
Tactic: rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
⊢ ∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) =
    HSMul.hSMul (β := N) t
      (∑ i : ↥b.support,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f i) : R) ((P.coroot : (a : ι) → N) (↑i : ι) : N))
have simp_rw : ∑ x : ↥b.support,
    t • HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f x) : R) ((P.coroot : (a : ι) → N) (↑x : ι) : N) =
  HSMul.hSMul (β := N) t
    (∑ i : ↥b.support,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) (↑(f i) : R) ((P.coroot : (a : ι) → N) (↑i : ι) : N))
Tactic: simp_rw [mul_smul, ← Finset.smul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    (∑ i : ↥b.support, HSMul.hSMul (β := N) (t * (↑(f i) : R)) ((P.coroot : (a : ι) → N) (↑i : ι) : N) : N)
⊢ (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
have hf₁ : Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
  ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
      (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
        ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
          fun (x : ↥b.support) ↦ (↑(f x) : R))) :
    N)
Tactic: replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k)
      (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by
    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]
    simp_rw [mul_smul, ← Finset.smul_sum]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
⊢ (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
have hg : Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
  ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
Tactic: have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
hf :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
hg :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
⊢ (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
have hf₁ : Eq.{u_4 + 1} (α := N)
  ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
  ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
      (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
        ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
          fun (x : ↥b.support) ↦ (↑(f x) : R))) :
    N)
Tactic: rw [hg] at hf
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)
f : ↥b.support → ℤ
g : Finsupp.{u_1, u_2} (↥b.support) R := single (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h) 1
hf :
  Eq.{u_4 + 1} (α := N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N)
        (HSMul.hSMul (β := Finsupp.{u_1, u_2} (↥b.support) R) t
          ((LinearEquiv.symm (linearEquivFunOnFinite R R ↥b.support) : (a : ↥b.support → R) → ↥b.support →₀ R)
            fun (x : ↥b.support) ↦ (↑(f x) : R))) :
      N)
hg :
  Eq.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N)
    ((linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι) : (a : ↥b.support →₀ R) → N) g : N)
⊢ (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
have this : Injective (α := Finsupp.{u_1, u_2} (↥b.support) R) (β := N)
  (⇑(linearCombination R fun (k : ↥b.support) ↦ (P.coroot : (a : ι) → N) (↑k : ι)) : (a : ↥b.support →₀ R) → N)
Tactic: have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linearIndepOn_coroot
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Base (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 : RootPairing ι R M N
b : P.Base
inst_5 : Finite ι
inst_6 : IsAddTorsionFree M
inst_7 : IsAddTorsionFree N
i : ι
h : i ∈ b.support
t : R
ht :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M))
⊢ ∃ (z : ℤ), (↑z : R) * t = 1
have obtain : ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
  ∃ (z : ℤ), (↑z : R) * t = 1
Tactic: classical
  obtain ⟨j, hj⟩ := ht
  obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i := by
    have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
    rw [image_eq_range, mem_span_range_iff_exists_fun] at this
    refine this.imp fun f hf ↦ ?_
    simp only [Finset.coe_sort_coe] at hf
    simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]
  use f ⟨i, h⟩
  replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k)
      (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by
    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
      Fintype.linearCombination_apply, hf]
    simp_rw [mul_smul, ← Finset.smul_sum]
  let g : b.support →₀ R := single ⟨i, h⟩ 1
  have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
  rw [hg] at hf
  have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linearIndepOn_coroot
  simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm
Cleared hypotheses: ht