awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
⊢ i = j
have rw : Eq.{u_2 + 1} (α := M) ((r : (a : ι) → M) i : M) ((r : (a : ι) → M) j : M)
Tactic: rw [← EmbeddingLike.apply_eq_iff_eq r]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
⊢ Eq.{u_1 + 1} (α := R) ((c j : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
have rw : Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
Tactic: rw [← this, h_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
rw : Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
⊢ Eq.{u_1 + 1} (α := R) ((c j : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 2 2
Tactic: rw [← this, h_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
⊢ Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) j : M) : R) (2 : R)
have rw : Eq.{u_1 + 1} (α := R) ((c j : (a : M) → R) ((r : (a : ι) → M) j : M) : R) (2 : R)
Tactic: rw [this, h_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
this :
  ∀ (k : ι),
    Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
      ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
rw : Eq.{u_1 + 1} (α := R) ((c j : (a : M) → R) ((r : (a : ι) → M) j : M) : R) (2 : R)
⊢ Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) j : M) : R) (2 : R)
have rw₁ : Eq.{u_1 + 1} (α := R) 2 2
Tactic: rw [this, h_two]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Reflection (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : IsAddTorsionFree M
r : ι ↪ M
c : ι → Dual R M
hfin : Set.Finite.{u_2} (α := M) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
h_two : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) i : M) : R) (2 : R)
h_mapsTo :
  ∀ (i : ι),
    MapsTo.{u_2, u_2} (α := M) (β := M) (⇑(preReflection ((r : (a : ι) → M) i) (c i) : End R M) : (a : M) → M)
      (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)) (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))
i j : ι
hij :
  Eq (α := Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c i) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
    ((LinearMap.dualMap (Submodule.subtype (span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M)))) :
          (a : Dual R M) → Dual R ↥(span R (range (⇑r : (a : ι) → M))))
        (c j) :
      Dual.{u_1, u_2} R ↥(span R (range.{u_2, u_3 + 1} (ι := ι) (⇑r : (a : ι) → M))))
⊢ i = j
have e_a : ∀ (k : ι),
  Eq.{u_1 + 1} (α := R) ((c i : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
    ((c j : (a : M) → R) ((r : (a : ι) → M) k : M) : R)
Tactic: suffices ∀ k, c i (r k) = c j (r k) by
    rw [← EmbeddingLike.apply_eq_iff_eq r]
    exact eq_of_mapsTo_reflection_of_mem (f := c i) (g := c j) hfin (h_two i) (h_two j)
      (by rw [← this, h_two]) (by rw [this, h_two]) (h_mapsTo i) (h_mapsTo j) (mem_range_self j)
-- 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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
⊢ b.support.Nonempty
have by_contra! : ∀ (contra : b.support = ∅), False
Tactic: by_contra! contra
-- 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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
contra : b.support = ∅
⊢ False
have inhabit : ∀ (inhabited_h : Inhabited ι), False
Tactic: inhabit ι
-- 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 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ False
have this : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i, j} i_1 → Eq.{u_2 + 1} (α := R) (1 i_1) 0
Tactic: have := linearIndepOn_iff'.mp b.linearIndepOn_root ({i, j} : Finset ι) 1
    (by simp [Set.insert_subset_iff, hi, hj]) (by simp [Finset.sum_pair hij, contra])
-- 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 : Nontrivial R
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
intro : ∀ (contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)), False
⊢ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
have intro₁ : ∀ (contra : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
  (this : ∀ (i_1 : ι), Membership.mem (γ := Finset ι) {i, j} i_1 → Eq.{u_2 + 1} (α := R) (1 i_1) 0), False
Tactic: classical
  intro contra
  have := linearIndepOn_iff'.mp b.linearIndepOn_root ({i, j} : Finset ι) 1
    (by simp [Set.insert_subset_iff, hi, hj]) (by simp [Finset.sum_pair hij, contra])
  simp_all
-- 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
i j : ↥b.support
hij : i ≠ j
⊢ 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)
have this : {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)
Tactic: have : ({(j : ι), (i : ι)} : Set ι) ⊆ b.support := by simp [pair_subset_iff]
-- 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
i j : ↥b.support
hij : i ≠ j
this : {(↑j : ι), (↑i : ι)} ⊆ (↑b.support : Set ι)
⊢ 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)
have 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)
Tactic: rw [← linearIndepOn_id_range_iff (by simp_all)]
-- 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
i : ι
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℤ M) (span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    ((P.root : (a : ι) → M) i : M)
have 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)
Tactic: have := b.root_mem_or_neg_mem i
-- 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
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)
have 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)
Tactic: simp only [← span_nat_eq_addSubmonoidClosure, mem_toAddSubmonoid] 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
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)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule ℤ M) (span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι)))
    ((P.root : (a : ι) → M) i : M)
have rw : Membership.mem (α := M) (γ := Submodule ℤ M)
  (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)
Tactic: rw [← span_span_of_tower (R := ℕ)]
-- 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
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)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)
have 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)
Tactic: rcases this with hi | hi
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
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)
⊢ Membership.mem (α := M) (γ := Submodule ℤ M)
    (span ℤ (↑(span ℕ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) ((P.root : (a : ι) → M) i : M)
have 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)
Tactic: rcases this with hi | hi
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
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)
have inr : 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]
-- 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
⊢ 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)))
have refine : range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M) ⊆
  (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)
Tactic: refine le_antisymm (span_mono <| image_subset_range _ _) (span_le.mpr ?_)
-- 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
⊢ Eq (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan R)
have rw : Eq (α := Submodule R M) (span R (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) (P.rootSpan R)
Tactic: rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower]
-- 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
rw :
  Eq (α := Submodule R M) (span R (↑(span ℤ ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) : Set M)) (P.rootSpan R)
⊢ Eq (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan R)
have rw₁ : Eq (α := Submodule R M) (span R (↑(span ℤ (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) : Set M))
  (P.rootSpan R)
Tactic: rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower]
-- 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
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)
⊢ Eq (α := Submodule R M) (span R ((⇑P.root : (a : ι) → M) '' (↑b.support : Set ι))) (P.rootSpan R)
have rw₂ : Eq (α := Submodule R M) (span R (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) (P.rootSpan R)
Tactic: rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower]
-- 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: obtain ⟨j, hj⟩ := ht
Cleared hypotheses: ht