mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
⊢ (piFinset fun a ↦ image (f a) (s a)) = image (fun b a ↦ f a (b a)) (piFinset s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b ↦ if h : a = b then h ▸ x else f b h) ∈ piFinset t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b ↦ if h : a = b then h ▸ x else f b h) a = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * (n + k).choose k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun f ↦ f a) (piFinset t) = t a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a a' : α) (m : Multiset α) (b : Multiset ((a : α) → a ∈ m → β a)),
    ((t a).bind fun b_1 ↦ map (Pi.cons (a' ::ₘ m) a b_1) ((t a').bind fun b_2 ↦ map (Pi.cons m a' b_2) b)) ≍
      (t a').bind fun b_1 ↦ map (Pi.cons (a ::ₘ m) a' b_1) ((t a).bind fun b_2 ↦ map (Pi.cons m a b_2) b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ (pi 0 t).card = (map (fun a ↦ (t a).card) 0).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.pi t).card = (map (fun a ↦ (t a).card) s).prod →
      ((a ::ₘ s).pi t).card = (map (fun a ↦ (t a).card) (a ::ₘ s)).prod

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ n.ascFactorial k = k ! * (n + k - 1).choose k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s t : (a : α) → Finset (δ a)
⊢ (piFinset fun i ↦ s i ∩ t i) = piFinset s ∩ piFinset t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ {f ∈ piFinset t | f a = x} = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k).choose k = (n + 1).ascFactorial k / k !

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
t : Finset (δ i)
hts : t ⊆ s i
⊢ piFinset (update s i t) = {f ∈ piFinset s | f i ∈ t}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
a : δ i
ha : a ∈ s i
⊢ piFinset (update s i {a}) = {f ∈ piFinset s | f i = a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
⊢ ¬a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ ∀ (x : (a : α) → β a), x ∈ Fintype.piFinset fun x ↦ univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type ?u.6
β : Type ?u.8
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Fintype (α ↪ β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
⊢ (univ.pi fun a ↦ univ) = univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
⊢ s.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ n.choose r ≤ n.choose (r + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n r : ℕ
hr : r ≤ n / 2
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ {f ∈ Fintype.piFinset fun x ↦ s | ∃ a ∈ s, const ι a = f} = s.piDiag ι

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
⊢ n.choose r ≤ n.choose (n / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : DecidableEq (ι → α)
s : Finset α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ s.piDiag ι ⊆ Fintype.piFinset fun x ↦ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: a c : ℕ
⊢ a.choose c ≤ a.succ.choose c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: a b c : ℕ
⊢ a.choose c ≤ (a + b).choose c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ (univ.pi t).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n.multichoose 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ {f | ∀ (i : ι), f i ∈ t i}.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: k : ℕ
⊢ multichoose 1 k = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (Fin.cons s f) = s ∪ ⋃ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
⊢ Pi.cons s a b₁ f a ⋯ = Pi.cons s a b₂ g a ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
⊢ iUnion (Fin.snoc f s) = (⋃ i, f i) ∪ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: k : ℕ
⊢ multichoose 2 k = k + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = f 0 ∪ iUnion (f ∘ Fin.succ)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n.multichoose 1 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
⊢ x✝.multichoose 0 = (x✝ + 0 - 1).choose 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: k : ℕ
⊢ multichoose 0 (k + 1) = (0 + (k + 1) - 1).choose (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin (n + 1) → Set α
⊢ ⋃ i, f i = iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup) →
      (a ::ₘ s).Nodup → (∀ (a_3 : α), a_3 ∈ a ::ₘ s → (t a_3).Nodup) → ((a ::ₘ s).pi t).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).multichoose (k + 1) = (n + 1 + (k + 1) - 1).choose (k + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
⊢ f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: M✝ : Type u_1
G : Type u_2
α✝ : Type u_3
β : Type u_4
M : Type u_5
α : Type u_6
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Subsingleton α
x y : α
⊢ 1 • x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
g h : G
⊢ (h * g⁻¹) • g • x₀ = h • x₀

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pretransitive

Goal state before:
pp: G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
⊢ IsPretransitive G X

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Finite (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
⊢ Finite (α ↪ β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : Sort u_4
inst✝ : Finite β
e₁ e₂ : α ≃ β
h : e₁.toEmbedding = e₂.toEmbedding
⊢ ∀ (x : α), e₁ x = e₂ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ ∀ (x : α × β), x ∈ s.toFinset ×ˢ t.toFinset ↔ x ∈ s ×ˢ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
inst✝ : Fintype ↑s
⊢ ∀ (x : α × α), x ∈ s.toFinset.offDiag ↔ x ∈ s.offDiag

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
hs : Fintype ↑s
ht : Fintype ↑t
⊢ Fintype ↑(image2 f s t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(image2 f s t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ (s ×ˢ t).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
⊢ (image2 f s t).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
hs : s.Finite
ht : t.Finite
⊢ ∀ (a : α × β), a ∈ hs.toFinset ×ˢ ht.toFinset ↔ a ∈ ⋯.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ ∀ (a : α × α), a ∈ ⋯.toFinset ↔ a ∈ hs.toFinset.offDiag

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
h : (image2 f s t).Infinite
⊢ (s ×ˢ t).Infinite

Tactic:
rw [← image_uncurry_prod] at h
    exact h.of_image _

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun a ↦ f a b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hfs : ∀ b ∈ t, InjOn (fun x ↦ f x b) s
hft : ∀ a ∈ s, InjOn (f a) t
⊢ (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ DecidablePred fun x ↦ x ∈ s ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
⊢ s⁻¹.Finite ↔ s.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
⊢ ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ Fintype ↑(S ^ n * Set.singleton a)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
⊢ S ^ n * {a} = S ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
⊢ ∀ (k : ℕ), Fintype.card G ≤ k → Fintype.card ↑(S ^ k) = Fintype.card ↑(S ^ Fintype.card G)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
a b : R
x : M
⊢ (f a * f b) • x = f a • f b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ 1 • b = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝² x✝¹ : N
x✝ : α
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : Monoid N
g : N →* M
x✝ : α
⊢ 1 • x✝ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
⊢ IsPretransitive E G

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
M : Type ?u.7
N : Type ?u.9
inst✝³ : Monoid M
inst✝² : MulOneClass N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
x y : M
⊢ (x * y) • 1 = x • 1 * y • 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
M : Type u_2
N : Type u_3
A : Type u_4
α : Type u_5
⊢ MulAction.IsPretransitive (Perm α) α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ toPerm 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.End

Goal state before:
pp: G : Type u_1
α : Type u_5
inst✝¹ : AddGroup G
inst✝ : AddAction G α
⊢ toPerm 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a * ↑c = b * ↑c
⊢ a = b

Tactic:
← Units.mul_inv_eq_iff_eq_mul,

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : a * ↑c * ↑c⁻¹ = b
⊢ a = b
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
x✝ : IsConj a b
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a = b
⊢ IsConj a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ SemiconjBy (↑((Units.map f) c)) (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
h : a = 1
⊢ IsConj 1 a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ IsConj 1 a ↔ a = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
a b : α
⊢ (b * a * b⁻¹)⁻¹ = b * a⁻¹ * b⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
a b c : α
⊢ b * a * b⁻¹ * (b * c * b⁻¹) = b * (a * c) * b⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
i : ℕ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
i : ℤ
a b : α
⊢ (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Group α
x a b : α
⊢ (fun g ↦ x * g * x⁻¹) a = (fun g ↦ x * g * x⁻¹) b → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
⊢ Function.Surjective (map f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.RightInverse (Quotient.lift id ⋯) ConjClasses.mk

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
revert b
  rw [forall_isConj]
  intro b
  rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
  rfl

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f sᶜ = (f '' s)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (range f)ᶜ ⊆ kernImage f s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
p q : Subsemigroup M
h : p.carrier = q.carrier
⊢ p = q

Tactic:
by

Goal state after: