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

Goal state before:
pp: case convert_3
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ t.ncard ≤ s.ncard

Tactic:
]

Goal state after:
case convert_3
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : t.ncard ≤ s.ncard
ht : t.Finite
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x ↦ ⟨f ↑x ⋯, ⋯⟩
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ t.ncard ≤ s.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g z : α
⊢ g⁻¹ * z ∈ s ↔ g⁻¹ * z ∈ s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ Quotient.mk'' x✝ = ↑x ↔ x✝ ∈ x • ↑s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ Quotient.mk'' x✝ = ↑x ↔ x✝ ∈ x • ↑s
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑{x | ↑x = ↑(Quotient.out L)}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑{x | ↑x = ↑(Quotient.out L)}
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
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩⁻¹ * ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩ ∈ s.subgroupOf t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
⊢ ⟨(f (Quotient.mk'' b))⁻¹ * b, ⋯⟩⁻¹ * ⟨(f (Quotient.mk'' c))⁻¹ * c, ⋯⟩ ∈ s.subgroupOf t
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.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
a : α ⧸ s
b c : α
h : (leftRel s) b c
key : f ↑b = f ↑c
⊢ (leftRel s) b c

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s) b c
key : f ↑b = f ↑c
⊢ (leftRel s) b c
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
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (f a.1 * ↑b)⁻¹ * (f a.1 * ↑c) ∈ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (f a.1 * ↑b)⁻¹ * (f a.1 * ↑c) ∈ s
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
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (↑b)⁻¹ * ↑c ∈ s

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
⊢ (↑b)⁻¹ * ↑c ∈ 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'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ s.toFinset → β := fun a h ↦ f a ⋯
⊢ s.ncard ≤ t.ncard

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 ⋯
⊢ s.ncard ≤ t.ncard
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ Finite ↥H ∧ Finite (G ⧸ H) ↔ Finite ↥H ∧ Finite (G ⧸ H)

Tactic:
]

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 ↥?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
β : Type u_2
s : Set α
f : α → β
⊢ s.ncard = s.ncard

Tactic:
]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
t : Set α
ht : t ∈ {t | t ⊆ ↑s ∧ t.ncard = n}
⊢ t.Finite

Tactic:
]

Goal state after:
α : Type u_1
n : ℕ
s : Finset α
t : Set α
ht : t ∈ {t | t ⊆ ↑s ∧ t.ncard = n}
⊢ t.Finite
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.encard + t.encard = s.encard + t.encard

Tactic:
]

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.ncard + t.ncard

Tactic:
]

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
]

Goal state after:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ 0 ≤ s.ncard + t.ncard

Tactic:
]

Goal state after:
case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ 0 ≤ s.ncard + t.ncard
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.encard + t.encard = s.encard + t.encard

Tactic:
]

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 = ∅ ↔ s ∩ t = ∅

Tactic:
]

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.encard = t.encard

Tactic:
]

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 \ s).ncard

Tactic:
]

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✝ : α
⊢ f a = f x✝ ↔ f a = f x✝

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑a.2 ∈ t

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑a.2 ∈ t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Group α
x y : α
h : x⁻¹ * y = 1
⊢ (id x)⁻¹ * id y = 1
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.ncard - ↑s.ncard = ↑t.ncard - ↑s.ncard

Tactic:
]

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

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

Tactic:
hs.sdiff.cast_ncard_eq

Goal state after:
case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ s.encard ≤ (s \ t).encard + t.encard
Module: Mathlib.Data.Set.Card

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

Tactic:
]

Goal state after:
case inl
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ s.encard ≤ (s \ t).encard + t.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case e'_3
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ ![] = ![]

Tactic:
]

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ ¬t ⊆ s
Module: Mathlib.Data.Set.Card

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

Tactic:
]

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

Tactic:
]

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 \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard

Tactic:
]

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Finite α
s : Set α
n : ℕ
h : sᶜ.ncard = n
⊢ sᶜ.ncard = n
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
⊢ sᶜ.ncard = 0 ↔ sᶜ.ncard = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Even (Nat.card α)
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:
]

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
  rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]

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

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
Module: Mathlib.Data.Set.Card

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h : (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty
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
⊢ 1 = 1

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty
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 ∈ φ.ker

Tactic:
]

Goal state after:
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 ∈ φ.ker
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
a : A
b : B
⊢ (a * (algebraMap R A) r, b * (algebraMap R B) r) = (a * (algebraMap R A) r, b * (algebraMap R B) r)

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty
Module: Mathlib.Data.Set.Card

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

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
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
⊢ 1 = 1

Tactic:
]

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

Goal state after:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ
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
a : A
b : B
⊢ ((algebraMap R A) r * a, (algebraMap R B) r * b) = ((algebraMap R A) r * a, (algebraMap R B) r * b)

Tactic:
]

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 φ) x = (kerLift φ) x

Tactic:
]

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

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

Tactic:
]

Goal state after:
case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n = t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
Module: Mathlib.GroupTheory.QuotientGroup.Basic

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

Tactic:
]

Goal state after:
A : Type u
inst✝ : CommGroup A
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ (MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out x))
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 : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (e.trans d) n) (Quotient.mk'' (Quotient.out x))

Tactic:
]

Goal state after:
A B C : Type u
inst✝² : CommGroup A
inst✝¹ : CommGroup B
inst✝ : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : A ⧸ (zpowGroupHom n).range
⊢ ((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n)) (Quotient.mk'' (Quotient.out x)) =
    (equivQuotientZPowOfEquiv (e.trans d) n) (Quotient.mk'' (Quotient.out x))
Module: Mathlib.Data.Set.Card

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

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').ncard = t'.card
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 N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩

Tactic:
]

Goal state after:
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 N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑(H ⊔ N)
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ k = k

pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ s.ncard ≤ k

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ s.ncard ≤ k
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
]

Goal state after:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
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 N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑H * ↑N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩

Tactic:
]

Goal state after:
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 N : Subgroup G
hLE : H ≤ normalizer ↑N
this✝ : (N.subgroupOf H).Normal := normal_subgroupOf_of_le_normalizer hLE
this : (N.subgroupOf (H ⊔ N)).Normal := normal_subgroupOf_sup_of_le_normalizer hLE
φ : ↥H →* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N) := (mk' (N.subgroupOf (H ⊔ N))).comp (inclusion ⋯)
x : ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
y : G
hy✝ : y ∈ H ⊔ N
hy : y ∈ ↑H * ↑N
⊢ ∃ a, φ a = Quotient.mk'' ⟨y, hy✝⟩
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
a : α
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset, insert a hs.toFinset = ht.toFinset

Tactic:
]

Goal state after:
case inl
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ hs.toFinset, insert a hs.toFinset = ht.toFinset
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
]

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
Module: Mathlib.Data.Set.Card

Goal state before:
pp: case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
]

Goal state after:
case inr
α : Type u_1
s : Set α
hs : s.Finite
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : Subsingleton α
s : Set α
⊢ ⋯.toFinset.card ≤ 1
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Finite ↑s
⊢ 1 < s.ncard ↔ 1 < s.ncard

Tactic:
]

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

Goal state before:
pp: case refine_1
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : Finite ↑s
⊢ s.Nontrivial ∧ s.Finite

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
s : Set α
hs : 1 < s.ncard
this : Finite ↑s
⊢ s.Nontrivial ∧ s.Finite