mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
inst✝ : Nonempty α
g : β → γ
h : Surjective fun x ↦ g ∘ x
c : γ
a : α
f : α → β
hf : (fun x ↦ g ∘ x) f = fun x ↦ c
⊢ ∃ a, g a = c

Tactic:
exact ⟨f a, congr_fun hf _⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r✝ : α → β → Prop
f✝ : α → γ
g : β → δ
c : γ
d : δ
r : α → α → Prop
inst✝ : Std.Symm r
f : α → β
x y : α
hxy : r x y
⊢ Relation.Map r f f (f y) (f x)

Tactic:
exact ⟨y, x, symm hxy, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j

Tactic:
rw [← update_inr_comp_inr, Function.comp_apply]

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivisionMonoid (f i)
a✝ b✝ : (i : I) → f i
h : a✝ * b✝ = 1
x✝ : I
⊢ a✝⁻¹ x✝ = b✝ x✝

Tactic:
exact DivisionMonoid.inv_eq_of_mul _ _ (congrFun h _)

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap < (b, a) ↔ x < (a, b)

Tactic:
← swap_lt_swap

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap.swap < (b, a).swap ↔ x < (a, b)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x

Tactic:
by
  rintro rfl
  exact (hf.reflect_lt h1).not_ge (Int.le_of_lt_add_one <| hf.reflect_lt h2)

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬Nonempty ↑s ↔ s = ∅

Tactic:
rw [nonempty_subtype, not_exists, eq_empty_iff_forall_notMem]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ (b ⊔ c) = b ⊔ (c ⊔ a)

Tactic:
by
  rw [sup_comm, sup_assoc]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ x ⊔ y ≤ c ↔ x ⊔ y ≤ c

Tactic:
simp only [sup_le_iff]; rw [← H, @sup_le_iff α A, H, H]

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

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ Disjoint (insert a s) t ↔ ¬a ∈ t ∧ Disjoint s t

Tactic:
simp only [Set.disjoint_left, Set.mem_insert_iff, forall_eq_or_imp]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ⊔ c = c

Tactic:
sup_of_le_right hbc

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ c = c
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s \ t = tᶜ ∩ s

Tactic:
by rw [sdiff_eq, inter_comm]

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

Goal state before:
pp: α : Type u_1
s t u : Set α
⊢ (s ∩ t) \ u = s \ u ∩ t

Tactic:
by
  rw [sdiff_eq, sdiff_eq, inter_right_comm]

Goal state after:
Module: Mathlib.Data.Sigma.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_4
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
⊢ a = b ∧ f ≍ g

Tactic:
rcases ‹Nonempty γ› with ⟨i⟩
  obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)
  simpa [funext_iff] using h

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

Goal state before:
pp: ι : Type u_1
β : ι → Type u_3
inst✝ : DecidableEq ι
x : (i : ι) → β i
i : ι
s : Set (β i)
⊢ update x i '' s = univ.pi (update (fun j ↦ {x j}) i s)

Tactic:
ext y
  simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
    mem_univ, true_implies]
  rw [forall_update_iff (p := fun x s => y x ∈ s)]
  simp [eq_comm]

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:
rw [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.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
x✝ : ∃ f t, s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
rw [hs, image_fst_graphOn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t

Tactic:
rwa [SurjOn, ← H.image_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
intro y hy
  rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩
  rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩
  obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm
  exact mem_image_of_mem f ⟨hx₁, hx₂⟩

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

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

Tactic:
cases i with

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✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f (x * y) = f x * (f (1 * 1⁻¹ * y⁻¹))⁻¹

Tactic:
{ simp only [one_mul, inv_one, ← map_div, inv_inv] }

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)
⊢ InjOn f (s ∪ r)

Tactic:
rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
    · refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
      rw [← h.image_eq]
      exact ⟨x, hxs, hxy⟩
    exact (subset_sdiff.1 hrss).2.symm.mono_left h.mapsTo

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 ^ (n - 1 + 1) = a ^ n

Tactic:
Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn

Goal state after:
M : Type u_4
inst✝ : Monoid M
n : ℕ
hn : n ≠ 0
a : M
⊢ a ^ n = a ^ n
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by rw [mul_eq_one_iff_eq_inv, inv_inv]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a ↦ a / b

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a ↦ a * b⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a ↦ b / a

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
G : Type u_3
inst✝ : Group G
b : G
⊢ Injective fun a ↦ b * a⁻¹
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a * c⁻¹ = b * c⁻¹ ↔ a = b
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : IsMulCommutative M
inst✝ : IsMulCommutative N
x✝¹ x✝ : M × N
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by ext <;> apply mul_comm'

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

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)

Tactic:
rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_3
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ : M₀
Hne : a✝ ≠ 0
x✝¹ x✝ : M₀
He : (fun x ↦ a✝ * x) x✝¹ = (fun x ↦ a✝ * x) x✝
this : f a✝ * f x✝¹ = f a✝ * f x✝
⊢ x✝¹ = x✝

Tactic:
exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)

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

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
n : ℕ
inst✝ : Nontrivial M₀
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
by
  rw [zero_pow_eq, one_ne_zero.ite_eq_left_iff]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ y = z

Tactic:
by
    dsimp only at h; rw [← inv_mul_cancel_left₀ hx y, h, inv_mul_cancel_left₀ hx z]

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

Goal state before:
pp: m n : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
⊢ ∀ (hn : m ≤ n), Int.strongRec lt ge n = ge n hn fun k x ↦ Int.strongRec lt ge k

Tactic:
refine m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n

Goal state after:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ Int.strongRec lt ge n = ge n hn fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r s : R
x✝ : M
inst✝¹ : AddCommMonoid M₂
inst✝ : SMul R M₂
f : M →+ M₂
hf : Surjective ⇑f
smul : ∀ (c : R) (x : M), f (c • x) = c • f x
x : M₂
⊢ 0 • x = 0

Tactic:
by
      rcases hf x with ⟨x, rfl⟩
      rw [← f.map_zero, ← smul, zero_smul]

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Defs

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
m : ℤ
x✝ : ℕ
ih : ∀ (n : ℤ), ↑(↑x✝ * n) = ↑x✝ • ↑n
⊢ ∀ (n : ℤ), ↑((↑x✝ + 1) * n) = (↑x✝ + 1) • ↑n

Tactic:
by simp [add_mul, add_zsmul, ih]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : IsUnit a
hb : ¬IsUnit b
⊢ ¬IsUnit (a * b)

Tactic:
simpa [ha.mul_left_iff]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inr.inl
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a b : M₀
h : IsUnit a ∨ IsUnit b
ha : ¬IsUnit a
hb : IsUnit b
this : ¬IsUnit (a * b)
⊢ (a * b)⁻¹ʳ = b⁻¹ʳ * a⁻¹ʳ

Tactic:
simp [Ring.inverse_non_unit, ha, this]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : AddMonoidWithOne α
⊢ 2 = 1 + 1

Tactic:
by rw [one_add_one_eq_two]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
⊢ ∃ b, b * b ≤ a

Tactic:
by_cases! h : a < 1

Goal state after:
case pos
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ ∃ b, b * b ≤ a

case neg
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : 1 ≤ a
⊢ ∃ b, b * b ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * d
⊢ b ≤ a

pp: case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ a

Tactic:
· exact le_of_mul_le_mul_of_pos_right h <| hc.trans_le hcd

Goal state after:
case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ a * c ≤ b

Tactic:
le_mul_inv_iff₀ hc

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c ≤ b ↔ a * c ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ a * c

Tactic:
by
  rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a ≤ b * c⁻¹
hc : 0 < c
⊢ a * c ≤ b

Tactic:
le_mul_inv_iff₀ hc

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a * c ≤ b
hc : 0 < c
⊢ a * c ≤ b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
a b : α₁ ⊕ α₂
⊢ Sum.Lex s₁ s₂ ((e₁.sumCongr e₂.toEquiv) a) ((e₁.sumCongr e₂.toEquiv) b) ↔ Sum.Lex r₁ r₂ a b

Tactic:
by
    obtain ⟨f, hf⟩ := e₁; obtain ⟨g, hg⟩ := e₂; cases a <;> cases b <;> simp [hf, hg]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
⊢ -(a + b) = -b + -a

Tactic:
obtain rfl | ha := eq_or_ne a ⊤
    · simp
    obtain rfl | hb := eq_or_ne b ⊤
    · simp
    · exact left_neg_eq_right_neg (a := a + b) (by simp [neg_add_cancel_of_ne_top, *])
        (by simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *])

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x : β
⊢ e.symm ↑x ≠ 0

Tactic:
by simp [e.symm_apply_eq]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
w x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < w
⊢ x + w ≤ z + w

Tactic:
cases w

Goal state after:
case top
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < ⊤
⊢ x + ⊤ ≤ z + ⊤

case coe
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
a✝ : α
yw : y < ↑a✝
⊢ x + ↑a✝ ≤ z + ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ IsAddLeftRegular ↑a

Tactic:
rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]

Goal state after:
case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
b c : α
⊢ a + b = a + c → b = c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ IsAddRightRegular ↑a

Tactic:
rintro (_ | b) (_ | c) <;> simp [none_eq_bot, some_eq_coe, ← coe_add]

Goal state after:
case some.some
α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
b c : α
⊢ b + a = c + a → b = c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝³ : Add α
x : WithBot α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
⊢ AddLECancellable x → x ≠ ⊥

Tactic:
rintro h rfl; exact (bot_lt_coe <| Classical.arbitrary _).not_ge <| h <| by simp

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case right.left
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < x

Tactic:
exact lt_of_lt_of_le hlt ‹z' ≤ _›

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case right.right
α : Type u_1
inst✝¹ : LinearOrder α
x y : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
hy : y ≠ 0
z' : WithZero α
hnz' : z' ≠ 0
hzx : z' ≤ x
hzy : z' ≤ y
z : WithZero α
hnz : z ≠ 0
hlt : z < z'
⊢ z < y

Tactic:
exact lt_of_lt_of_le hlt ‹z' ≤ _›

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

Goal state before:
pp: α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : MulOneClass S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r * f r = 1

Tactic:
rw [← map_mul, invOf_mul_self, map_one]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ⊥

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.toDual ⊥ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ⊥

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.top
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ ⊤ ↔ WithTop.ofDual ⊤ ≤ ↑a✝

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : α
a✝ : αᵒᵈ
⊢ WithBot.toDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.ofDual ↑a✝ ≤ ↑a✝¹

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.top
α : Type u_1
inst✝ : LE α
⊢ WithBot.ofDual ⊥ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ⊥

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.ofDual ⊥ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ⊥

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.top
α : Type u_1
inst✝ : LE α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ ≤ ⊤ ↔ WithTop.toDual ⊤ ≤ ↑a✝

Tactic:
simp [toDual_le]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ : αᵒᵈ
a✝ : α
⊢ WithBot.ofDual ↑a✝¹ ≤ ↑a✝ ↔ WithTop.toDual ↑a✝ ≤ ↑a✝¹

Tactic:
simp [toDual_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ image2 f (s ∪ s') t = image2 f s t ∪ image2 f s' t

Tactic:
simp_rw [← image_prod, union_prod, image_union]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|

Tactic:
exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |a| = a
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
simp only [h, neg_dvd]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : Ring α
inst✝ : LinearOrder α
a b : α
h : |a| = -a
⊢ |a| ∣ b ↔ a ∣ b

Tactic:
simp only [h, neg_dvd]

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑s ⊕ ↑(t \ s ∪ s ∩ t) ≃ ↑s ⊕ ↑t

Tactic:
{ rw [(_ : t \ s ∪ s ∩ t = t)]
        rw [union_comm, inter_comm, inter_union_sdiff] }

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
k : α
n : ℤ
x a a' : α
h : k + a = a'
⊢ k + termg n x a = termg n x a'

Tactic:
by
  simp [h.symm, termg, add_comm, add_assoc]

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
rw [h₁, h₂, Nat.cast_commute]

Goal state after:
case eq
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * db + nb * da = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
rw [h₁, h₂, Nat.cast_commute]

Goal state after:
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case nil
α : Type u
i j : ℕ
⊢ (dropSlice i j []).length = [].length - min j ([].length - i)

Tactic:
cases i with

Goal state after:
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i j : ℕ), (dropSlice i j tail✝).length = tail✝.length - min j (tail✝.length - i)
i j : ℕ
⊢ (dropSlice i j (head✝ :: tail✝)).length = (head✝ :: tail✝).length - min j ((head✝ :: tail✝).length - i)

Tactic:
cases i with

Goal state after: