mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : 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 : ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
f : ι →₀ R
hf : f ∈ Finsupp.supported R R s
g : ι →₀ R
hg : g ∈ Finsupp.supported R R s
eq : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0) ↔
    ∀ x ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) x = 0 → x = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ (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), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0

Tactic:
]

Goal state after:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
⊢ (∀ (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), ↑t ⊆ s → ∑ i ∈ t, g i • v i = 0 → ∀ i ∈ t, g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
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}
⊢ 1 + 1 + 1 = 3

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}
⊢ 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}
⊢ x ∉ {y, z}

Tactic:
]

Goal state after:
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}
⊢ 1 + 1 + 1 = 3

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}
⊢ y ∉ {z}

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}
⊢ x ∉ {y, z}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
h : s.encard = 4
⊢ 4 ≠ 0

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
h : s.encard = 4
⊢ 4 ≠ 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
⊢ ∑ x ∈ t, g x • v x = 0

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
⊢ ∀ x ∈ t, x ∉ range Subtype.val → g x • v x = 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
⊢ ∑ x ∈ t, g x • v x = 0

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
⊢ ∀ x ∈ t, x ∉ range Subtype.val → g x • v x = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y z, x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
hx : x ∈ s
⊢ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y z, x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
hx : x ∈ s
⊢ ∃ 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_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 = s

Tactic:
]

Goal state after:
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
⊢ ∀ x ∉ univ \ {i}, (Finsupp.single i (l i) - l) x = 0

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
⊢ ∀ x ∉ univ \ {i}, (Finsupp.single i (l i) - l) x = 0
Module: Mathlib.Data.Set.Card

Goal state before:
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}
⊢ 1 + 1 + 1 + 1 = 4

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}
⊢ 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}
⊢ 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}
⊢ x ∉ {y, z, w}

Tactic:
]

Goal state after:
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}
⊢ 1 + 1 + 1 + 1 = 4

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}
⊢ z ∉ {w}

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}
⊢ y ∉ {z, w}

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}
⊢ x ∉ {y, z, w}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_2
k : ℕ
⊢ (Iio k).encard = (Iio k).encard

Tactic:
]

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

Goal state before:
pp: case e'_3
k : ℕ
⊢ ↑k = ↑k

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : ∃ x, t \ s = {x}
⊢ ∃ a, t = insert a s

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : ∃ x, t \ s = {x}
⊢ ∃ a, t = insert a s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ insert x s = insert x s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : n + 1 ≤ n
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : n + 1 ≤ n
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
IH : ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = ↑n
hk : ↑n + 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ ↑n + 1 = ↑n + 1

Tactic:
]

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

Goal state before:
pp: case top
α : Type u_1
s : Set α
a✝ : ∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : s.encard = ⊤
⊢ ∃ t ⊆ s, t.encard = ⊤

Tactic:
]

Goal state after:
case top
α : Type u_1
s : Set α
a✝ : ∀ (n : ℕ), ↑n ≤ s.encard → ∃ t ⊆ s, t.encard = ↑n
hk : s.encard = ⊤
⊢ ∃ t ⊆ s, t.encard = ⊤
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ ∀ x ∈ N, x = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0
⊢ ∀ x ∈ N, x = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : 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 : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : k + s.encard ≤ (t \ s).encard + s.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∀ (g : Fin 1 → R), ∑ i, g i • (Subtype.val ∘ fun x_1 ↦ ⟨x, hx⟩) i = 0 → ∀ (i : Fin 1), g i = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
N : Submodule R M
x : M
hx : x ∈ N
x_ne : x ≠ 0
⊢ ∀ (g : Fin 1 → R), ∑ i, g i • (Subtype.val ∘ fun x_1 ↦ ⟨x, hx⟩) i = 0 → ∀ (i : Fin 1), g i = 0
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ s.encard + r'.encard = s.encard + r'.encard

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ ENat.card ↑s = ENat.card ↑s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ ENat.card α ≤ ENat.card α

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ s.encard ≤ s.encard

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ InjOn f s

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ InjOn f s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ Function.invFunOn f s '' f '' s = s

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ Function.invFunOn f s '' f '' s = s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ t.encard = t.encard

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ t.encard ≤ t.encard

Tactic:
]

Goal state after:
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}))

Tactic:
intro h i h_in_span
    apply one_ne_zero (h i 1 (by simp [h_in_span]))

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ s.encard ≤ t.encard

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ s.encard ≤ t.encard
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: case insert
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H

Tactic:
]

Goal state after:
case insert
η : Type u_1
f : η → Type u_2
inst✝³ : (i : η) → MulOneClass (f i)
S : Type u_3
inst✝² : SetLike S ((i : η) → f i)
inst✝¹ : SubmonoidClass S ((i : η) → f i)
inst✝ : DecidableEq η
H : S
i : η
I : Finset η
hnotMem : i ∉ I
ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ i_1 ∉ insert i I, x i_1 = 1
h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x = 0
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x = 0
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ False
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this✝ : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ 0
this : N = ⊥
⊢ P ⊥

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
this✝ : DecidableEq M
Pbot : P ⊥
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ 0
this : N = ⊥
⊢ P ⊥
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : ↑s), v ↑i ∉ span K (v ∘ Subtype.val '' (univ \ {i}))) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
]

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
s : Set ι
⊢ (∀ (i : ↑s), v ↑i ∉ span K (v ∘ Subtype.val '' (univ \ {i}))) ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
this : α ≃ Fin ⋯.choose
⊢ α ≃ Fin ⋯.choose

Tactic:
]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
this : α ≃ Fin ⋯.choose
⊢ α ≃ Fin ⋯.choose
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nonempty α ↔ Nonempty α

Tactic:
]

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ insert a (s \ {a}) ⊆ Function.update f₀ a b ⁻¹' t ∧
    InjOn (Function.update f₀ a b) (s \ {a}) ∧ Function.update f₀ a b a ∉ Function.update f₀ a b '' (s \ {a})

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ insert a (s \ {a}) ⊆ Function.update f₀ a b ⁻¹' t ∧
    InjOn (Function.update f₀ a b) (s \ {a}) ∧ Function.update f₀ a b a ∉ Function.update f₀ a b '' (s \ {a})
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ f₀ x = f₀ x

pp: case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ x ≠ a

Tactic:
]

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : x ∉ {a}
⊢ x ≠ a
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ t = t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
this : Function.Injective (MapsTo.restrict f s t hf)
⊢ s.encard ≤ t.encard

Tactic:
let f' : s ↪ t := ⟨hf.restrict, this⟩

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
this : Function.Injective (MapsTo.restrict f s t hf)
f' : ↑s ↪ ↑t := { toFun := MapsTo.restrict f s t hf, inj' := this }
⊢ s.encard ≤ t.encard
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝¹ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Finite β
hlt : Nat.card β < n
⊢ P β

Tactic:
]

Goal state after:
case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝¹ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Finite β
hlt : Nat.card β < n
⊢ P β
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case h.inr
P : Type u_4 → Prop
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [Finite α], Nat.card α = m → P α
α : Type u_4
inst✝ : Finite α
hn : Nat.card α = n
hnontriv : Nontrivial α
⊢ P α

Tactic:
apply hstep
    intro β _ hlt
    rw [hn] at hlt
    exact ih (Nat.card β) hlt _ rfl

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ s.Finite

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.Finite
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : Finite α
⊢ ↑(Nat.card α) = Cardinal.mk α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ Fintype.card ↑s = Fintype.card ↑s

Tactic:
]

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

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

Tactic:
]

Goal state after: