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

Goal state before:
pp: k : ℕ
⊢ {i | i < k}.encard = ↑k

Tactic:
by

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 : t.encard = s.encard + 1
⊢ ∃ a, t = insert a s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hk : 0 ≤ s.encard
⊢ ∅.encard = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ t₀ ≠ s

Tactic:
by

Goal state after:
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
⊢ l = 0

Tactic:
by

Goal state after:
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₀
⊢ (insert x t₀).encard = ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : Submodule R M
b : Basis ι R ↥P
x : M
⊢ x ∈ P ↔ ∃ c, x = c.sum fun i x ↦ x • ↑(b i)

Tactic:
by

Goal state after:
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
inst✝ : Subsingleton ι
i : ι
hi : ∀ (r : R), r • v i = 0 → r = 0
⊢ LinearIndependent R v

Tactic:
by

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:
exact ⟨s, Subset.rfl, hk⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
P : Submodule R M
b : Basis ι R ↥P
x : M
c : ι → R
⊢ (x = (equivFunOnFinite.symm c).sum fun i x ↦ x • ↑(b i)) ↔ x = ∑ i, c i • ↑(b i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = k

Tactic:
by

Goal state after:
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
inst✝² : IsDomain R
inst✝¹ : IsTorsionFree R M
inst✝ : Subsingleton ι
i : ι
hi : v i ≠ 0
⊢ ∀ (r : R), r • v i = 0 → r = 0

Tactic:
by

Goal state after:
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
i : ι
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
hi : v i ≠ 0
⊢ LinearIndepOn R v {i}

Tactic:
by

Goal state after:
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 : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard

Tactic:
by

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

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

Tactic:
by

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
⊢ (f '' s).encard = s.encard

Tactic:
by

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 α ≤ (range f).encard

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ N = ⊥

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
h : ∀ (i : ι) (a : K), a • v i ∈ span K (v '' (univ \ {i})) → a = 0
i : ι
h_in_span : v i ∈ span K (v '' (univ \ {i}))
⊢ 1 • v i ∈ span K (v '' (univ \ {i}))

Tactic:
by

Goal state after:
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
⊢ (f ⁻¹' t).encard = t.encard

Tactic:
by

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

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

Tactic:
by

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
⊢ s.encard ≤ t.encard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
P Q : Set α
x✝¹ x✝ : ↑(P ↓∩ Q)
h :
  (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝¹ =
    (fun x ↦
        match x with
        | ⟨⟨x, property⟩, hx⟩ => ⟨x, hx⟩)
      x✝
⊢ x✝¹ = x✝

Tactic:
by

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 \ {a}).encard ≤ (t \ {b}).encard

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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
⊢ x = Function.update x i 1 * Pi.mulSingle i (x i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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
⊢ Pi.mulSingle i (x i) ∈ H

Tactic:
by

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
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
⊢ P ⊥

Tactic:
by

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 : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ 0
this : N = ⊥
⊢ P N

Tactic:
by

Goal state after:
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
⊢ LinearIndependent K v ↔ ∀ (i : ι), v i ∉ span K (v '' (univ \ {i}))

Tactic:
by

Goal state after:
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 ι
⊢ LinearIndepOn K v s ↔ ∀ i ∈ s, v i ∉ span K (v '' (s \ {i}))

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst✝ : Finite α
⊢ α ≃ Fin (Nat.card α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
h : Nat.card α = n
⊢ α ≃ Fin n

Tactic:
by

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

Goal state before:
pp: α : Type u_4
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Option α) = Nat.card α + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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
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
j : η
hj : j ∉ I
heq : ¬j = i
⊢ j ∉ insert i I

Tactic:
by

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
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 = Function.update f₀ a b x

Tactic:
by

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
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
by

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, BijOn f s t

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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 η
I : Finset η
H : S
x : (i : η) → f i
h1 : ∀ i ∉ I, x i = 1
h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hc : t.encard < s.encard
hf : MapsTo f s t
⊢ ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ ∀ i ∉ Finset.univ, x i = 1

Tactic:
by

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
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
⊢ P N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : 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✝¹ : Finite η
inst✝ : DecidableEq η
H : S
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

Tactic:
by

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

Goal state before:
pp: P : Type u_4 → Prop
α : Type u_4
inst✝ : Finite α
hbase : ∀ (α : Type u_4) [Finite α] [Subsingleton α], P α
hstep : ∀ (α : Type u_4) [Finite α] [Nontrivial α], (∀ (β : Type u_4) [Finite β], Nat.card β < Nat.card α → P β) → P α
⊢ P α

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝² : (i : η) → MulOneClass (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H✝ : (i : η) → Submonoid (f i)
J : Submonoid ((i : η) → f i)
h : pi univ H✝ ≤ J
i : η
x✝¹ : (i : η) → f i
x✝ : x✝¹ ∈ map (MonoidHom.mulSingle f i) (H✝ i)
x : f i
hx : x ∈ ↑(H✝ i)
H : (MonoidHom.mulSingle f i) x = x✝¹
⊢ x✝¹ ∈ pi univ H✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.ncard ≤ k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : s.ncard ≤ k
⊢ s.encard = ↑s.ncard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
⊢ s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Finite

Goal state before:
pp: η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → MulOneClass (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ (pi univ fun i ↦ closure (s i)) ≤ closure (univ.pi fun i ↦ s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.ncard ≤ t.ncard

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).ncard = s.card

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
⊢ ∀ (x : ↥⊥), x ∈ {1}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : Nat.card ↥H = Nat.card G
⊢ H = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : H = ⊤
⊢ Nat.card ↥H = Nat.card G

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : H = ⊥
⊢ Nat.card ↥H ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_3
inst✝ : Group H
K : Subgroup G
f : G →* H
hf : Function.Injective ⇑f
⊢ Nat.card ↥(map f K) = Nat.card ↥K

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ ∅.ncard = 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 0 < s.ncard ↔ s.Nonempty

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.ncard = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑(t \ s) ≤ 0
⊢ t ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).ncard ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).ncard = s.ncard * t.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
i : η
_x : f i
hx : _x ∈ s i
j : η
⊢ (MonoidHom.mulSingle f i) _x j ∈ s j

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ (𝒫 s).ncard = 2 ^ s.ncard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card ↑t ≤ ENat.card ↑s
this : ENat.card ↑t ≤ 0 + ENat.card ↑s
⊢ ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Finite

Goal state before:
pp: η : Type u_3
f : η → Type u_4
inst✝¹ : (i : η) → Group (f i)
inst✝ : Finite η
s : (i : η) → Set (f i)
hs : ∀ (i : η), 1 ∈ s i
⊢ (pi univ fun i ↦ closure (s i)) ≤ closure (univ.pi fun i ↦ s i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∉ s
hs : s.Finite
⊢ (insert a s).ncard = s.ncard + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a s).ncard = s.ncard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
⊢ ENat.card ↑s < ENat.card ↑t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
e : α ≃ α
hs : s.Finite
h : ⇑e '' s = s
⊢ ⇑e '' s ⊆ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
s : Set α
hs : s.Finite
⊢ (insert a s).Finite

Tactic:
by

Goal state after:
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
val✝ : Fintype ↑S
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑((fun n ↦ x * n * x⁻¹) '' S)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
inst✝ : Finite α
⊢ l.length ≤ Nat.card α

Tactic:
by

Goal state after:
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
⊢ x ∈ normalizer S

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
h : l.Nodup
⊢ ↑l.length ≤ ENat.card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : s.Finite
⊢ (insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1

Tactic:
by

Goal state after: