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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y) ⊓ z \ (y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))

Tactic:
sdiff_sdiff_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ z \ (y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ z \ (y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))

Tactic:
sdiff_sdiff_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) = z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x))
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z \ (x \ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)

Tactic:
sdiff_sdiff_right,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (z \ x ⊔ z ⊓ x ⊓ y) ⊓ z \ (y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x)
Module: Mathlib.Logic.Equiv.Sum

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
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
⊢ (fun a ↦ if h : a = default then none else some ⟨a, h⟩) (Option.elim' default Subtype.val none) = none

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) = x ⊔ y

Tactic:
by simp

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

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
β₁ : α → Sort u_9
β₂ : α → Sort u_10
F : (a : α) → β₁ a ≃ β₂ a
H : (a : α) → β₁ a
⊢ ∀ (x : α), Pi.map (fun a ↦ ⇑(F a).symm) (Pi.map (fun a ↦ ⇑(F a)) H) x = H x

Tactic:
by simp

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

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
β₁ : α → Sort u_9
β₂ : α → Sort u_10
F : (a : α) → β₁ a ≃ β₂ a
H : (a : α) → β₂ a
⊢ ∀ (x : α), Pi.map (fun a ↦ ⇑(F a)) (Pi.map (fun a ↦ ⇑(F a).symm) H) x = H x

Tactic:
by simp

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

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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
a : { a // p a }
⊢ ↑((fun b ↦ ⟨e.symm ↑b, ⋯⟩) ((fun a ↦ ⟨e ↑a, ⋯⟩) a)) = ↑a

Tactic:
by simp

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

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
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
b : { b // q b }
⊢ ↑((fun a ↦ ⟨e ↑a, ⋯⟩) ((fun b ↦ ⟨e.symm ↑b, ⋯⟩) b)) = ↑b

Tactic:
by simp

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

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
p : β → Prop
e : α ≃ β
⊢ ∀ (a : α), p (e a) ↔ p (e a)

Tactic:
by simp

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

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_9
x✝ : { f // ∀ (i : ι), (f i).fst = i }
f : ι → (i : ι) × π i
hf : ∀ (i : ι), (f i).fst = i
i : ι
⊢ (↑((fun f ↦ ⟨fun i ↦ ⟨i, f i⟩, ⋯⟩) ((fun f i ↦ ⋯.mpr (↑f i).snd) ⟨f, hf⟩)) i).snd ≍ (↑⟨f, hf⟩ i).snd

Tactic:
by simp

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

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_9
β : α → Type u_10
a : α
b : β a
⊢ (fun x ↦
        match x with
        | ⟨⟨fst, b⟩, h⟩ => h ▸ b)
      ((fun b ↦ ⟨⟨a, b⟩, ⋯⟩) b) =
    b

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b

Tactic:
by
  refine le_antisymm (sup_le symmDiff_le_sup inf_le_sup) ?_
  rw [sup_inf_left, symmDiff]
  refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)
  · rw [sup_right_comm]
    exact le_sup_of_le_left le_sdiff_sup
  · rw [sup_assoc]
    exact le_sup_of_le_right le_sdiff_sup

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:
by 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:
by 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:
by simp

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

Goal state before:
pp: α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ

Tactic:
ext ⟨x, x_in_s⟩

Goal state after:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u ↔ ⟨x, x_in_s⟩ ∈ (Subtype.val ⁻¹' v)ᶜ
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:
by 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:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Tactic:
by
  refine (range_extend_subset _ _ _).antisymm ?_
  rintro z (⟨x, rfl⟩ | ⟨y, hy, rfl⟩)
  exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]

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

Goal state before:
pp: case succ
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : ↑s
k : ℕ
ih : ↑((restrict f s s h)^[k] x) = f^[k] ↑x
⊢ ↑((restrict f s s h)^[k + 1] x) = f^[k + 1] ↑x

Tactic:
| succ k ih =>

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

Goal state before:
pp: case inr.refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact prod_mono H.1 H.2

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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case mp
X : Type u_1
Y : Sort u_2
f : X → Y
s : Set X
x : X
hx : x ∈ s
⊢ toPullbackDiag f x ∈ pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Tactic:
exact ⟨rfl, hx, hx⟩

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ ∀ ⦃a₂ : Set α⦄, f '' s = f '' a₂ → s = a₂

Tactic:
t

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s = f '' t → s = t
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:
by 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:
by simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s.pi t₁ ⊆ s.pi t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ s.pi t₁ = ∅

Tactic:
refine
    ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
  rw [← Ne, ← nonempty_iff_ne_empty]
  intro hne i hi
  simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
    image_mono (f := fun f : ∀ i, α i => f i) h

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:
by 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✝³ : One M
inst✝² : One N
inst✝¹ : FunLike F M N
inst✝ : OneHomClass F M N
f : F
⊢ ⇑f ∘ 1 = 1

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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 \ {f a} = t
x : α
hx : x ∈ s
⊢ a ∈ insert a s

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
⊢ (k : ℤ) → k < _n + 1 → motive k

Tactic:
l

Goal state after:
case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
l : ℤ
⊢ l < _n + 1 → motive l
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ f '' s ∪ (f '' s₁ ∩ t') \ t ⊆ t'

Tactic:
h.image_eq,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ∪ (f '' s₁ ∩ t') \ t ⊆ t'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'

Tactic:
exact ⟨htt', sdiff_subset.trans inter_subset_right⟩

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

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s

Tactic:
exact ⟨x, hxs, hxy⟩

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' s ∪ f '' r

Tactic:
h.image_eq,

Goal state after:
case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' r
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)

Tactic:
exact h.bijOn_image ha.bijOn_univ hf.injOn

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a * a ^ (n - 1) = a ^ n

Tactic:
← pow_succ',

Goal state after:
M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ (n - 1 + 1) = a ^ n
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:
by 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:
by 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:
by 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:
by simp

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : IsRightCancelMul M
a b : M
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

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:
by 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:
by 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:
by 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:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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:
by 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 / (b * c)

Tactic:
by 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 / (b / c)

Tactic:
by simp

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

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

Tactic:
by 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:
by 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 / b / c

Tactic:
by 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:
by simp

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

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

Tactic:
by 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:
by simp

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

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

Tactic:
by 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 / b * (1 / c)

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / c / (b / c) = a / b

Tactic:
← inv_div c b,

Goal state after:
G : Type u_3
inst✝ : Group G
a b c : G
⊢ a / c / (c / b)⁻¹ = a / b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (g * a)
h_inv : ∀ (a : G), P a → P (g⁻¹ * a)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g⁻¹ * g ^ (-↑n))

Tactic:
exact h_inv _ ih

Goal state after: