awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i j : ↥b.support
hij : i ≠ j
⊢ {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)

Tactic:
have : ({(j : ι), (i : ι)} : Set ι) ⊆ b.support := by simp [pair_subset_iff]
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i j : ↥b.support
hij : i ≠ j
this : {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)
⊢ Injective.{1, u_3 + 1} (α := Fin (Nat.succ 0).succ) (β := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) (↑j : ι)] : Fin (Nat.succ 0).succ → M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i j : ↥b.support
hij : i ≠ j
this : {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)
rw :
  LinearIndepOn.{u_3, u_2, u_3} (ι := M) R (M := M) (id : (a : M) → M)
    (range (ι := Fin (Nat.succ 0).succ) ![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) (↑j : ι)] : Set M)
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) (↑j : ι)] : Fin (Nat.succ 0).succ → M)

Tactic:
rw [← linearIndepOn_id_range_iff (by simp_all)]

Premises used: linearIndepOn_id_range_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i j : ↥b.support
hij : i ≠ j
this : {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)
⊢ LinearIndepOn.{u_3, u_2, u_3} (ι := M) R (M := M) (id : (a : M) → M)
    (range (ι := Fin (Nat.succ 0).succ) ![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) (↑j : ι)] : Set M)

Tactic:
simpa [image_pair] using LinearIndepOn.id_image <| b.linearIndepOn_root.mono this

Premises used: Set.image_pair, RootPairing.Base.linearIndepOn_root, LinearIndepOn.mono, LinearIndepOn.id_image
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : M)

Tactic:
have := b.root_mem_or_neg_mem i
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
this :
  Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := AddSubmonoid M)
      (AddSubmonoid.closure ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (-(P.root : (a : ι) → M) i : M)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      (-(P.root : (a : ι) → M) i : M)

Tactic:
simp only [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid] at this

Premises used: Submodule.mem_toAddSubmonoid, Submodule.span_nat_eq_addSubmonoidClosure
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
this :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      (-(P.root : (a : ι) → M) i : M)
rw :
  Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℤ M) (span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    ((P.root : (a : ι) → M) i : M)

Tactic:
rw [← span_span_of_tower (R := ℕ)]

Premises used: Submodule.span_span_of_tower, Nat
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
this :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      ((P.root : (a : ι) → M) i : M) ∨
    Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
      (-(P.root : (a : ι) → M) i : M)
inl :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        ((P.root : (a : ι) → M) i : M)),
    Membership.mem (α := M) (γ := Submodule ℤ M)
      (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)
inr :
  ∀
    (hi :
      Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
        (-(P.root : (a : ι) → M) i : M)),
    Membership.mem (α := M) (γ := Submodule ℤ M)
      (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)

Tactic:
rcases this with hi | hi
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)

Tactic:
subset_span hi

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    ((P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)

Tactic:
exact subset_span hi

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-(P.root : (a : ι) → M) i : M)
inr :
  Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) (-(P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)

Tactic:
rw [← neg_mem_iff]

Premises used: neg_mem_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-(P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) (-(P.root : (a : ι) → M) i : M)

Tactic:
subset_span hi

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
hi :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℕ M) (span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (-(P.root : (a : ι) → M) i : M)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) (-(P.root : (a : ι) → M) i : M)

Tactic:
exact subset_span hi

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
⊢ Membership.mem.{u_4, u_4} (α := N) (γ := Submodule ℤ N) (span ℤ ((⇑P.coroot : (a : ι) → N) '' (↑b.support : Set ι)))
    ((P.coroot : (a : ι) → N) i : N)

Tactic:
b.flip.root_mem_span_int i

Premises used: RootPairing.Base.root_mem_span_int, Set.Mem, setOf, RootPairing.Base.flip
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ Eq.{u_3 + 1} (α := Submodule ℤ M) (span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (span ℤ (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))

Tactic:
le_antisymm (span_mono <| image_subset_range _ _) (span_le.mpr ?_)

Premises used: Iff.mpr, Set.image_subset_range, le_antisymm, Submodule.span_mono, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
refine :
  range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ⊆
    (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)
⊢ Eq.{u_3 + 1} (α := Submodule ℤ M) (span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    (span ℤ (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))

Tactic:
refine le_antisymm (span_mono <| image_subset_range _ _) (span_le.mpr ?_)

Premises used: Iff.mpr, Set.image_subset_range, le_antisymm, Submodule.span_mono, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
⊢ Membership.mem (α := M) (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
b.root_mem_span_int i

Premises used: RootPairing.Base.root_mem_span_int
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
i : ι
⊢ Membership.mem (α := M) (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
exact b.root_mem_span_int i

Premises used: RootPairing.Base.root_mem_span_int
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ Eq.{u_4 + 1} (α := Submodule ℤ N) (span ℤ ((⇑P.coroot : (a : ι) → N) '' (↑b.support : Set ι)))
    (span ℤ (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))

Tactic:
b.flip.span_int_root_support

Premises used: setOf, RootPairing.Base.span_int_root_support, RootPairing.Base.flip
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
rw :
  Eq (α := Submodule R M) (span R (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) (P.rootSpan R)
rw₁ :
  Eq (α := Submodule R M) (span R (↑(span ℤ (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) : Set M))
    (P.rootSpan R)
rw₂ rw₃ : Eq (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) (P.rootSpan R)
⊢ Eq (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan R)

Tactic:
rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower]

Premises used: Submodule.span_span_of_tower, Int, RootPairing.Base.span_int_root_support
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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
⊢ Eq (α := Submodule R N) (span R ((⇑P.coroot : (a : ι) → N) '' (↑b.support : Set ι))) (P.corootSpan R)

Tactic:
b.flip.span_root_support

Premises used: setOf, RootPairing.Base.flip, RootPairing.Base.span_root_support
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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))
obtain :
  ∀ (j : ι) (hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) t ((P.root : (a : ι) → M) i : M)),
    ∃ (z : ℤ), (↑z : R) * t = 1
⊢ ∃ (z : ℤ), (↑z : R) * t = 1

Tactic:
obtain ⟨j, hj⟩ := ht
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
⊢ ∃ (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

Premises used: Set.image_eq_range, Submodule.mem_span_range_iff_exists_fun
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)

Tactic:
this.imp fun f hf ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
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)
⊢ ∃ (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)

Tactic:
refine this.imp fun f hf ↦ ?_

Premises used: Exists.imp
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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))
simp_rw₃ : (P.coroot : (a : ι) → N) i = HSMul.hSMul (β := N) t ((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:
simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf,
      coroot_eq_smul_coroot_iff.mpr hj]

Premises used: Iff.mpr, RootPairing.coroot_eq_smul_coroot_iff, Finset.smul_sum, Int.cast_smul_eq_zsmul, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
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
⊢ ∃ (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]

Premises used: RootPairing.coroot, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Base
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)
h₁ : (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) i h)) : R) * t = 1
⊢ ∃ (z : ℤ), (↑z : R) * t = 1

Tactic:
use f ⟨i, h⟩

Premises used: Subtype.mk