mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
s : Multiset ι
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
g : ι → M
⊢ (map (fun i ↦ f (g i)) s).prod = f (map g s).prod

Tactic:
convert! (s.map g).prod_hom f
  exact (map_map _ _ _).symm

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ ∀ (a : α), a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
⊢ ∀ (a : α), a ∈ m → ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) ⟦a✝⟧).prod = f (map f₁ ⟦a✝⟧).prod (map f₂ ⟦a✝⟧).prod

Tactic:
;

Goal state after:
case h
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) ⟦a✝⟧).prod = f (map f₁ ⟦a✝⟧).prod (map f₂ ⟦a✝⟧).prod
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
a✝ : β
⊢ a✝ ∈ s.disjiUnion (fun a ↦ {f a}) ⋯ ↔ a✝ ∈ map { toFun := f, inj' := hf } s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
hf : Function.Injective f
a✝ : β
⊢ a✝ ∈ s.disjiUnion (fun a ↦ {f a}) ⋯ ↔ a✝ ∈ map { toFun := f, inj' := hf } s
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ fold op (op (b a) (fold op b₀ (map b ha))) (t a + ha.bind t) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha))

Tactic:
fold_add,

Goal state after:
case cons
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha✝ : Std.Associative op
ι : Type u_4
t : ι → Multiset α
b : ι → α
b₀ : α
a : ι
ha : Multiset ι
ih : fold op (fold op b₀ (map b ha)) (ha.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha)
⊢ op (fold op (b a) (t a)) (fold op (fold op b₀ (map b ha)) (ha.bind t)) =
    op (fold op (b a) (t a)) (fold op b₀ (map (fun i ↦ fold op (b i) (t i)) ha))
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case H
n : ℕ
⊢ 0 < 2

Tactic:
;

Goal state after:
case H
n : ℕ
⊢ 0 < 2
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0

Tactic:
;

Goal state after:
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
⊢ Finite (α × β)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
⊢ Finite (α × β)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!

Tactic:
;

Goal state after:
case inr
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ = n + 1
⊢ (n + 1).choose (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
this : Finite α
⊢ Finite (α × β)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a : α
b : β
H : (Nonempty β → Finite α) ∧ (Nonempty α → Finite β)
this : Finite α
⊢ Finite (α × β)
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)

Tactic:
;

Goal state after:
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n.choose k * (k ! * (n - k)!)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b

Tactic:
;

Goal state after:
n a b : ℕ
h : n = a + b
this : (a + b).choose a = (a + b).choose b
⊢ n.choose a = n.choose b
Module: Mathlib.Data.Finset.Prod

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty

Tactic:
;

Goal state after:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ (s.pi t).Nonempty ↔ ∀ a ∈ s, (t a).Nonempty
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((a ::ₘ s.val).pi fun a ↦ (t a).val).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup

Tactic:
;

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((a ::ₘ s.val).pi fun a ↦ (t a).val).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup
Module: Mathlib.Data.Finset.Prod

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : α × α
⊢ a✝ ∈ s.diag ↔ a✝ ∈ {a ∈ s ×ˢ s | a.1 = a.2}

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a✝ : α × α
⊢ a✝ ∈ s.diag ↔ a✝ ∈ {a ∈ s ×ˢ s | a.1 = a.2}
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: case e_f
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)) = fun b ↦
    (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup

Tactic:
;

Goal state after:
case e_f
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)) = fun b ↦
    (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup
Module: Mathlib.Data.Multiset.Pi

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

Tactic:
;

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
⊢ ((t a).bind fun b ↦ map (Pi.cons (a ::ₘ m) a b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)) ≍
    (t a).bind fun b ↦ map (Pi.cons (a ::ₘ m) a b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(s.piDiag ι) = #s

Tactic:
rw [piDiag, card_image_of_injective _ const_injective]

Goal state after:
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)
a✝ : (a : α) → δ a
⊢ (a✝ ∈ piFinset fun a ↦ image (f a) (s a)) ↔ a✝ ∈ image (fun b a ↦ f a (b a)) (piFinset s)

Tactic:
;

Goal state after:
α : 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)
a✝ : (a : α) → δ a
⊢ (a✝ ∈ piFinset fun a ↦ image (f a) (s a)) ↔ a✝ ∈ image (fun b a ↦ f a (b a)) (piFinset s)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
;

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((t a).bind fun b ↦ map (Pi.cons (a' ::ₘ m) a b) ((t a').bind fun b ↦ map (Pi.cons m a' b) n)) ≍
    (t a').bind fun b ↦ map (Pi.cons (a ::ₘ m) a' b) ((t a).bind fun b ↦ map (Pi.cons m a b) n)

Tactic:
simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b _
        apply bind_hcongr
        · rw [cons_swap a a']
        intro b' _
        apply map_hcongr
        · rw [cons_swap a a']
        intro f _
        exact Pi.cons_swap eq

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
  cases n
  · cases k
    · rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
    · simp only [zero_ascFactorial, Nat.zero_add, succ_sub_succ_eq_sub,
        Nat.sub_zero, choose_succ_self, Nat.mul_zero]
  rw [ascFactorial_eq_factorial_mul_choose]
  simp only [succ_add_sub_one]

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
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
hs : ¬a ∈ s ∧ s.Nodup
⊢ ¬a ∈ s

Tactic:
;

Goal state after:
α : 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
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
hs : ¬a ∈ s ∧ s.Nodup
⊢ ¬a ∈ s
Module: Mathlib.Data.Fintype.Pi

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

Tactic:
;

Goal state after:
α : Type u_3
β : α → Type u_4
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : (a : α) → Fintype (β a)
a✝ : (a : α) → a ∈ univ → β a
⊢ (a✝ ∈ univ.pi fun a ↦ univ) ↔ a✝ ∈ univ
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
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : ¬a ∈ s ∧ s.Nodup
⊢ s.Nodup

Tactic:
;

Goal state after:
α : 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
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : ¬a ∈ s ∧ s.Nodup
⊢ s.Nodup
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
apply Nat.mul_le_mul_left

Goal state after:
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case succ
a c b_n : ℕ
b_ih : a.choose c ≤ (a + b_n).choose c
⊢ a.choose c ≤ (a + (b_n + 1)).choose c

Tactic:
| succ b_n b_ih =>

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

Goal state before:
pp: case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1

Tactic:
;

Goal state after:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
h : a✝ ∈ 0
⊢ Pi.empty β a✝ h ∈ t a✝

Tactic:
;

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ 0 → β a
this : f = Pi.empty β
a✝ : α
h : a✝ ∈ 0
⊢ Pi.empty β a✝ h ∈ t a✝
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:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
q : Subsemigroup M
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
q : Subsemigroup M
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝ } = q
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s carrier✝¹ : Set M
mul_mem'✝¹ : ∀ {a b : M}, a ∈ carrier✝¹ → b ∈ carrier✝¹ → a * b ∈ carrier✝¹
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ }.carrier = { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ } = { carrier := carrier✝, mul_mem' := mul_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s carrier✝¹ : Set M
mul_mem'✝¹ : ∀ {a b : M}, a ∈ carrier✝¹ → b ∈ carrier✝¹ → a * b ∈ carrier✝¹
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ }.carrier = { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ } = { carrier := carrier✝, mul_mem' := mul_mem'✝ }
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ univ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ univ

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ univ
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
⊢ f '' ⋃ i, s i = ⋃ i, f '' s i

Tactic:
ext1 x
  simp only [mem_image, mem_iUnion, ← exists_and_right, exists_comm (α := α)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
x✝ : α
⊢ x✝ ∈ f ⁻¹' ⋂ i, s i ↔ x✝ ∈ ⋂ i, f ⁻¹' s i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
x✝ : α
⊢ x✝ ∈ f ⁻¹' ⋂ i, s i ↔ x✝ ∈ ⋂ i, f ⁻¹' s i
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
x✝ : α × β
⊢ x✝ ∈ 1 ×ˢ 1 ↔ x✝ ∈ 1

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
x✝ : α × β
⊢ x✝ ∈ 1 ×ˢ 1 ↔ x✝ ∈ 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
⊢ 1 ×ˢ 1 = 1

Tactic:
by ext; simp [Prod.ext_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i✝ : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
i : ι
⊢ a i = b i

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u_2
I : Type u
f : I → Type v
M : ι → Type u_3
N : ι → Type u_4
i✝ : I
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), IsMulTorsionFree (M i)
n : ℕ
hn : n ≠ 0
a b : (i : ι) → M i
hab : (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b
i : ι
⊢ a i = b i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_7
x✝² x✝¹ : I → α
x✝ : I
⊢ (⇑f ∘ (x✝² * x✝¹)) x✝ = (⇑f ∘ x✝² * ⇑f ∘ x✝¹) x✝

Tactic:
;

Goal state after:
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → Mul (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
I : Type u_7
x✝² x✝¹ : I → α
x✝ : I
⊢ (⇑f ∘ (x✝² * x✝¹)) x✝ = (⇑f ∘ x✝² * ⇑f ∘ x✝¹) x✝
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun x ↦ f x⁻¹) '' s = g '' s

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : InvolutiveInv α
s : Set α
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = g x
⊢ (fun x ↦ f x⁻¹) '' s = g '' s
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝ : I
⊢ (⇑f ∘ 1) x✝ = 1 x✝

Tactic:
;

Goal state after:
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝ : I
⊢ (⇑f ∘ 1) x✝ = 1 x✝
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (z, w) ∈ ⋃ x, s x ×ˢ t x ↔ (z, w) ∈ (⋃ x, s x) ×ˢ ⋃ x, t x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (z, w) ∈ ⋃ x, s x ×ˢ t x ↔ (z, w) ∈ (⋃ x, s x) ×ˢ ⋃ x, t x
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝² x✝¹ : I → α
x✝ : I
⊢ (⇑f ∘ (x✝² * x✝¹)) x✝ = (⇑f ∘ x✝² * ⇑f ∘ x✝¹) x✝

Tactic:
;

Goal state after:
ι : Type u_1
α✝ : Type u_2
I✝ : Type u
f✝ : I✝ → Type v
M : ι → Type u_3
N : ι → Type u_4
i : I✝
inst✝² : (i : I✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
x✝² x✝¹ : I → α
x✝ : I
⊢ (⇑f ∘ (x✝² * x✝¹)) x✝ = (⇑f ∘ x✝² * ⇑f ∘ x✝¹) x✝
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)

Tactic:
;

Goal state after:
I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
i j : I
hij : i ≠ j
x : f i
y : f j
⊢ Commute (mulSingle i x) (mulSingle j y)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ x✝ ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x✝ ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ x✝ ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x✝ ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ (∃ a b, (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ a_1 b_1, (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x✝) ↔
    (∃ x, x ∈ s₁ ∧ ∃ y, y ∈ s₂ ∧ x * y = x✝.1) ∧ ∃ x, x ∈ t₁ ∧ ∃ y, y ∈ t₂ ∧ x * y = x✝.2

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Mul α
inst✝ : Mul β
s₁ s₂ : Set α
t₁ t₂ : Set β
x✝ : α × β
⊢ (∃ a b, (a ∈ s₁ ∧ b ∈ t₁) ∧ ∃ a_1 b_1, (a_1 ∈ s₂ ∧ b_1 ∈ t₂) ∧ (a * a_1, b * b_1) = x✝) ↔
    (∃ x, x ∈ s₁ ∧ ∃ y, y ∈ s₂ ∧ x * y = x✝.1) ∧ ∃ x, x ∈ t₁ ∧ ∃ y, y ∈ t₂ ∧ x * y = x✝.2
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : Monoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ n * s).Nonempty
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst✝ : γ
snd✝ : δ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ fst✝ ∈ f a ∧ snd✝ ∈ g b) ↔ (∃ i ∈ s, fst✝ ∈ f i) ∧ ∃ i ∈ t, snd✝ ∈ g i

Tactic:
;

Goal state after:
δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst✝ : γ
snd✝ : δ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ fst✝ ∈ f a ∧ snd✝ ∈ g b) ↔ (∃ i ∈ s, fst✝ ∈ f i) ∧ ∃ i ∈ t, snd✝ ∈ g i