mathlib-initiative/mathlib-tactics huggingface dataset:
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:
ext

Goal state after:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
x✝ : α
⊢ x✝ ∈ iUnion (Fin.cons s f) ↔ x✝ ∈ s ∪ ⋃ i, f i
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:
ext

Goal state after:
α : Type u_1
n : ℕ
f : Fin n → Set α
s : Set α
x✝ : α
⊢ x✝ ∈ iUnion (Fin.snoc f s) ↔ x✝ ∈ (⋃ i, f i) ∪ s
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) ↔
    ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1

Tactic:
constructor

Goal state after:
case cons.mp
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∃ a_1, a_1 ∈ t a ∧ ∃ a_2, (∀ (a : α) (h : a ∈ m), a_2 a h ∈ t a) ∧ Pi.cons m a a_1 a_2 = f) →
    ∀ (a_2 : α) (h : a_2 ∈ a ::ₘ m), f a_2 h ∈ t a_2

case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ (∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1) →
    ∃ a_2, a_2 ∈ t a ∧ ∃ a_3, (∀ (a : α) (h : a ∈ m), a_3 a h ∈ t a) ∧ Pi.cons m a a_2 a_3 = f
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:
constructor

Goal state after:
G : Type u_2
X : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G X
x₀ : X
ha : ∀ (x : X), ∃ g, g • x₀ = x
⊢ ∀ (x y : X), ∃ g, g • x = y
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬s.Finite ∧ t.Nonempty ∨ ¬t.Finite ∧ s.Nonempty

Tactic:
@and_comm ¬_,

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ Subsingleton M

Tactic:
constructor

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: case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
· simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
⊢ f '' ⋃₀ s = ⋃₀ (image f '' s)

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set α)
x✝ : β
⊢ x✝ ∈ f '' ⋃₀ s ↔ x✝ ∈ ⋃₀ (image f '' s)
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:
ext

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.Data.Set.Lattice.Image

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

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ⋃ i, t i ↔ x✝ ∈ ⋃ i, s ×ˢ t i
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:
ext

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
x✝ : α × β
⊢ x✝ ∈ 1 ×ˢ 1 ↔ x✝ ∈ 1
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
⊢ (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ i, s i) ×ˢ t ↔ x✝ ∈ ⋃ i, s i ×ˢ t
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 → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
ext

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.Data.Set.Lattice.Image

Goal state before:
pp: ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
⊢ ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i

Tactic:
ext

Goal state after:
ι : Type u_9
ι' : Type u_10
α : Type u_11
β : Type u_12
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ x✝ ∈ ⋃ x, s x.1 ×ˢ t x.2 ↔ x✝ ∈ (⋃ i, s i) ×ˢ ⋃ i, t 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✝) → MulOneClass (f✝ i)
α : Type u_5
β : Type u_6
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
I : Type u_7
⊢ ⇑f ∘ 1 = 1

Tactic:
ext

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.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 → α
⊢ ⇑f ∘ (x✝¹ * x✝) = ⇑f ∘ x✝¹ * ⇑f ∘ x✝

Tactic:
ext

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

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

case right
α : 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 → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
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 β
⊢ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
ext

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✝ : α × β
⊢ x✝ ∈ s₁ ×ˢ t₁ * s₂ ×ˢ t₂ ↔ x✝ ∈ (s₁ * s₂) ×ˢ (t₁ * t₂)

Tactic:
simp [mem_mul]

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 α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t

Tactic:
by
  rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
  simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j}

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ ⋃ i ∈ s, ⋃ j ∈ t, {f i j}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s → ∃ a, s = {a} ∧ IsUnit a

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ (∃ a, s = {a} ∧ IsUnit a) → IsUnit s
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x ↦ a * x) ⁻¹' {b} = {a⁻¹ * b}

Tactic:
← image_mul_left',

Goal state after:
α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x ↦ a⁻¹ * x) '' {b} = {a⁻¹ * b}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x ↦ a * x) ⁻¹' 1 = {a⁻¹}

Tactic:
← image_mul_left',

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x ↦ a⁻¹ * x) '' 1 = {a⁻¹}
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) ↔ ∃ x, x ∈ H ∧ P x

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x⁻¹) → ∃ x, x ∈ H ∧ P x

case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x, x ∈ H ∧ P x) → ∃ x, x ∈ H ∧ P x⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: N : Type u_5
inst✝ : Group N
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K

Tactic:
ext

Goal state after:
N : Type u_5
inst✝ : Group N
K : Subgroup N
x✝ : N
⊢ x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K ↔ map (↑e) K = H

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K → map (↑e) K = H

case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) K = H → map (↑e.symm) H = K
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ f.range = map f ⊤

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ f.range ↔ x✝ ∈ map f ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ comap f f.range = ⊤

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : G
⊢ x✝ ∈ comap f f.range ↔ x✝ ∈ ⊤
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker ↔ f x = f y

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker → f x = f y

case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → x / y ∈ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
⊢ H.equivMapOfInjective ↑e ⋯ = e.subgroupMap H

Tactic:
ext

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
e : G ≃* G'
x✝ : ↥H
⊢ ↑((H.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.subgroupMap H) x✝)
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y ↔ y⁻¹ * x ∈ f.ker

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → y⁻¹ * x ∈ f.ker

case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ y⁻¹ * x ∈ f.ker → f x = f y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
constructor

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ x ∈ s ⊔ t → ∃ y ∈ s, ∃ z ∈ t, y * z = x

case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor

Goal state after:
case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
constructor

Goal state after:
case mp.left
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s

case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u ↔ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

Tactic:
constructor

Goal state after:
case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u → map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

case mpr
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u → s.prod t ≤ u
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

Tactic:
constructor

Goal state after:
case mp.left
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
⊢ map (inl M N) s ≤ u

case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
⊢ map (inr M N) t ≤ u
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
⊢ domRestrict 1 M' = 1

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝ : ↥M'
⊢ (domRestrict 1 M') x✝ = 1 x✝
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝¹ x✝ : M →* A
⊢ (x✝¹ * x✝).domRestrict M' = x✝¹.domRestrict M' * x✝.domRestrict M'

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝⁶ : MulOneClass M
inst✝⁵ : MulOneClass N
inst✝⁴ : MulOneClass P
S✝ : Submonoid M
F : Type u_4
inst✝³ : FunLike F M N
mc : MonoidHomClass F M N
S : Type u_5
inst✝² : SetLike S M
inst✝¹ : SubmonoidClass S M
M' : S
A : Type u_6
inst✝ : CommMonoid A
x✝² x✝¹ : M →* A
x✝ : ↥M'
⊢ ((x✝² * x✝¹).domRestrict M') x✝ = (x✝².domRestrict M' * x✝¹.domRestrict M') x✝
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker 1 = ⊤

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
⊢ S.equivMapOfInjective ↑e ⋯ = e.submonoidMap S

Tactic:
ext

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
e : M ≃* N
x✝ : ↥S
⊢ ↑((S.equivMapOfInjective ↑e ⋯) x✝) = ↑((e.submonoidMap S) x✝)
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
ih : (m + n).bodd = (m.bodd ^^ n.bodd)
⊢ (m + (n + 1)).bodd = (m.bodd ^^ (n + 1).bodd)

Tactic:
simp [← Nat.add_assoc, ih]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
induction n
  case zero => simp
  case succ n ih => simp [← Nat.add_assoc, ih]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ (bit b n).bits = b :: n.bits

Tactic:
rw [Nat.bits, Nat.bits, binaryRec_eq]

Goal state after:
case h
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = closure {g}

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
g x✝ : G
⊢ x✝ ∈ zpowers g ↔ x✝ ∈ closure {g}
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
K : Subgroup N
⊢ H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

Tactic:
simpa only [← Subgroup.toSubmonoid_inj] using! Submonoid.prod_eq_bot_iff

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
ext

Goal state after:
G : Type u_1
inst✝ : Group G
x : G
x✝ : Additive G
⊢ x✝ ∈ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) ↔ x✝ ∈ ↑(AddSubgroup.zmultiples (Additive.ofMul x))
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: ⊢ AddSubgroup.closure {1} = ⊤

Tactic:
ext

Goal state after:
x✝ : ℤ
⊢ x✝ ∈ AddSubgroup.closure {1} ↔ x✝ ∈ ⊤
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : CommGroup G
s : Set G
⊢ normalizer s = ⊤

Tactic:
ext

Goal state after:
G : Type u_5
inst✝ : CommGroup G
s : Set G
x✝ : G
⊢ x✝ ∈ normalizer s ↔ x✝ ∈ ⊤
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : y ∈ normalizer ↑H
hx : f y ∈ map f (normalizer ↑H)
⊢ (↑(MulAut.conj (f y))).comp f = f.comp ↑(MulAut.conj y)

Tactic:
ext

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
y : G
hy : y ∈ normalizer ↑H
hx : f y ∈ map f (normalizer ↑H)
x✝ : G
⊢ ((↑(MulAut.conj (f y))).comp f) x✝ = (f.comp ↑(MulAut.conj y)) x✝
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ closure (conjugatesOfSet (s ∪ t)) = closure (conjugatesOfSet s) ⊔ closure (conjugatesOfSet t)

Tactic:
Group.conjugatesOfSet_union,

Goal state after:
G : Type u_5
inst✝ : Group G
s t : Set G
⊢ closure (conjugatesOfSet s ∪ conjugatesOfSet t) = closure (conjugatesOfSet s) ⊔ closure (conjugatesOfSet t)
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x

case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x) → (x • s ∩ t).Nonempty
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

case mpr
α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x) → (x • s ∩ t).Nonempty
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a : α
s : Set α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext

Goal state after:
α : Type u_2
inst✝ : Group α
a : α
s : Set α
x✝ : α
⊢ x✝ ∈ (a • s)⁻¹ ↔ x✝ ∈ op a⁻¹ • s⁻¹