mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ (∀ ⦃x₁ : α⦄, x₁ ∈ {a, b} → ∀ ⦃x₂ : α⦄, x₂ ∈ {a, b} → f x₁ = f x₂ → x₁ = x₂) ↔ f a = f b → a = b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ (∀ ⦃x₁ : α⦄, x₁ ∈ {a, b} → ∀ ⦃x₂ : α⦄, x₂ ∈ {a, b} → f x₁ = f x₂ → x₁ = x₂) ↔ f a = f b → a = b
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:
;

Goal state after:
ι : 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
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:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x : β
⊢ x ∈ Prod.snd '' graphOn f s ↔ x ∈ f '' s
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk
ι : 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
g : OneHom M N
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝, map_one' := map_one'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_one' := map_one'✝ } = g

Tactic:
;

Goal state after:
case mk
ι : 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
g : OneHom M N
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝, map_one' := map_one'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_one' := map_one'✝ } = g
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk.mk
ι : 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
toFun✝¹ : M → N
map_one'✝¹ : toFun✝¹ 1 = 1
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun = { toFun := toFun✝, map_one' := map_one'✝ }.toFun
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹ } = { toFun := toFun✝, map_one' := map_one'✝ }

Tactic:
;

Goal state after:
case mk.mk
ι : 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
toFun✝¹ : M → N
map_one'✝¹ : toFun✝¹ 1 = 1
toFun✝ : M → N
map_one'✝ : toFun✝ 1 = 1
h : { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun = { toFun := toFun✝, map_one' := map_one'✝ }.toFun
⊢ { toFun := toFun✝¹, map_one' := map_one'✝¹ } = { toFun := toFun✝, map_one' := map_one'✝ }
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk
ι : 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
g : M →ₙ* N
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_mul' := map_mul'✝ } = g

Tactic:
;

Goal state after:
case mk
ι : 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
g : M →ₙ* N
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_mul' := map_mul'✝ } = g
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: case mk.mk
ι : 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
toFun✝¹ : M → N
map_mul'✝¹ : ∀ (x y : M), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun = { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } = { toFun := toFun✝, map_mul' := map_mul'✝ }

Tactic:
;

Goal state after:
case mk.mk
ι : 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
toFun✝¹ : M → N
map_mul'✝¹ : ∀ (x y : M), toFun✝¹ (x * y) = toFun✝¹ x * toFun✝¹ y
toFun✝ : M → N
map_mul'✝ : ∀ (x y : M), toFun✝ (x * y) = toFun✝ x * toFun✝ y
h : { toFun := toFun✝¹, map_mul' := map_mul'✝¹ }.toFun = { toFun := toFun✝, map_mul' := map_mul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_mul' := map_mul'✝¹ } = { toFun := toFun✝, map_mul' := map_mul'✝ }
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:
;

Goal state after:
ι : 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✝
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Subsingleton β
inst✝ : Nonempty β
val✝ : Unique β
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
;

Goal state after:
case intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Subsingleton β
inst✝ : Nonempty β
val✝ : Unique β
⊢ SurjOn f s univ ↔ s.Nonempty
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✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MulHomClass F G H
f : F
hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹
g h : ι → G
x✝ : ι
⊢ (⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝
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:
;

Goal state after:
ι : 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✝
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: case refl
F : 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
inst✝¹ : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i : ι
x✝¹ x✝ : M i
__Equiv✝ : M i ≃ M i := Equiv.cast ⋯
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝

Tactic:
;

Goal state after:
case refl
F : 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
inst✝¹ : EquivLike F α β
ι : Type u_9
M : ι → Type u_10
inst✝ : (i : ι) → Mul (M i)
i : ι
x✝¹ x✝ : M i
__Equiv✝ : M i ≃ M i := Equiv.cast ⋯
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝
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:
;

Goal state after:
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✝
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:
;

Goal state after:
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✝
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:
;

Goal state after:
ι : 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✝
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' f '' s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' f '' s
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:
;

Goal state after:
ι : 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✝
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅
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✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
g : ι → G
n : ℤ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ a, a ∈ s ∧ p (f a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ a, a ∈ s ∧ p (f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ a, a ∈ s ∧ p (f a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ a, a ∈ s ∧ p (f a)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ b, b ∈ t ∧ p b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ b, b ∈ t ∧ p b
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ a < a + 1

Tactic:
;

Goal state after:
a : ℤ
⊢ a < a + 1
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a : ℤ
⊢ a - 1 < a

Tactic:
;

Goal state after:
a : ℤ
⊢ a - 1 < a
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
⊢ motive (-↑n)

Tactic:
;

Goal state after:
case negSucc
motive : ℤ → Prop
zero : motive 0
succ : ∀ (i : ℕ), motive ↑i → motive (↑i + 1)
pred : ∀ (i : ℕ), motive (-↑i) → motive (-↑i - 1)
i n : ℕ
⊢ motive (-↑n)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

pp: motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)

Tactic:
;

Goal state after:
motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ cast ?m.44 zero =
    match 0 with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n

motive : ℤ → Sort u_1
b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
⊢ motive b = (fun x ↦ motive x) (b + 0)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s

Tactic:
;

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s
Module: Mathlib.Data.Int.Init

Goal state before:
pp: 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)
hz : z ≤ b
| cast ⋯
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n)

Tactic:
;

Goal state after:
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)
hz : z ≤ b
| cast ⋯
    (match z - 1 - b with
    | ofNat n => inductionOn'.pos b zero succ n
    | -[n+1] => inductionOn'.neg b zero pred n)
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a ⋯

Tactic:
;

Goal state after:
case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a ⋯
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ ≍ f a ⋯

Tactic:
;

Goal state after:
case refl
α : Sort u
a : α
β : (a' : α) → a = a' → Sort v
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ ≍ f a ⋯
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
⊢ a = a

Tactic:
;

Goal state after:
case refl
α : Sort u
a : α
⊢ a = a
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
⊢ a = cast ⋯ a

Tactic:
;

Goal state after:
case refl
α : Sort u
a : α
⊢ a = cast ⋯ a
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: case refl
α : Sort u
a : α
⊢ cast ⋯ a = a

Tactic:
;

Goal state after:
case refl
α : Sort u
a : α
⊢ cast ⋯ a = a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s
Module: Mathlib.Algebra.Group.Hom.Basic

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DivisionCommMonoid α
x✝ : α
⊢ (invMonoidHom.comp invMonoidHom) x✝ = (MonoidHom.id α) x✝
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)

Tactic:
;

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)

Tactic:
;

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -(↑m / (↑n + 1) + 1)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) a) ∈ Subtype.val ∘ ⇑f '' t

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
s t : Set α
h : MapsTo (⇑g) s t
a : α
ha : a ∈ s
⊢ (g.extendDomain f) ((Subtype.val ∘ ⇑f) a) ∈ Subtype.val ∘ ⇑f '' t
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (⇑g₁) (⇑g₂) s
a : α
ha : a ∈ s
⊢ (g₁.extendDomain f) ((g₂.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
Module: Mathlib.Data.Set.Function

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ∧ t₁.Nonempty ∧ t₂ = ∅
⊢ False

Tactic:
;

Goal state after:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ∧ t₁.Nonempty ∧ t₂ = ∅
⊢ False
Module: Mathlib.Data.Set.Function

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ∧ t₁ = ∅ ∧ t₂.Nonempty
⊢ False

Tactic:
;

Goal state after:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ∧ t₁ = ∅ ∧ t₂.Nonempty
⊢ False
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2

Tactic:
;

Goal state after:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2
Module: Mathlib.Algebra.Group.TypeTags.Basic

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
a : M i
j : ι
⊢ single i (ofMul a) j = ofMul (mulSingle i a j)

Tactic:
by
  rcases eq_or_ne j i with rfl | h
  · simp only [mulSingle_eq_same, single_eq_same]
  · simp only [single, ne_eq, h, not_false_eq_true, Function.update_of_ne, zero_apply, mulSingle,
      one_apply, ofMul_one]

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

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1

Tactic:
;

Goal state after:
case mp
M : Type u_4
inst✝ : MulOneClass M
b : M
h : 1 * b = 1
⊢ b = 1
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1

Tactic:
;

Goal state after:
case mpr
M : Type u_4
inst✝ : MulOneClass M
a : M
h : a * 1 = 1
⊢ a = 1
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:
;

Goal state after:
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x ↦ a * x)^[0] x✝ = a ^ 0 * x✝
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:
;

Goal state after:
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x ↦ x * a)^[0] x✝ = x✝ * a ^ 0
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:
;

Goal state after:
M : Type u_4
inst✝ : Monoid M
k : ℕ
x✝ : M
⊢ (fun x ↦ x ^ k)^[0] x✝ = x✝ ^ k ^ 0
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : Monoid M
k n : ℕ
x✝ : M
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by
  rw [eq_inv_of_mul_eq_one_right h, one_div]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a = c * b

Tactic:
by rw [← h, inv_mul_cancel_right]

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 / c / b = a / b

Tactic:
;

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: G : Type u_3
inst✝ : Group G
k : ℤ
x✝ : G
⊢ (fun x ↦ x ^ k)^[0] x✝ = x✝ ^ k ^ 0

Tactic:
;

Goal state after:
G : Type u_3
inst✝ : Group G
k : ℤ
x✝ : G
⊢ (fun x ↦ x ^ k)^[0] x✝ = x✝ ^ k ^ 0
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
x✝ : G
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)

Tactic:
;

Goal state after:
G : Type u_3
inst✝ : Group G
k : ℤ
n : ℕ
x✝ : G
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
;

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ c / a * (a / b) = c / b
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }

Tactic:
;

Goal state after:
α : Type u
inst✝ : Monoid α
v i₁ : α
vi₁ : v * i₁ = 1
iv₁ : i₁ * v = 1
v' i₂ : α
vi₂ : v' * i₂ = 1
iv₂ : i₂ * v' = 1
e : v = v'
⊢ { val := v, inv := i₁, val_inv := vi₁, inv_val := iv₁ } = { val := v', inv := i₂, val_inv := vi₂, inv_val := iv₂ }