mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝⁹ : Max α
inst✝⁸ : Min α
inst✝⁷ : LE α
inst✝⁶ : LT α
inst✝⁵ : Top α
inst✝⁴ : Bot α
inst✝³ : Compl α
inst✝² : SDiff α
inst✝¹ : HImp α
inst✝ : BooleanAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a b : α
⊢ f a ⊓ (f b)ᶜ = f (a ⊓ bᶜ)

Tactic:
rw [map_inf, map_compl]

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type ?u.23
α₂ : Type ?u.25
β₁ : Type ?u.22
β₂ : Type ?u.24
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
x✝ : α₁ × β₁
a : α₁
b : β₁
⊢ Prod.map (⇑e₁.symm) (⇑e₂.symm) (Prod.map ⇑e₁ ⇑e₂ (a, b)) = (a, b)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α : Sort u_1
α₁✝ : Sort u_2
α₂✝ : Sort u_3
β : Sort u_4
β₁✝ : Sort u_5
β₂✝ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α₁ : Type ?u.23
α₂ : Type ?u.25
β₁ : Type ?u.22
β₂ : Type ?u.24
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
x✝ : α₂ × β₂
a : α₂
b : β₂
⊢ Prod.map (⇑e₁) (⇑e₂) (Prod.map ⇑e₁.symm ⇑e₂.symm (a, b)) = (a, b)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ ((prodCongrLeft e).trans (prodComm β₂ α₁)) (a, b) = ((prodComm β₁ α₁).trans (prodCongrRight e)) (a, b)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Prod

Goal state before:
pp: α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)) ⟨a, b⟩ = ((sigmaEquivProd α₁ β₁).trans (prodCongrRight e)) ⟨a, b⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: α₁ : Type u_11
β₁ : Type u_12
e : α₁ ≃ β₁
f : α₁ → α₁
x : α₁
⊢ e (f x) = e.conj f (e x)

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
f : α → α
⊢ preimage f^[0] = (preimage f)^[0]

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {True} ↔ x✝ ∈ {a | p a}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {False} ↔ x✝ ∈ {a | ¬p a}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∃ y, y ∈ f '' s ∧ p y) ↔ ∃ x, x ∈ s ∧ p (f x)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
x✝¹ : Set α
x✝ : α
⊢ x✝ ∈ id '' x✝¹ ↔ x✝ ∈ id x✝¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ (fun x ↦ x) '' s ↔ x✝ ∈ s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ id '' s = s

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
f : α → α
⊢ image f^[0] = (image f)^[0]

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
c : α
d : β
⊢ (c, d) ∈ {a} ×ˢ {b} ↔ (c, d) ∈ {(a, b)}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) = t

Tactic:
rwa [image_preimage_inter, inter_eq_left]

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

Goal state before:
pp: case zero
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
⊢ ↑((restrict f s s h)^[0] x) = f^[0] ↑x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
x✝ : α
⊢ x✝ ∈ Subtype.val '' t.restrictPreimage f ⁻¹' u ↔ x✝ ∈ f ⁻¹' Subtype.val '' u

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∀ (a : α), a ∈ range f → p a) ↔ ∀ (i : ι), p (f i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i)

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
i : α
h : i = j
⊢ (if j = j ∨ j ∈ s then f j else g j) = update (fun i ↦ if i ∈ s then f i else g i) j (f j) j

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g x = update g x (f x) x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Tactic:
simp only [EqOn, ← forall_and]
  refine forall_congr' fun a => ?_; by_cases a ∈ s <;> simp [*]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inl ↔ Sum.inl val✝ ∈ {x | x.isLeft = true}

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inl ↔ Sum.inr val✝ ∈ {x | x.isLeft = true}

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inr ↔ Sum.inl val✝ ∈ {x | x.isRight = true}

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inr ↔ Sum.inr val✝ ∈ {x | x.isRight = true}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl ⊓ range Sum.inr ⊆ ⊥

Tactic:
by
      rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
      exact Sum.noConfusion rfl rfl (heq_of_eq h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set β
x✝ : α
⊢ x✝ ∈ Sum.inl ⁻¹' Sum.inr '' s ↔ x✝ ∈ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' Sum.inl '' s ↔ x✝ ∈ ∅

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : α
⊢ Sum.inl val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val✝ : β
⊢ Sum.inr val✝ ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val✝ ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ range (inclusion h) ↔ ⟨x, hx⟩ ∈ {x | ↑x ∈ s}

Tactic:
simp

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

Goal state before:
pp: ι : Type u_8
α : ι → Type u_9
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t fun x ↦ univ) = s.pi t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ∅.offDiag = ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
a : α
⊢ {a}.offDiag = ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (x : α × α), x ∈ univ.offDiag ↔ x ∈ (diagonal α)ᶜ

Tactic:
simp

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

Goal state before:
pp: case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (range fun x ↦ (some x).elim b f) = range f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u : Set α
v : Set β
⊢ ∀ (b : α), b ∈ u → ∀ (c : β), c ∈ v → Sum.inl b ≠ Sum.inr c

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
t : (i : ι) → Set (α i)
⊢ ∀ (i : ι), ¬i ∈ univ → Surjective (f i)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x✝ : (x : ι) → α x
⊢ x✝ ∈ eval i ⁻¹' s ↔ x✝ ∈ {i}.pi (update (fun x ↦ univ) i s)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' s.pi t
⊢ x = update f i x i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ (InjOn f s ∧ InjOn f {a} ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ {a} → f x ≠ f y) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
x✝ : (b : ι) → α b
⊢ (x✝ ∈ ⇑(piCongrLeft α f).symm ⁻¹' s.pi fun i' ↦ t (f i')) ↔ x✝ ∈ (⇑f '' s).pi t

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (a : (b : ι) → α b),
    (piCongrLeft α f).symm a ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ (piCongrLeft α f).symm a ∈ s.pi fun i ↦ t (f i)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
π : ι ⊕ ι' → Type u_4
t : (i : ι ⊕ ι') → Set (π i)
x✝ : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))
⊢ x✝ ∈ ⇑(sumPiEquivProdPi π).symm ⁻¹' univ.pi t ↔ x✝ ∈ (univ.pi fun i ↦ t (Sum.inl i)) ×ˢ univ.pi fun i ↦ t (Sum.inr i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁

Tactic:
h.image_subset_image_iff h₁ h₂,

Goal state after:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ s₁ ⊆ s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : β
⊢ x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : α → β
⊢ graphOn f univ = graphOn g univ ↔ f = g

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst s

Tactic:
hf

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst (graphOn f (Prod.fst '' s))
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : One M
inst✝² : One N
inst✝¹ : FunLike F M N
inst✝ : OneHomClass F M N
f : F
⊢ ⇑f ∘ 1 = 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
x✝ : ι
⊢ (⇑f ∘ (g * h)) x✝ = (⇑f ∘ g * ⇑f ∘ h) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
x✝ : ι
⊢ (⇑f ∘ g⁻¹) x✝ = (⇑f ∘ g)⁻¹ x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : N
⊢ ((↑e).comp ↑e.symm) x✝ = (MonoidHom.id N) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
⊢ ⇑f ∘ (g * h⁻¹) = ⇑f ∘ g * (⇑f ∘ h)⁻¹

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
e : M ≃* N
x✝ : M
⊢ ((↑e.symm).comp ↑e) x✝ = (MonoidHom.id M) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℤ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
hnp : OneHom N P
hmn : OneHom M N
⊢ hnp (hmn 1) = 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
hnp : N →ₙ* P
hmn : M →ₙ* N
x y : M
⊢ hnp (hmn (x * y)) = hnp (hmn x) * hnp (hmn y)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
hnp : N →* P
hmn : M →* N
⊢ hnp (hmn 1) = 1

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
hnp : N →* P
hmn : M →* N
⊢ ∀ (x y : M), hnp (hmn (x * y)) = hnp (hmn x) * hnp (hmn y)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ BijOn f s t

Tactic:
exact ⟨by simp [← this, mapsTo_iff_image_subset], h.injOn.mono (subset_insert ..),
        by simp [← this, surjOn_image]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ a ∈ insert a s

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : DivisionMonoid β
f : α →* β
g h : α
⊢ f (g * h⁻¹) = f g * (f h)⁻¹

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b✝ c d m n : ℤ
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = motive (b + ↑0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
x✝ : α
⊢ (invMonoidHom.comp invMonoidHom) x✝ = (MonoidHom.id α) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : One M
inst✝ : MulOneClass N
f g : OneHom M N
⊢ f 1 * g 1 = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : One M
inst✝ : InvOneClass N
f : OneHom M N
⊢ (f 1)⁻¹ = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : One M
inst✝ : DivisionMonoid N
f g : OneHom M N
⊢ f 1 / g 1 = 1

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : Mul M
inst✝¹ : CommSemigroup N
inst✝ : CommSemigroup P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f g : M →* N
⊢ f 1 * g 1 = 1

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
N : Type u_3
P : Type u_4
inst✝² : MulOneClass M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid P
g : N →* P
f₁ f₂ : M →* N
x✝ : M
⊢ (g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
φ : G →* H
ψ : M →* G
x✝ : M
⊢ (φ.comp ψ⁻¹) x✝ = (φ.comp ψ)⁻¹ x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
G : Type u_5
H : Type u_6
inst✝² : MulOneClass M
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : G →* H
g h : M →* G
x✝ : M
⊢ (f.comp (g / h)) x✝ = (f.comp g / f.comp h) x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
x✝ : a * b = 1
⊢ a ^ 0 * b ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x ↦ a * x)^[0] x✝ = a ^ 0 * x✝

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x ↦ x * a)^[0] x✝ = x✝ * a ^ 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a b : M
⊢ (fun x ↦ a * x)^[n] b = a ^ n * b

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a b : M
⊢ (fun x ↦ x * a)^[n] b = b * a ^ n

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x ↦ a * x)^[n] 1 = a ^ n

Tactic:
simp

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k : ℕ
x✝ : M
⊢ (fun x ↦ x ^ k)^[0] x✝ = x✝ ^ k ^ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ 1 / a * (1 / b) = 1 / (b * a)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ a⁻¹ / b = (b * a)⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ (a / b)⁻¹ = b / a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ 1 / (a / b) = b / a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ 1 / (1 / a) = a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ a ^ (-0) = (a ^ 0)⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop (op (unop x✝ ^ ↑x✝¹) * x✝)

Tactic:
unop_mul,

Goal state after:
α : Type u_1
inst✝ : DivInvMonoid α
x✝¹ : ℕ
x✝ : αᵐᵒᵖ
⊢ unop x✝ * unop x✝ ^ x✝¹ = unop x✝ * unop (op (unop x✝ ^ ↑x✝¹))
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b c : α
⊢ a / (b / c) = a * c / b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ a / b⁻¹ = a * b

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a / b)⁻¹ = a⁻¹ / b⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a / b = b⁻¹ * a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a⁻¹ * b = b / a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a⁻¹ / b = b⁻¹ / a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a * b)⁻¹ = a⁻¹ / b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a⁻¹ / b⁻¹ = b / a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ (a⁻¹ / b⁻¹)⁻¹ = a / b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ 1 / a * (1 / b) = 1 / (a * b)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a / b / c = a / c / b

Tactic:
simp

Goal state after: