mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Refl r
a : α
⊢ Decidable.decide (r a a) = true

Tactic:
simpa using refl a

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u
e : β = α
a : α
b : β
h : a ≍ b
⊢ a = cast e b

Tactic:
cases h; rfl

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u
inst✝¹ : Subsingleton α
inst✝ : Nonempty α
⊢ Nonempty (Unique α)

Tactic:
by
  inhabit α
  exact ⟨Unique.mk' α⟩

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

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f g : F
h : f = g
⊢ ⇑f = ⇑g

Tactic:
cases h; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N α
f : α → β
hf : Surjective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ c₁ • c₂ • f x = c₂ • c₁ • f x

Tactic:
simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : DivInvMonoid β
inst✝¹ : SMul α β
inst✝ : IsScalarTower α β β
r : α
x y : β
⊢ r • x / y = r • (x / y)

Tactic:
simp [div_eq_mul_inv, smul_mul_assoc]

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

Goal state before:
pp: α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
⊢ rec f g x = cast ⋯ (rec f g y)

Tactic:
cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (inl c)
⊢ x.isLeft = true

Tactic:
cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (inl a) y
⊢ y.isLeft = true

Tactic:
cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (inr d)
⊢ x.isRight = true

Tactic:
cases h; rfl

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (inr b) y
⊢ y.isRight = true

Tactic:
cases h; rfl

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

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ (x₁ • y) • z = x₁ • y • z

Tactic:
rw [smul_eq_mul, mul_comm, ← smul_eq_mul, ← smul_comm, smul_eq_mul,
    mul_comm, ← smul_eq_mul]

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

Goal state before:
pp: b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ b₀.toNat ≤ b₁.toNat

Tactic:
cases b₀ <;> cases b₁ <;> simp_all +decide

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

Goal state before:
pp: case inr
n m : ℕ
h : m < n
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
rcases eq_or_ne m 0 with rfl | hm
    · simp
    · simp only [hm, h.not_ge, or_self, iff_false]
      refine not_dvd_of_pos_of_lt ?_ ?_ <;>
      grind

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

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
⊢ P x

Tactic:
have := al (x - lo) ((Nat.sub_lt_sub_iff_right hl).2 hh)

Goal state after:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P (lo + (x - lo))
⊢ P x
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
o : Ordering
⊢ o.swap.Compares a b ↔ o.Compares b a

Tactic:
by
  cases o
  · exact Iff.rfl
  · exact eq_comm
  · exact Iff.rfl

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hexists : ∃ M, P M
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
⊢ P ⊤

Tactic:
contrapose! hexists

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
hexists : ¬P ⊤
⊢ ∀ (M : α), ¬P M
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
x✝ : Std.Irrefl r
⊢ ∀ (a b : α), r a b = ⊥ a b

Tactic:
by simp [not_rel_of_subsingleton]

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

Goal state before:
pp: case zero
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n + 0 ≤ f (n + 0)

Tactic:
rw [Nat.add_zero, Nat.add_zero]

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

Goal state before:
pp: α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← subsingleton_iff_singleton ha]

Goal state after:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
⊢ t.ite s₁ s₂ = s₁ ∪ s₂ \ t

Tactic:
by
  ext x
  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_right_of_imp (@h x)]

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

Goal state before:
pp: case inl
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
jb : β ia
⊢ update f ⟨ia, ib⟩ x ⟨ia, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ia jb

pp: case inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb

Tactic:
· simp
    grind

Goal state after:
case inr
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ i.fst i.snd
ia : α
ib : β ia
x : γ ⟨ia, ib⟩.fst ⟨ia, ib⟩.snd
ja : α
jb : β ja
ha : ia ≠ ja
⊢ update f ⟨ia, ib⟩ x ⟨ja, jb⟩ =
    update (fun x y ↦ f ⟨x, y⟩) ⟨ia, ib⟩.fst (update (fun y ↦ f ⟨⟨ia, ib⟩.fst, y⟩) ⟨ia, ib⟩.snd x) ja jb
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [sup_inf_left, symmDiff]

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
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
inst✝¹ : DecidableEq α✝
α : Type u_9
inst✝ : Nontrivial α
⊢ Nontrivial (Perm α)

Tactic:
by
  classical
  obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
  exact Function.Injective.nontrivial (Equiv.swap_injective_of_left a)

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

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

Tactic:
ext ⟨a, b⟩ : 1

Goal state after:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : β₁
b : α₁
⊢ ((prodCongrLeft e).trans (prodComm β₂ α₁)) (a, b) = ((prodComm β₁ α₁).trans (prodCongrRight e)) (a, b)
Module: Mathlib.Logic.Equiv.Basic

Goal state before:
pp: case mp.inl
α : Type u_9
inst✝ : DecidableEq α
s : Set α
j : α
hj : ¬j ∈ s
a : α
ha hi : a ∈ s
⊢ (swap a j) a ∈ insert j s \ {a}

pp: case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ (swap i j) a ∈ insert j s \ {i}

Tactic:
· rw [swap_apply_left]; exact ⟨.inl rfl, (ne_of_mem_of_not_mem hi hj).symm⟩

Goal state after:
case mp.inr
α : Type u_9
inst✝ : DecidableEq α
s : Set α
i j : α
hi : i ∈ s
hj : ¬j ∈ s
a : α
ha : a ∈ s
ne : a ≠ i
⊢ (swap i j) a ∈ insert j s \ {i}
Module: Mathlib.Logic.Equiv.Prod

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

Tactic:
ext ⟨a, b⟩ : 1

Goal state after:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((prodCongrRight e).trans (prodComm α₁ β₂)) (a, b) = ((prodComm α₁ β₁).trans (prodCongrLeft e)) (a, b)
Module: Mathlib.Logic.Equiv.Prod

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

Tactic:
ext ⟨a, b⟩ : 1

Goal state after:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaCongrRight e).trans (sigmaEquivProd α₁ β₂)) ⟨a, b⟩ = ((sigmaEquivProd α₁ β₁).trans (prodCongrRight e)) ⟨a, b⟩
Module: Mathlib.Logic.Equiv.Prod

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

Tactic:
ext ⟨a, b⟩ : 1

Goal state after:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : α₁ → β₁ ≃ β₂
a : α₁
b : β₁
⊢ ((sigmaEquivProd α₁ β₁).symm.trans (sigmaCongrRight e)) (a, b) =
    ((prodCongrRight e).trans (sigmaEquivProd α₁ β₂).symm) (a, b)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ b ⇔ a ⇔ a = b

Tactic:
by simp [bihimp_assoc]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_10
e : α ≃ β
f : (a : α) → P a
b : β
x : P (e.symm b)
b' : β
⊢ (Equiv.piCongrLeft' P e) (update f (e.symm b) x) b' = update ((Equiv.piCongrLeft' P e) f) b x b'

Tactic:
rcases eq_or_ne b' b with (rfl | h) <;> simp_all

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
y : β
⊢ y ∈ f '' s ∪ g '' sᶜ → y ∈ range (s.piecewise f g)

Tactic:
rintro (⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩) <;> use x <;> simp_all

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ x ∈ (s ∪ t).offDiag ↔ x ∈ s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Tactic:
simp only [mem_offDiag, mem_union, ne_eq, mem_prod]

Goal state after:
α : Type u_1
s t : Set α
h : Disjoint s t
x : α × α
⊢ (x.1 ∈ s ∨ x.1 ∈ t) ∧ (x.2 ∈ s ∨ x.2 ∈ t) ∧ ¬x.1 = x.2 ↔
    ((x.1 ∈ s ∧ x.2 ∈ s ∧ ¬x.1 = x.2 ∨ x.1 ∈ t ∧ x.2 ∈ t ∧ ¬x.1 = x.2) ∨ x.1 ∈ s ∧ x.2 ∈ t) ∨ x.1 ∈ t ∧ x.2 ∈ s
Module: Mathlib.Algebra.Group.Equiv.Defs

Goal state before:
pp: 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 j : ι
h : i = j
x✝¹ x✝ : M i
⊢ (Equiv.cast ⋯).toFun (x✝¹ * x✝) = (Equiv.cast ⋯).toFun x✝¹ * (Equiv.cast ⋯).toFun x✝

Tactic:
cases h; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ BijOn f (s \ {a}) (t \ {f a})

Tactic:
convert! h₁.subset_left sdiff_subset

Goal state after:
case e'_5
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ t \ {f a} = f '' (s \ {a})
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ (fun x ↦ f' (f x)) '' s = s

Tactic:
image_congr hf,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ (fun a ↦ a) '' s = s
Module: Mathlib.Data.Int.Init

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

Tactic:
show z - 1 - b = -[(b - z).toNat+1] by lia,

Goal state after:
case pos
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
h✝ : z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - 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: α : Sort u
a a' : α
β : (a' : α) → a = a' → Sort v
h : a = a'
f : (a' : α) → (h : a = a') → β a' h
⊢ f a ⋯ = ⋯ ▸ f a' h

Tactic:
cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

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

Tactic:
cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α : Sort u
a a' : α
h : a ≍ a'
⊢ a = a'

Tactic:
cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α β : Sort u
a : α
b : β
h : a ≍ b
⊢ a = cast ⋯ b

Tactic:
cases h; rfl

Goal state after:
Module: Mathlib.Tactic.DepRewrite

Goal state before:
pp: α β : Sort u
a : α
b : β
h : a ≍ b
⊢ cast ⋯ a = b

Tactic:
cases h; rfl

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

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

Tactic:
show z - 1 - b = -[(b - z).toNat+1] by lia,

Goal state after:
case neg
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
h✝ : ¬z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a + b ≤ c ↔ b < c

Tactic:
Int.add_le_iff_le_sub,

Goal state after:
a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a ≤ c - b ↔ b < c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a * a ^ n = a ^ (n + 1)

Tactic:
by
  rw [Int.add_comm, zpow_add, zpow_one]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * (↑u₂ * (u₂.inv * u₁.inv)) = 1

Tactic:
← mul_assoc u₂.val,

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * (↑u₂ * u₂.inv * u₁.inv) = 1
Module: Mathlib.Algebra.Group.InjSurj

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝⁶ : Mul M₂
inst✝⁵ : One M₂
inst✝⁴ : Pow M₂ ℕ
inst✝³ : Inv M₂
inst✝² : Div M₂
inst✝¹ : Pow M₂ ℤ
inst✝ : DivInvMonoid M₁
f : M₁ → M₂
hf : Surjective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
⊢ f x ^ ↑n.succ = f x ^ ↑n * f x

Tactic:
rw [← zpow, ← zpow, zpow_natCast, zpow_natCast, pow_succ, ← mul]

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

Goal state before:
pp: α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑b⁻¹ = ↑d⁻¹ * c ↔ a * ↑d = c * ↑b

Tactic:
mul_comm _ c,

Goal state after:
α : Type u
inst✝ : CommMonoid α
a c : α
b d : αˣ
⊢ a * ↑b⁻¹ = c * ↑d⁻¹ ↔ a * ↑d = c * ↑b
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
⊢ NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0

Tactic:
by
  simp only [forall_and, ← noZeroDivisors_iff_right_eq_zero_of_mul,
    ← noZeroDivisors_iff_left_eq_zero_of_mul, and_self]

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

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : n = 0
⊢ 0 ^ n = 1

pp: case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
· rw [h, pow_zero]

Goal state after:
case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ swap i j * (swap i j * σ) = σ

Tactic:
by
  simp [← mul_assoc]

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a / c = b / d

Tactic:
← mul_left_inj' hc,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
| a / c * c = b / d * c
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = b / d * c

Tactic:
mul_comm _ c,

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a = c * (b / d)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : Ring R
a : R
n : ℕ
⊢ a * (-1) ^ n = 0 ↔ a = 0

Tactic:
by
  obtain h | h := neg_one_pow_eq_or R n <;> simp [h]

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

Goal state before:
pp: α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
a : α
inst✝ : RightDistribClass α
ha : Even a
b : α
⊢ Even (a * b)

Tactic:
rcases ha with ⟨k, rfl⟩
  use k * b
  rw [add_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - d ≤ c + (a - c + (b - d))

Tactic:
← tsub_le_iff_left

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + b - d - c ≤ a - c + (b - d)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b ≤ 0 ↔ a ≤ b

Tactic:
rw [tsub_le_iff_left, add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b ≤ a + c + (b - (a + c))

Tactic:
← tsub_le_iff_left

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - (a + c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a ≤ c + (b - a - c)

Tactic:
← tsub_le_iff_left

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - a - c
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a ≤ b + c ∧ a ≠ b + c

Tactic:
← tsub_le_iff_left

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a - b ≤ c ∧ a ≠ b + c
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftReflectLE α
h : a + d = c + b
⊢ a - b = c - d

Tactic:
calc a - b = a + d - d - b := by rw [add_tsub_cancel_right]
           _ = c + b - b - d := by rw [h, tsub_right_comm]
           _ = c - d := by rw [add_tsub_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ b * a ↔ 1 ≤ b

Tactic:
mul_comm',

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a ≤ a * b ↔ 1 ≤ b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ b * a ≤ a ↔ b ≤ 1

Tactic:
mul_comm',

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : MulOneClass α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ b ≤ 1
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
⊢ c * a ≤ c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ c * a ≤ c * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
⊢ a * c ≤ b * c

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : 0 ≤ a / b
hc : c ≠ 0
⊢ a * c / (b * c) ≤ a / b

Tactic:
rw [mul_div_mul_right _ _ hc]

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b c : G₀
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ a * c / (b * c)

Tactic:
rw [mul_div_mul_right _ _ hc]

Goal state after: