mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Finite

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
⊢ Nat.card { x // p x } = s.card

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ lift.{u, v} #β < ℵ₀

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ Nat.card α ≤ Nat.card β

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ lift.{v, u} #α < ℵ₀

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
this : lift.{u, v} #β ≤ lift.{v, u} #α
⊢ Nat.card β ≤ Nat.card α

Tactic:
simpa using! toNat_le_toNat this (by simp)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
f : α → β
hf : Surjective f
⊢ Nat.card β ≤ Nat.card α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j with ↑j < i, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
⊢ ∀ (j : Fin n), (↑j < i.succ) = (↑j < i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
i : ℕ
⊢ (take i (ofFn f)).prod = ∏ j with ↑j < i, f j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
⊢ [].alternatingProd = ∏ i, [][i] ^ (-1) ^ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g : G
⊢ [g].alternatingProd = ∏ i, [g][i] ^ (-1) ^ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: G : Type u_3
inst✝ : DivisionCommMonoid G
g h : G
L : List G
⊢ g * h⁻¹ * ∏ i, L[i] ^ (-1) ^ ↑i = ∏ i, (g :: h :: L)[i] ^ (-1) ^ ↑i

Tactic:
by

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (span R (range (v ∘ Sum.inl))) (span R (range (v ∘ Sum.inr)))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
⊢ Bijective f ↔ Injective f ∧ Nat.card α = Nat.card β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
⊢ ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
h₁ : ∑ i, (-1) ^ ↑i • d i = d 0 + ∑ i, (-1) ^ (↑i + 1) • d i.castSucc.succ + (-1) ^ (n + 1) • d (last (n + 1))
⊢ ∑ i, (-1) ^ (↑i + 1) • (r i.castSucc + r i.succ) =
    ∑ i, (-1) ^ (↑i + 1) • r i.castSucc + ∑ i, (-1) ^ (↑i + 1) • r i.succ

Tactic:
by

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

Goal state before:
pp: ι : 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
⊢ LinearIndependent R v ↔
    ∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: α : Type u_3
inst✝ : AddCommGroup α
n : ℕ
d : Fin (n + 2) → α
r : Fin (n + 1) → α
h_first : d 0 = r 0
h_mid : ∀ (i : Fin n), d i.succ.castSucc = r i.castSucc + r i.succ
h_last : d (last (n + 1)) = r (last n)
⊢ ∑ i, (-1) ^ ↑i • d i = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
a✝ : Nontrivial R
⊢ Disjoint (span R (range fun x ↦ v ↑x)) (span R (range fun x ↦ v ↑x))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
⊢ Bijective f ↔ Surjective f ∧ Nat.card α = Nat.card β

Tactic:
by

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

Goal state before:
pp: α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Nat.card (Fin n) = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
⊢ Nat.card ↑(f '' s) = Nat.card ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hs : LinearIndepOn R v s
ht : LinearIndepOn R v t
hdj : Disjoint (span R (v '' s)) (span R (v '' t))
⊢ LinearIndepOn R v (s ∪ t)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hs : LinearIndepOn R id s
ht : LinearIndepOn R id t
hdj : Disjoint (span R s) (span R t)
⊢ Disjoint (span R (id '' s)) (span R (id '' t))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card ↑(range f) = Nat.card α

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
t : Set ι
hdj : Disjoint s t
⊢ LinearIndepOn R v (s ∪ t) ↔ LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (span R (v '' s)) (span R (v '' t))

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
⊢ α ≃ Fin (Nat.card α)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set M
hdj : Disjoint s t
⊢ LinearIndepOn R id (s ∪ t) ↔ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Nat.card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ Nat.card (α × β) = Nat.card α * Nat.card β

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Tactic:
let _ (a : α) : Fintype (β a) := Fintype.ofFinite (β a)

Goal state after:
α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
x✝ : (a : α) → Fintype (β a) := fun a ↦ Fintype.ofFinite (β a)
⊢ Nat.card (Sigma β) = ∑ a, Nat.card (β a)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝¹ : Fintype α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Nat.card (Sigma β) = ∑ a, Nat.card (β a)

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ s, (g i * i x - g i * a x) • ⇑i) y = ∑ i ∈ s, g i * i x * i y - ∑ i ∈ s, g i * a x * i y

Tactic:
by

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

Goal state before:
pp: ι : 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
⊢ ¬LinearIndependent R v ↔ ∃ s t f, Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, 0 < f i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ toNat (lift.{u_1, u_3} (∏ i, #(β i))) = ∏ a, toNat #(β a)

Tactic:
toNat_lift,

Goal state after:
α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ toNat (∏ i, #(β i)) = ∏ a, toNat #(β a)
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a, Nat.card (β a)

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ s, g i * i x * i y - ∑ i ∈ s, g i * a x * i y =
    ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Nat.card (ZMod n) = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
t : Set β
⊢ Nat.card ↑({a} ×ˢ t) = Nat.card ↑t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ Nat.card ↑(s ×ˢ {b}) = Nat.card ↑s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Nat.card ↑(graphOn f s) = Nat.card ↑s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ card α = ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ card α = ⊤ ↔ Infinite α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ card α < ⊤

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ card α < ⊤ ↔ Finite α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ card (α ⊕ β) = card α + card β

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card α ≤ card β

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n ≤ toENat c ↔ ↑n ≤ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_3}
n : ℕ
⊢ toENat c ≤ ↑n ↔ c ≤ ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n = toENat c ↔ ↑n = c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_3}
n : ℕ
⊢ toENat c = ↑n ↔ c = ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ ↑n < toENat c ↔ ↑n < c

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ toENat c < ↑n ↔ c < ↑n

Tactic:
simp only [← not_le, Cardinal.natCast_le_toENat]

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_3}
⊢ toENat c < ↑n ↔ c < ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ card α = 0 ↔ IsEmpty α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ card α ≠ 0 ↔ Nonempty α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ 0 < card α ↔ Nonempty α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ 1 ≤ card α ↔ Nonempty α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nonempty α
⊢ 0 < card α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
⊢ card α ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ card α = 1 ↔ Nonempty (Unique α)

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * i x * i y - ∑ i ∈ insert a s, g i * a x * i y =
    ∑ i ∈ insert a s, g i * (i x * i y) - ∑ i ∈ insert a s, a x * (g i * i y)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
⊢ 1 < card α ↔ Nontrivial α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Nontrivial α
⊢ 1 < card α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ card α
x y : α
⊢ 3 ≤ #α

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ card (α × β) = card α * card β

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * (i x * i y) - ∑ i ∈ insert a s, a x * (g i * i y) =
    (∑ i ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y = 0

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
⊢ g i • ⇑i = g i • ⇑a

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
i : G →* L
his : i ∈ s
⊢ ∃ y, i y ≠ a y

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
⊢ card (α → β) = card β ^ card α

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
i : G →* L
his : i ∈ s
⊢ g i = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type w
v : ι → M
hv : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type v
v : ι → M
hv : LinearIndependent R v
⊢ #ι ≤ Module.rank R M

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
ι : Type u_1
v : ι → M
s : Set ι
hs : LinearIndepOn R v s
⊢ s.encard ≤ toENat (Module.rank R M)

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
⊢ ?m.41 < iSup ?m.43

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h✝ : lift.{v, w} c < lift.{w, v} (Module.rank R M)
c' : Cardinal.{v}
hc' : c' < Module.rank R M
hcc' : lift.{w, v} c' = lift.{v, w} c
s : Set M
hs : LinearIndepOn R id s
h : c' < #↑↑⟨s, hs⟩
t : Set M
hst : t ⊆ ↑⟨s, hs⟩
ht : #↑t = c'
⊢ lift.{w, v} #↑t = lift.{v, w} c

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{w}
h : lift.{v, w} c < lift.{w, v} (Module.rank R M)
⊢ ∃ s, lift.{w, v} #↑s = lift.{v, w} c ∧ LinearIndepOn R id s

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : Cardinal.{v}
h : c < Module.rank R M
⊢ ∃ s, #↑s = c ∧ LinearIndepOn R id s

Tactic:
by

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

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ g a * 1 = (g a • ⇑a) 1

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
n : ℕ
s : { s // LinearIndepOn R id s }
le : ↑(n + 1) ≤ #↑↑s
t : Finset ↑↑s
ht : n + 1 = t.card
⊢ (Finset.map (Embedding.subtype fun x ↦ x ∈ ↑s) t).card = n + 1

Tactic:
by

Goal state after: