awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R_1 : Type u
M_1 : Type v
ι : Type w
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
R : Type u
M : Type v
inst_3 : Ring R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
inst_8 : Module.Finite R M
inst_9 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : #{ i : ι // p i ≠ ⊥ } < ℵ₀
⊢ Fintype { i : ι // p i ≠ ⊥ }
have this₁ : Nonempty.{w + 1} (Fintype { i : ι // p i ≠ ⊥ })
Tactic: rw [Cardinal.lt_aleph0_iff_fintype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R_1 : Type u
M_1 : Type v
ι : Type w
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
R : Type u
M : Type v
inst_3 : Ring R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
inst_8 : Module.Finite R M
inst_9 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ Fintype { i : ι // p i ≠ ⊥ }
have suffices : #{ i : ι // p i ≠ ⊥ } < ℵ₀
Tactic: suffices #{ i // p i ≠ ⊥ } < (ℵ₀ : Cardinal.{w}) by
    rw [Cardinal.lt_aleph0_iff_fintype] at this
    exact this.some
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R_1 : Type u
M_1 : Type v
ι : Type w
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
R : Type u
M : Type v
inst_3 : Ring R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
inst_8 : Module.Finite R M
inst_9 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ #{ i : ι // p i ≠ ⊥ } < ℵ₀
have refine : (↑(finrank R M) : Cardinal.{w}) < ℵ₀
Tactic: refine lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M < #t
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have obtain : ∀ (g : ↥t → R) (sum : Eq.{u_2 + 1} (α := M) (∑ i : ↥t, g i • (↑i : M)) 0) (z : ↥t) (nonzero : g z ≠ 0),
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ ∃ x ∈ t, f x ≠ 0
Tactic: obtain ⟨g, sum, z, nonzero⟩ := Fintype.not_linearIndependent_iff.mp
    (mt LinearIndependent.finset_card_le_finrank h.not_ge)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : Eq.{u_2 + 1} (α := M) (∑ i : ↥t, g i • (↑i : M)) 0
z : ↥t
nonzero : g z ≠ 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have refine : Eq (α := M) (∑ e ∈ t, extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 e • e) 0
Tactic: refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : Eq.{u_2 + 1} (α := M) (∑ i : ↥t, g i • (↑i : M)) 0
z : ↥t
nonzero : g z ≠ 0
⊢ Eq (α := M) (∑ e ∈ t, extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 e • e) 0
have rw : Eq.{u_2 + 1} (α := M)
  (∑ i : (↑(↑t : Set M) : Type u_2), extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 (↑i : M) • (↑i : M)) 0
Tactic: rw [← Finset.sum_finset_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M < #t
g : ↥t → R
sum : Eq.{u_2 + 1} (α := M) (∑ i : ↥t, g i • (↑i : M)) 0
z : ↥t
nonzero : g z ≠ 0
⊢ Eq.{u_2 + 1} (α := M)
    (∑ i : (↑(↑t : Set M) : Type u_2), extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 (↑i : M) • (↑i : M)) 0
have h₁ : ∀ (x : (↑(↑t : Set M) : Type u_2)),
  Membership.mem (γ := Finset (↑(↑t : Set M) : Type u_2)) Finset.univ x →
    extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 (↑x : M) = g x
Tactic: convert! sum
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have obtain : ∀ (x₀ : M) (x₀_mem : x₀ ∈ t),
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
Tactic: obtain ⟨x₀, x₀_mem⟩ := card_pos.1 ((Nat.succ_pos _).trans h)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
⊢ finrank R M < #t'
have rw : finrank R M < #t - 1
Tactic: rw [card_map, card_erase_of_mem x₀_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have h' : finrank R M < #t'
Tactic: have h' : finrank R M < t'.card := by
    rw [card_map, card_erase_of_mem x₀_mem]
    exact Nat.lt_pred_iff.mpr h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have obtain : ∀ (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t') (nz : g x₁ ≠ 0),
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
Tactic: obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_finrank_lt_card h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have refine_1 : Eq (α := M) (∑ e ∈ t, f e • e) 0
Tactic: refine ⟨f, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
refine_1 : Eq (α := M) (∑ e ∈ t, f e • e) 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have refine_2 : Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0
Tactic: refine ⟨f, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
refine_1 : Eq (α := M) (∑ e ∈ t, f e • e) 0
refine_2 : Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have refine_3 : ∃ x ∈ t, f x ≠ 0
Tactic: refine ⟨f, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ Eq (α := M) (∑ e ∈ t, f e • e) 0
have refine_1 : ∀ (gsum : Eq (α := M) (∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀)) 0) (x₁ : M) (x₁_mem : x₁ ∈ t') (nz : g x₁ ≠ 0),
  let f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀);
  Eq (α := M) (∑ e ∈ t, f e • e) 0
Tactic: rw [sum_map, Embedding.coeFn_mk] at gsum
Cleared hypotheses: gsum, x₁, x₁_mem, nz, f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀)) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ Eq (α := M) (∑ e ∈ t, f e • e) 0
have refine_1 : Eq (α := M) (∑ x ∈ t.erase x₀, ((if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x - g (x - x₀) • x₀))
  (∑ x ∈ t.erase x₀, (g (x - x₀) • x - g (x - x₀) • x₀))
Tactic: simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀)) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ Eq (α := M) (∑ x ∈ t.erase x₀, ((if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x - g (x - x₀) • x₀))
    (∑ x ∈ t.erase x₀, (g (x - x₀) • x - g (x - x₀) • x₀))
have refine_1 : ∀ (x : M) (x_mem : x ∈ t.erase x₀),
  (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x - g (x - x₀) • x₀ =
    g (x - x₀) • x - g (x - x₀) • x₀
Tactic: refine sum_congr rfl fun x x_mem ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ x ∈ t.erase x₀, g (x - x₀) • (x - x₀)) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x : M
x_mem : x ∈ t.erase x₀
⊢ (if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀)) • x - g (x - x₀) • x₀ =
    g (x - x₀) • x - g (x - x₀) • x₀
have refine_1 : g (x - x₀) • x - g (x - x₀) • x₀ = g (x - x₀) • x - g (x - x₀) • x₀
Tactic: rw [if_neg (mem_erase.mp x_mem).1]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0
have refine_2 : Eq.{u_1 + 1} (α := R) (∑ x ∈ t.erase x₀, if x = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (x - x₀))
  (∑ z ∈ t.erase x₀, g (z - x₀))
Tactic: simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
x₁ : M
x₁_mem : x₁ ∈ t'
nz : g x₁ ≠ 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
⊢ ∃ x ∈ t, f x ≠ 0
have refine_3 : ∀ (x₁ : M) (x₁_mem' : x₁ ∈ t.erase x₀) (x₁_mem : Membership.mem (α := M) t' ((shift : (a : M) → M) x₁ : M))
  (nz : g ((shift : (a : M) → M) x₁) ≠ 0), ∃ x ∈ t, f x ≠ 0
Tactic: obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
Cleared hypotheses: x₁, x₁_mem, nz
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x₁ : M
x₁_mem' : x₁ ∈ t.erase x₀
x₁_mem : Membership.mem (α := M) t' ((shift : (a : M) → M) x₁ : M)
nz : g ((shift : (a : M) → M) x₁) ≠ 0
⊢ ∃ x ∈ t, f x ≠ 0
have this : x₁ ≠ x₀ ∧ x₁ ∈ t
Tactic: have := mem_erase.mp x₁_mem'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
let let₁ let₂ :
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have let₃ : let t' := Finset.map shift (t.erase x₀);
∀ (h' : finrank R M < #t'),
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
Tactic: classical
  let t' := (t.erase x₀).map shift
  have h' : finrank R M < t'.card := by
    rw [card_map, card_erase_of_mem x₀_mem]
    exact Nat.lt_pred_iff.mpr h
  -- to obtain a function `g`.
  obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_finrank_lt_card h'
  -- Then obtain `f` by translating back by `x₀`,
  -- and setting the value of `f` at `x₀` to ensure `∑ e ∈ t, f e = 0`.
  let f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
  refine ⟨f, ?_, ?_, ?_⟩
  -- After this, it's a matter of verifying the properties,
  -- based on the corresponding properties for `g`.
  · rw [sum_map, Embedding.coeFn_mk] at gsum
    simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]
    refine sum_congr rfl fun x x_mem ↦ ?_
    rw [if_neg (mem_erase.mp x_mem).1]
  · simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
    exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1
  · obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
    have := mem_erase.mp x₁_mem'
    exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
let let₁ let₂ :
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
let₃ :
  let t' := Finset.map shift (t.erase x₀);
  ∀ (h' : finrank R M < #t'),
    ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have let₄ : let t' := Finset.map shift (t.erase x₀);
∀ (h' : finrank R M < #t') (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t')
  (nz : g x₁ ≠ 0),
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
Tactic: classical
  let t' := (t.erase x₀).map shift
  have h' : finrank R M < t'.card := by
    rw [card_map, card_erase_of_mem x₀_mem]
    exact Nat.lt_pred_iff.mpr h
  -- to obtain a function `g`.
  obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_finrank_lt_card h'
  -- Then obtain `f` by translating back by `x₀`,
  -- and setting the value of `f` at `x₀` to ensure `∑ e ∈ t, f e = 0`.
  let f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
  refine ⟨f, ?_, ?_, ?_⟩
  -- After this, it's a matter of verifying the properties,
  -- based on the corresponding properties for `g`.
  · rw [sum_map, Embedding.coeFn_mk] at gsum
    simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]
    refine sum_congr rfl fun x x_mem ↦ ?_
    rw [if_neg (mem_erase.mp x_mem).1]
  · simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
    exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1
  · obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
    have := mem_erase.mp x₁_mem'
    exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
let let₁ let₂ :
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
let₃ :
  let t' := Finset.map shift (t.erase x₀);
  ∀ (h' : finrank R M < #t'),
    ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
let₄ let₅ :
  let t' := Finset.map shift (t.erase x₀);
  ∀ (h' : finrank R M < #t') (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t')
    (nz : g x₁ ≠ 0),
    ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have refine_1 : let t' := Finset.map shift (t.erase x₀);
∀ (h' : finrank R M < #t') (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t')
  (nz : g x₁ ≠ 0),
  let f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀);
  Eq (α := M) (∑ e ∈ t, f e • e) 0
Tactic: classical
  let t' := (t.erase x₀).map shift
  have h' : finrank R M < t'.card := by
    rw [card_map, card_erase_of_mem x₀_mem]
    exact Nat.lt_pred_iff.mpr h
  -- to obtain a function `g`.
  obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_finrank_lt_card h'
  -- Then obtain `f` by translating back by `x₀`,
  -- and setting the value of `f` at `x₀` to ensure `∑ e ∈ t, f e = 0`.
  let f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
  refine ⟨f, ?_, ?_, ?_⟩
  -- After this, it's a matter of verifying the properties,
  -- based on the corresponding properties for `g`.
  · rw [sum_map, Embedding.coeFn_mk] at gsum
    simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]
    refine sum_congr rfl fun x x_mem ↦ ?_
    rw [if_neg (mem_erase.mp x_mem).1]
  · simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
    exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1
  · obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
    have := mem_erase.mp x₁_mem'
    exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩