mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case refine_1
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝

pp: case refine_2
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ j (i' r • m) = r • j m

Tactic:
·

Goal state after:
case refine_1
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective ⇑j
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
i' : R' → R
hi' : RightInverse i' i
x✝¹ x✝ : R'
h : i' x✝¹ = i' x✝
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ Module.rank R M < ℵ₀

pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀

Tactic:
·

Goal state after:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ Module.rank R M < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀

Tactic:
·

Goal state after:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M ≤ ↑n
⊢ ↑n < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀

pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀

Tactic:
·

Goal state after:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ Module.rank R M < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀

Tactic:
·

Goal state after:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M < ↑n
⊢ ↑n < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Tactic:
·

Goal state after:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Tactic:
·

Goal state after:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.encard = ↑s.toFinset.card

Tactic:
have h := toFinite s
  rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ ¬s = ∅ ↔ s.Nonempty

Tactic:
nonempty_iff_ne_empty

Goal state after:
α : Type u_1
s : Set α
⊢ ¬s = ∅ ↔ s ≠ ∅
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
S' : Type v'
inst✝² : CommSemiring R'
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
r : R'
x✝ : S
this : j ((algebraMap R S) (i r)) = (algebraMap R' S') r
⊢ ↑j (i r • x✝) = r • ↑j x✝

Tactic:
simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ ?b ≤ lift.{v', v} (⨆ ι, #↑↑ι)

pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ ?b

pp: case b
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ Cardinal.{max v' v}

Tactic:
·

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ ?b ≤ lift.{v', v} (⨆ ι, #↑↑ι)
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} #↑↑⟨rangeSplitting ⇑f '' s, ⋯⟩

Tactic:
·

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} #↑↑⟨rangeSplitting ⇑f '' s, ⋯⟩
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
·

Goal state after:
case pos
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')

pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
·

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)

Tactic:
·

Goal state after:
case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M ≃ₗ[R] M'
⊢ lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
·

Goal state after:
case neg
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : LinearOrder R
inst✝³ : CanonicallyOrderedAdd R
inst✝² : AddRightReflectLE R
inst✝¹ : IsCancelAdd M
inst✝ : DecidableEq ι
s : Finset ι
x✝ : ∃ x, ∃ (_ : x ⊆ s), ∃ x_1, ∃ (_ : ∑ i ∈ x, x_1 i • v i = ∑ i ∈ s \ x, x_1 i • v i), ∃ x, ∃ (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ t ⊆ s, ∃ f, ∑ i ∈ t, f i • v i = ∑ i ∈ s \ t, f i • v i ∧ ∃ i ∈ t, f i ≠ 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k

pp: case refine_2
α : Type u_1
s : Set α
k : ℕ∞
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k) → s.encard = k + 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
·

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
s : Finset ι
f g : ι → R
⊢ ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ s.encard = 3

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y

pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}

Tactic:
·

Goal state after:
case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ (∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0) →
    ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0

pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ (∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) →
    ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0

Tactic:
·

Goal state after:
case mp
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ (∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0) →
    ∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}

Tactic:
·

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mpr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ (∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) →
    ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0

Tactic:
·

Goal state after:
case mpr
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
s : Finset ι
⊢ (∀ (f : ι → R), ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0) →
    ∀ (g : ↑↑s → R), ∑ i, g i • v ↑i = 0 → ∀ (i : ↑↑s), g i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ g i = 0

pp: case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
t : Finset ↑s
g : ↑s → R
h0 : ∑ i ∈ t, g i • v ↑i = 0
i : ↑s
hit : i ∈ t
⊢ g i = 0

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
h : ∀ (s_1 : Finset ↑s) (g : ↑s → R), ∑ i ∈ s_1, g i • v ↑i = 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : ↑t ⊆ s
h0 : ∑ i ∈ t, g i • v i = 0
i : ι
hit : i ∈ t
⊢ g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
h : s.encard = 4
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

pp: case refine_2
α : Type u_1
s : Set α
x✝ : ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
x y z w : α
hxy : x ≠ y
hxz : x ≠ z
hxw : x ≠ w
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s = {x, y, z, w}
⊢ s.encard = 4

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
s : Set α
h : s.encard = 4
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ y

pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

pp: case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}

Tactic:
·

Goal state after:
case refine_1.refine_1
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ y
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z

pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

pp: case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}

Tactic:
·

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ z

Tactic:
rintro rfl; exact (hs.symm.subset (Or.inr (Or.inl rfl))).2 rfl

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w

pp: case refine_1.refine_4
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}

Tactic:
·

Goal state after:
case refine_1.refine_3
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ x ≠ w
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ Finsupp.single i (l i) - l ∈ Finsupp.supported R R (univ \ {i})

pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i (l i) - l) = l i • v i

Tactic:
·

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ Finsupp.single i (l i) - l ∈ Finsupp.supported R R (univ \ {i})
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_2
k : ℕ
⊢ {i | i < k}.encard = (↑(Finset.range k)).encard

pp: case e'_3
k : ℕ
⊢ ↑k = ↑(Finset.range k).card

Tactic:
·

Goal state after:
case e'_2
k : ℕ
⊢ {i | i < k}.encard = (↑(Finset.range k)).encard
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i (l i) - l) = l i • v i

Tactic:
·

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i (l i) - l) = l i • v i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

pp: case inr
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard ≠ ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k

Tactic:
·

Goal state after:
case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) → ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

pp: case mpr
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))) → ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0

Tactic:
·

Goal state after:
case mp
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
⊢ (∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0) → ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard

pp: case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (f '' s).encard ≤ s.encard

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard