mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ ∈ s.toFinset

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 : (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₂ ∈ s.toFinset

Tactic:
by

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

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 : (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 ⋯
⊢ f'' a₁ ⋯ = f'' a₂ ⋯

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 : (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
⊢ a₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ RightInverse (fun a ↦ Quotient.map' (fun b ↦ f a.1 * ↑b) ⋯ a.2) fun a ↦
    (Quotient.map' id ⋯ a, Quotient.map' (fun g ↦ ⟨(f (Quotient.mk'' g))⁻¹ * g, ⋯⟩) ⋯ a)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
s : Set α
⊢ univ.ncard = s.ncard

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s)) a b → (leftRel (H.subgroupOf t)) ((inclusion h) a) ((inclusion h) b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
h₁ : {t | t ⊆ ↑s ∧ t.ncard = n} ⊆ range SetLike.coe
⊢ SetLike.coe ⁻¹' {t | t ⊆ ↑s ∧ t.ncard = n} = ↑(Finset.powersetCard n s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
n : ℕ
⊢ {t | t ⊆ s ∧ t.ncard = n}.ncard = s.ncard.choose n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
⊢ ∀ (a₁ a₂ : ↥s),
    Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a₁) = Quotient.map' ⇑(inclusion h) ⋯ (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
by

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

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ (leftRel (s.subgroupOf H)) a b → (leftRel (t.subgroupOf H)) (id a) (id b)

Tactic:
by

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

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ (leftRel s) a b → (leftRel t) (id a) (id b)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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.ncard + t.ncard ↔ Disjoint s t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ (t \ s).ncard + s.ncard = t.ncard

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : ↥H),
    (fun q i ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁) =
        (fun q i ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

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
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (fun q i ↦ quotientMapOfLE ⋯ q) (Quotient.mk'' a₁) = (fun q i ↦ quotientMapOfLE ⋯ q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ x✝ ∈ ⇑f ⁻¹' {f a} ↔ x✝ ∈ a • ↑f.ker

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : ↥s × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (fun a ↦ (⟨(Quotient.out ↑↑a)⁻¹ * ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) ((fun a ↦ ⟨Quotient.out ↑a.2 * ↑a.1, ⋯⟩) (⟨a, ha⟩, ⟨x, hx⟩)) =
    (⟨a, ha⟩, ⟨x, hx⟩)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ univ = ⋃ x, Quotient.out x • ↑H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x y : α
h : (leftRel ⊥) x y
⊢ (id x)⁻¹ * id y = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α ⧸ ⊥
⊢ ↑(Quotient.lift id ⋯ x) = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
x : α
⊢ Quotient.lift id ⋯ ↑x = x

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.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
by

Goal state after:
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 = i.removeNth (Pi.mulSingle i x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
R : Type u_3
inst✝ : AddGroupWithOne R
hst : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard = ↑t.ncard - ↑s.ncard

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (j : Fin (n + 1)) → Group (α j)
i : Fin (n + 1)
x y : α i
p : (j : Fin n) → α (i.succAbove j)
⊢ i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)

Tactic:
by

Goal state after:
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 → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ finZeroElim = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : Zero α
v : Fin n → α
x : α
x✝ : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Fin.Tuple

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

Tactic:
by

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

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

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
U : Set (G ⧸ N)
g : ↥N.op
⊢ g • ⇑(mk' N) ⁻¹' U = ⇑(mk' N) ⁻¹' U

Tactic:
by

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

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

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
A : Subgroup G
B : Subgroup H
q : (G × H) ⧸ A.prod B
⊢ ∀ (a b : G × H),
    (leftRel (A.prod B)) a b →
      (match a with
        | (g, h) => (↑g, ↑h)) =
        match b with
        | (g, h) => (↑g, ↑h)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
A : Subgroup G
B : Subgroup H
q : (G ⧸ A) × H ⧸ B
⊢ ∀ (a₁ : G) (a₂ : H) (b₁ : G) (b₂ : H), (leftRel A) a₁ b₁ → (leftRel B) a₂ b₂ → ↑(a₁, a₂) = ↑(b₁, b₂)

Tactic:
by

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

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 = Nat.card α - s.ncard

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
A : Subgroup G
B : Subgroup H
q : (G × H) ⧸ A.prod B
⊢ ∀ (a : G × H),
    (fun q ↦ Quotient.liftOn₂' q.1 q.2 (fun g h ↦ ↑(g, h)) ⋯)
        ((fun q ↦
            Quotient.liftOn' q
              (fun x ↦
                match x with
                | (g, h) => (↑g, ↑h))
              ⋯)
          (Quotient.mk'' a)) =
      Quotient.mk'' a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
n : ℕ
h : Nat.card α = n + s.ncard
⊢ sᶜ.ncard = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
⊢ s = univ ↔ s.ncard = Nat.card α

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
A : Subgroup G
B : Subgroup H
x✝ : (G ⧸ A) × H ⧸ B
q₁ : G ⧸ A
q₂ : H ⧸ B
⊢ ∀ (a₁ : G) (a₂ : H),
    (fun q ↦
          Quotient.liftOn' q
            (fun x ↦
              match x with
              | (g, h) => (↑g, ↑h))
            ⋯)
        ((fun q ↦ Quotient.liftOn₂' q.1 q.2 (fun g h ↦ ↑(g, h)) ⋯) (Quotient.mk'' a₁, Quotient.mk'' a₂)) =
      (Quotient.mk'' a₁, Quotient.mk'' a₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Even sᶜ.ncard ↔ Even s.ncard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Odd sᶜ.ncard ↔ Odd s.ncard

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < s.ncard + t.ncard
⊢ (s ∩ t).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ (leftRel φ.ker) a b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ a = φ b
⊢ (leftRel φ.ker) a b

Tactic:
by rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_cancel]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
g : G
hg : g ∈ φ.ker
⊢ g ∈ φ.rangeRestrict.ker

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (r : R) (x : A × B), ((algebraMap R A).prod (algebraMap R B)) r * x = x * ((algebraMap R A).prod (algebraMap R B)) r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ s.ncard + t.ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ φ.ker
a b : G
h : φ.rangeRestrict a = φ.rangeRestrict b
⊢ (leftRel φ.ker) a b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ (sᶜ ∩ tᶜ).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
φ : G →* H
⊢ Surjective ⇑(rangeKerLift φ)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
ψ : H → G
hφ : RightInverse ψ ⇑φ
x : G ⧸ φ.ker
⊢ (kerLift φ) ((mk ∘ ψ) ((kerLift φ) x)) = (kerLift φ) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (r : R) (x : A × B), r • x = ((algebraMap R A).prod (algebraMap R B)) r * x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
⊢ (quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯) = MonoidHom.id (↥A ⧸ A'.subgroupOf A)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
r : R
⊢ (↑↑(f.prod g.toRingHom)).toFun ((algebraMap R A) r) = (algebraMap R (B × C)) r

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝¹ : Group H
M : Type x
inst✝ : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
⊢ (quotientMapSubgroupOfOfLe ⋯ ⋯).comp (quotientMapSubgroupOfOfLe ⋯ ⋯) = MonoidHom.id (↥B ⧸ B'.subgroupOf B)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst✝⁴ : Group H
M : Type x
inst✝³ : Monoid M
φ : G →* H
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
f : A →* B
g✝ : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
g : A
x✝ : g ∈ (zpowGroupHom n).range
h : A
hg : h ^ n = g
⊢ (zpowGroupHom n) (f h) = f g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: A : Type u
inst✝ : CommGroup A
n : ℤ
⊢ MulEquiv.refl (A ⧸ (zpowGroupHom n).range) = equivQuotientZPowOfEquiv (MulEquiv.refl A) n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
⊢ s.card ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∅.ncard ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A →ₐ[R] B
g : A →ₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∃ t ⊆ s, t.ncard = n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ Subtype.val '' ↑t' ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').Finite

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
D : Type u_5
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] B
g : C →ₐ[R] D
r : R
⊢ (↑↑(f.prodMap g.toRingHom)).toFun ((algebraMap R (A × C)) r) = (algebraMap R (B × D)) r

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B✝ : Type u_3
C : Type u_4
inst✝¹⁴ : CommSemiring R
inst✝¹³ : Semiring A✝
inst✝¹² : Algebra R A✝
inst✝¹¹ : Semiring B✝
inst✝¹⁰ : Algebra R B✝
inst✝⁹ : Semiring C
inst✝⁸ : Algebra R C
S : Type u_5
T : Type u_6
A : Type u_7
B : Type u_8
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring S
inst✝⁴ : Semiring T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra R A
inst✝ : Algebra R B
l : S ≃ₐ[R] A
r : T ≃ₐ[R] B
⊢ ∀ (x : R), (l.toRingEquiv.prodCongr r.toRingEquiv) ((algebraMap R (S × T)) x) = (algebraMap R (A × B)) x

Tactic:
by

Goal state after: