mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Card

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩
  · obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
    rw [← insert_eq_of_mem hx, ← insert_sdiff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (3 : ℕ∞) = 2 + 1),
      (ENat.addLECancellable_of_ne_top ENat.one_ne_top).inj_left, encard_eq_two] at h
    obtain ⟨y, z, hne, hs⟩ := h
    refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
    · rintro rfl; exact (hs.symm.subset (Or.inl rfl)).2 rfl
    · rintro rfl; exact (hs.symm.subset (Or.inr rfl)).2 rfl
    rw [← hs, insert_sdiff_singleton, insert_eq_of_mem hx]
  rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton] <;> aesop

Goal state after:
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.Data.Set.Card

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
case refine_1.refine_2
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y w : α
hyw : y ≠ w
hyz : y ≠ x
hzw : x ≠ w
hs : s \ {x} = {y, x, w}
⊢ False
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 : α
hyz : y ≠ z
hyw : y ≠ x
hzw : z ≠ x
hs : s \ {x} = {y, z, x}
⊢ False

Tactic:
;

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

Goal state before:
pp: ι : 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 : ι
⊢ l i = 0 i

Tactic:
;

Goal state after:
ι : 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 : ι
⊢ l i = 0 i
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}
⊢ {x, y, z, w}.encard = 4

Tactic:
encard_insert_of_notMem,

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

Tactic:
encard_insert_of_notMem,

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}
⊢ {z, w}.encard + 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}
⊢ 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 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}.encard + 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}
⊢ 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:
encard_insert_of_notMem,

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}
⊢ {w}.encard + 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: α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ ∃ a, t = insert a s

Tactic:
;

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : 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}
⊢ t = insert x s

Tactic:
;

Goal state after:
case h
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t = insert x 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}
⊢ {x} ∪ s = insert x s

Tactic:
singleton_union

Goal state after:
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
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 ≤ t₀.encard
⊢ 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 ≤ t₀.encard
⊢ False
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: 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.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: case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤

Tactic:
;

Goal state after:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard = ⊤
hkt : ⊤ ≤ t.encard
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤
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 h.refine_1
α : 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 : α
hx : x ∈ s
⊢ (if x = a then b else f₀ x) ∈ t

Tactic:
;

Goal state after:
case h.refine_1
α : 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 : α
hx : x ∈ s
⊢ (if x = a then b else f₀ x) ∈ t
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
have := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

Goal state after:
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 : ℕ
rank_ih : (N : Submodule R M) → (∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) → P N
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n + 1
N' : Submodule R M
N'_le : N' ≤ N
x : M
x_mem : x ∈ N
x_ortho : ∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0
m : ℕ
v : Fin m → ↥N'
hli : LinearIndependent R (Subtype.val ∘ v)
⊢ (Subtype.val ∘ Fin.cons ⟨x, x_mem⟩ fun i ↦ ⟨↑(v i), ⋯⟩) = Fin.cons x (Subtype.val ∘ v)

Tactic:
ext i
      refine Fin.cases ?_ ?_ i <;> simp

Goal state after:
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
⊢ ∃ f, BijOn f s t

Tactic:
;

Goal state after:
α : 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
⊢ ∃ f, BijOn f s t
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t

Tactic:
rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h
  · rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
    cases h
    rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]
    exact Cardinal.mk_union_le s t
  · simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this : Fintype ↑t
⊢ Nat.card ↑s < Nat.card ↑t

Tactic:
have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))

Goal state after:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this✝ : Fintype ↑t
this : Fintype ↑s
⊢ Nat.card ↑s < Nat.card ↑t
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s ≠ ∅
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
hs : ∅.ncard ≠ 0
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
hs : ∅.ncard ≠ 0
⊢ False
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ normalizer S

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ normalizer S
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1

Tactic:
;

Goal state after:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ ↑(insert a s).ncard ≤ ↑s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1

Tactic:
;

Goal state after:
case inl
α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).encard ≤ s.encard + 1
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: case inl
α : Type u_1
l : List α
h : l.Nodup
h✝ : Finite α
⊢ ↑(Nat.card α) ≤ ENat.card α

Tactic:
ENat.card_eq_coe_natCard

Goal state after:
case inl
α : Type u_1
l : List α
h : l.Nodup
h✝ : Finite α
⊢ ↑(Nat.card α) ≤ ↑(Nat.card α)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard

Tactic:
;

Goal state after:
α : Type u_1
a : α
s : Set α
h : s.Infinite
⊢ 0 ≤ (insert a s).ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1

Tactic:
;

Goal state after:
α : Type u_1
a : α
s : Set α
h : s.Finite
⊢ s.ncard ≤ if a ∈ s then s.ncard else s.ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1

Tactic:
;

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).ncard < (s \ {a}).ncard + 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ ↑(f '' s).ncard ≤ ↑s.ncard

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ ↑(f '' s).ncard ≤ ↑s.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).encard ≤ s.encard

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
⊢ (f '' s).encard ≤ s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ ↑t.ncard

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : ∀ a ∈ s, f a ∈ t
f_inj : InjOn f s
ht : t.Finite
hle : s.encard ≤ t.encard
⊢ ↑s.ncard ≤ ↑t.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a • ↑s = ↑s
⊢ a ∈ a • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : op a • ↑s = ↑s
⊢ a ∈ op a • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
⊢ a₁ = a₂

Tactic:
have := hs.fintype

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this : Fintype ↑s
⊢ a₁ = a₂
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a : α
ha✝ : a ∈ s.toFinset
ha : a ∈ s
⊢ f'' a ha✝ ∈ t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
a : α
ha✝ : a ∈ s.toFinset
ha : a ∈ s
⊢ f'' a ha✝ ∈ t
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite ↥?m.11 ∧ Finite (G ⧸ ?m.11)

pp: G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Subgroup G

Tactic:
;

Goal state after:
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite ↥?m.11 ∧ Finite (G ⧸ ?m.11)

G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Subgroup G
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = ↑s.ncard + ↑t.ncard

Tactic:
;

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ ↑(s ∪ t).ncard + ↑(s ∩ t).ncard = ↑s.ncard + ↑t.ncard
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = fun i_1 ↦ Pi.mulSingle i x (i.succAbove i_1)

Tactic:
;

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → One (α j)
i : Fin (n + 1)
x : α i
⊢ x = Pi.mulSingle i x i ∧ 1 = fun i_1 ↦ Pi.mulSingle i x (i.succAbove i_1)
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : Group α
a✝ : α
⊢ ↑(Quotient.lift id ⋯ ⟦a✝⟧) = ⟦a✝⟧

Tactic:
;

Goal state after:
case h
α : Type u_1
inst✝ : Group α
a✝ : α
⊢ ↑(Quotient.lift id ⋯ ⟦a✝⟧) = ⟦a✝⟧
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i

Tactic:
;

Goal state after:
α : Type u_1
M : Type u_2
n : ℕ
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v + w) i = vecCons (x + vecHead w) (v + vecTail w) i
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Add α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v + vecCons y w) i = vecCons (vecHead v + y) (vecTail v + w) i
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin n.succ → α
i : Fin n.succ
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Sub α
v : Fin n.succ → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (v - vecCons y w) i = vecCons (vecHead v - y) (vecTail v - w) i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ (t \ s).ncard + s.ncard

Tactic:
;

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ (t \ s).ncard + s.ncard
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard

Tactic:
by
  rw [← ncard_inter_add_ncard_sdiff_eq_ncard s t hs, ← ncard_inter_add_ncard_sdiff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard + s.ncard = Nat.card α

Tactic:
by
  rw [add_comm, ncard_add_ncard_compl s hs hsc]

Goal state after: