awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{w, v} (↑(finrank R M) : Cardinal.{v}) = lift.{v, w} (↑(finrank R M) : Cardinal.{w})

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
i : lift.{w, v} (Module.rank R M) = lift.{w, v} (↑(finrank R M) : Cardinal.{v})
i₁ : lift.{w, v} (↑(finrank R M) : Cardinal.{v}) = lift.{v, w} (↑(finrank R M) : Cardinal.{w})
⊢ lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})

Tactic:
calc
    Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{w} (Module.rank R M) :=
      hp.subtype_ne_bot_le_rank
    _ = Cardinal.lift.{w} (finrank R M : Cardinal.{v}) := by rw [finrank_eq_rank]
    _ = Cardinal.lift.{v} (finrank R M : Cardinal.{w}) := by simp

Premises used: iSupIndep.subtype_ne_bot_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 ≠ ⊥ } < ℵ₀
⊢ Nonempty.{w + 1} (Fintype { i : ι // p i ≠ ⊥ })

Tactic:
rw [Cardinal.lt_aleph0_iff_fintype] at this

Premises used: Cardinal.lt_aleph0_iff_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 : Nonempty.{w + 1} (Fintype { i : ι // p i ≠ ⊥ })
⊢ Fintype { i : ι // p i ≠ ⊥ }

Tactic:
exact this.some

Premises used: Nonempty.some
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
suffices : #{ i : ι // p i ≠ ⊥ } < ℵ₀
⊢ Fintype { i : ι // p i ≠ ⊥ }

Tactic:
suffices #{ i // p i ≠ ⊥ } < (ℵ₀ : Cardinal.{w}) by
    rw [Cardinal.lt_aleph0_iff_fintype] at this
    exact this.some
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 ≠ ⊥ } < ℵ₀

Tactic:
lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_

Premises used: lt_of_le_of_lt, iSupIndep.subtype_ne_bot_le_finrank_aux
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
refine : (↑(finrank R M) : Cardinal.{w}) < ℵ₀
⊢ #{ i : ι // p i ≠ ⊥ } < ℵ₀

Tactic:
refine lt_of_le_of_lt hp.subtype_ne_bot_le_finrank_aux ?_

Premises used: lt_of_le_of_lt, iSupIndep.subtype_ne_bot_le_finrank_aux
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
⊢ (↑(finrank R M) : Cardinal.{w}) < ℵ₀

Tactic:
simp [Cardinal.natCast_lt_aleph0]

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
inst_7 : Fintype { i : ι // p i ≠ ⊥ }
⊢ Fintype.card.{w} { i : ι // p i ≠ ⊥ } ≤ finrank R M

Tactic:
simpa using hp.subtype_ne_bot_le_finrank_aux

Premises used: iSupIndep.subtype_ne_bot_le_finrank_aux
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
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
⊢ ∃ (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)

Premises used: mt, Fintype.not_linearIndependent_iff, LinearIndependent.finset_card_le_finrank, Iff.mp, LT.lt.not_ge, Cardinal.sum
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 rwa rwa₁ rwa₂ rwa₃ : g z ≠ 0
⊢ extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 (↑z : M) ≠ 0

Tactic:
rwa [Subtype.val_injective.extend_apply]

Premises used: Subtype.val_injective, Function.Injective.extend_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
refine : Eq (α := M) (∑ e ∈ t, extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 e • e) 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ ∃ x ∈ t, f x ≠ 0

Tactic:
refine ⟨Subtype.val.extend g 0, ?_, z, z.2, by rwa [Subtype.val_injective.extend_apply]⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
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
⊢ Eq (α := M) (∑ e ∈ t, extend (Subtype.val (p := fun (x : M) ↦ x ∈ t)) g 0 e • e) 0

Tactic:
rw [← Finset.sum_finset_coe]

Premises used: Finset.sum_finset_coe
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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, g i • (↑i : M)) 0

Tactic:
sum
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
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
⊢ 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:
convert! sum
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
x : (↑(↑t : Set M) : Type u_2)
h_1 : 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:
apply Subtype.val_injective.extend_apply

Premises used: Subtype.val_injective, Function.Injective.extend_apply
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
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
⊢ ∃ (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)

Premises used: Nat.succ_pos, Iff.mp, LT.lt.trans, Finset.card_pos
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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₀)
rw : finrank R M < #t - 1
⊢ finrank R M < #t'

Tactic:
rw [card_map, card_erase_of_mem x₀_mem]

Premises used: Finset.card_map, Finset.card_erase_of_mem
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 - 1

Tactic:
Nat.lt_pred_iff.mpr h

Premises used: Iff.mpr, Nat.lt_pred_iff, Nat.pred
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 - 1

Tactic:
exact Nat.lt_pred_iff.mpr h

Premises used: Iff.mpr, Nat.lt_pred_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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'

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
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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'
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
⊢ ∃ (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'

Premises used: Module.exists_nontrivial_relation_of_finrank_lt_card
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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

Tactic:
⟨f, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
refine_3 : ∃ 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

Tactic:
refine ⟨f, ?_, ?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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 :
  ∀ (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
⊢ Eq (α := M) (∑ e ∈ t, f e • e) 0

Tactic:
rw [sum_map, Embedding.coeFn_mk] at gsum

Premises used: Finset.sum_map, Function.Embedding.coeFn_mk
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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₀)
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₀))
⊢ Eq (α := M) (∑ e ∈ t, f e • e) 0

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]

Premises used: Finset.sum_smul, neg_smul, sub_eq_add_neg, if_pos, smul_sub, Finset.sum_erase_add, Finset.sum_sub_distrib
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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₀))

Tactic:
sum_congr rfl fun x x_mem ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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₀)
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₀
⊢ 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:
refine sum_congr rfl fun x x_mem ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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₀
refine_1 refine_1₁ : g (x - x₀) • x - g (x - x₀) • x₀ = g (x - x₀) • x - g (x - x₀) • 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:
rw [if_neg (mem_erase.mp x_mem).1]

Premises used: Finset.mem_erase, And.left, Iff.mp, if_neg
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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_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₀))
⊢ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0

Tactic:
simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]

Premises used: add_neg_eq_zero, if_pos, Finset.sum_erase_add
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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) (∑ 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:
sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1

Premises used: Finset.mem_erase, And.left, Iff.mp, if_neg, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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) (∑ 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:
exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1

Premises used: Finset.mem_erase, And.left, Iff.mp, if_neg, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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_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
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem

Premises used: Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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₁ ≠ x₀ ∧ x₁ ∈ t

Tactic:
have := mem_erase.mp x₁_mem'
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
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
this : x₁ ≠ x₀ ∧ x₁ ∈ t
⊢ x₁ ∈ t ∧ f x₁ ≠ 0

Tactic:
simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]

Premises used: And.right, And.left, Function.Embedding.coeFn_mk, sub_add_cancel, if_neg, true_and