mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : Nat.bit b n = 0
⊢ binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

Tactic:
obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h : bit false 0 zero = zero ∨ (0 = 0 → false = true)
h' : Nat.bit false 0 = 0
⊢ binaryRec zero bit (Nat.bit false 0) = bit false 0 (binaryRec zero bit 0)
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

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

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
H : x' = y'
⊢ x = y

Tactic:
rw [← hx', ← hy', H]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x1 x2 ↦ f x1 = x2

Tactic:
simp [forall_existsUnique_iff, funext_iff]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inl
α : Type u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

pp: case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
· exact .single .refl

Goal state after:
case refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: case succ
α : Type u
f g : α → α
h : Commute f g
n : ℕ
ihn : (f ∘ g)^[n] = f^[n] ∘ g^[n]
x : α
⊢ (f ∘ g)^[n + 1] x = (f^[n + 1] ∘ g^[n + 1]) x

Tactic:
simp only [ihn, (h.iterate_right n).eq, iterate_succ, comp_apply]

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]

Tactic:
by rw [Nat.mul_comm]

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
exact compare_gt_iff_gt

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f a b)

Tactic:
comm.comm a

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), A_le a a
le_trans✝ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm✝ : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total✝ : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge✝ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
a b : α
⊢ A_compare a b = B_compare a b

Tactic:
exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x < update x i a ↔ x i < a

Tactic:
simp [lt_iff_le_not_ge]

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ a < ⊤ ↔ ¬⊤ ≤ a

Tactic:
simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind.inl
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst < (a', b).fst
hb : x.snd ≤ (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

Tactic:
exact iha x.1 (ha'.trans_le ha) x.1 le_rfl x.2

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : MonotoneOn f {x | k ≤ x}
x y : ℕ
hle : x ≤ y
⊢ (fun n ↦ f (n + k)) x ≤ (fun n ↦ f (n + k)) y

Tactic:
rw [← Nat.add_le_add_iff_right] at hle
    exact h (Nat.le_add_left k x) (Nat.le_add_left k y) hle

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

Goal state before:
pp: α : Type u
s : Set α
⊢ ¬univ ⊆ s ↔ ∃ a, ¬a ∈ s

Tactic:
simp [not_subset]

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
by
  simp only [inf_sup_left, inf_comm _ c]

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

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

Tactic:
rw [inf_inf_sdiff, inf_bot_eq]

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

Goal state before:
pp: α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ (sigmaSigmaSubtype p h).symm c = ⟨⟨a, ⟨b, c⟩⟩, h⟩

Tactic:
rw [Equiv.symm_apply_eq]

Goal state after:
α : Type u_9
β : α → Type u_10
γ : (a : α) → β a → Type u_11
p : (a : α) × β a → Prop
uniq : Unique { ab // p ab }
a : α
b : β a
c : γ a b
h : p ⟨a, b⟩
⊢ c = (sigmaSigmaSubtype p h) ⟨⟨a, ⟨b, c⟩⟩, h⟩
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

Tactic:
rw [sdiff_symmDiff, sdiff_sup]

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

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

Tactic:
by rw [map_sup, map_compl]

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
right
      refine ⟨t \ {a}, by grind⟩

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
i j : α
h : i ≠ j
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g i = s.piecewise f g i

Tactic:
by simp [piecewise, h]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f

Tactic:
refine ⟨fun h y => ?_, Surjective.image_surjective⟩
  rcases h {y} with ⟨s, hs⟩
  have := mem_singleton y; rw [← hs] at this; rcases this with ⟨x, _, hx⟩
  exact ⟨x, hx⟩

Goal state after:
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)
b : β
hb : b ∈ t
⊢ p b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb; exact h _ ha

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

Goal state before:
pp: 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 : ℤ
⊢ motive n

Tactic:
by
  refine if hnm : n < m then lt n hnm else ge n (by lia) (n.inductionOn' m lt ?_ ?_)
  · intro _n _ ih l _
    exact if hlm : l < m then lt l hlm else ge l (by lia) fun k _ ↦ ih k (by lia)
  · exact fun n _ hn l _ ↦ hn l (by lia)

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * Int.negSucc n) = (a ^ ↑m) ^ Int.negSucc n

Tactic:
by
    rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]

Goal state after:
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:
rw [Int.add_comm, zpow_add, zpow_one]

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

Goal state before:
pp: case succ
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 ^ (↑n + 1))

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

Goal state after:
case succ
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)
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:
by
      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✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩
    exact mul_one _

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

Goal state before:
pp: α : Type u
inst✝¹ : RightCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩
    exact mul_one _

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

Goal state before:
pp: α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩
    exact mul_one _

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure <$> a) = a

Tactic:
by
  simp only [joinM, id, ← bind_pure_comp, bind_assoc, pure_bind, bind_pure]

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

Goal state before:
pp: case succ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ IsNilpotent (x ^ (n✝ + 1))

Tactic:
exact IsNilpotent.pow_succ _ hx

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Mul M
inst✝¹ : Group G
H : Type u_7
inst✝ : Group H
ϕ : G ≃* H
x✝ : MulAut G
⊢ (fun f ↦ ϕ.trans (MulEquiv.trans f ϕ.symm)) ((fun f ↦ ϕ.symm.trans (MulEquiv.trans f ϕ)) x✝) = x✝

Tactic:
simp [DFunLike.ext_iff]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Mul M
inst✝¹ : Group G
H : Type u_7
inst✝ : Group H
ϕ : G ≃* H
x✝ : MulAut H
⊢ (fun f ↦ ϕ.symm.trans (MulEquiv.trans f ϕ)) ((fun f ↦ ϕ.trans (MulEquiv.trans f ϕ.symm)) x✝) = x✝

Tactic:
simp [DFunLike.ext_iff]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Mul M
inst✝¹ : Group G
H : Type u_7
inst✝ : Group H
ϕ : G ≃* H
⊢ ∀ (x y : MulAut G),
    ϕ.symm.trans (MulEquiv.trans (x * y) ϕ) = ϕ.symm.trans (MulEquiv.trans x ϕ) * ϕ.symm.trans (MulEquiv.trans y ϕ)

Tactic:
simp [DFunLike.ext_iff]

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

Goal state before:
pp: α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c

Tactic:
by
  simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
rw [h.neg_zpow, one_zpow]

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

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

Tactic:
by
  rw [← mul_le_mul_iff_right a]
  simp

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

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

Tactic:
by
  rw [← mul_le_mul_iff_right a]
  simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightMono α
h : (c < a ∧ d < a) ∧ c < b ∧ d < b
⊢ c * d < a * b

Tactic:
exact mul_lt_mul_of_le_of_lt h.1.1.le h.2.2

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ c * b

Tactic:
mul_comm c

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.Group.Defs

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
a : α
⊢ a < a⁻¹ ↔ a < 1

Tactic:
contrapose!; exact inv_le_self_iff

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
· refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : a + c + b * c ≤ b
⊢ 1 + a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℤ
hn : 0 ≤ n
⊢ MonotoneOn (fun a ↦ a ^ n) {a | 0 ≤ a}

Tactic:
by
  lift n to ℕ using hn; simpa using pow_left_monotoneOn

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
⊢ x = y

Tactic:
rcases trichotomous_of r x y with (h | h | h)

Goal state after:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
⊢ x = y

case inr.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y

case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
h : a < 1
hn : n ≠ 0
⊢ a ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩

Goal state after:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a ^ k.succ < 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
hx : 1 < x
n : ℤ
hn : 0 < n
⊢ 1 < x ^ n

Tactic:
lift n to ℕ using Int.le_of_lt hn
  rw [zpow_natCast]
  exact one_lt_pow' hx (Int.natCast_pos.mp hn).ne'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Odd n
⊢ (-1) ^ n = -1

Tactic:
rw [h.neg_zpow, one_zpow]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ 1 ≤ a / b

Tactic:
one_le_div'

Goal state after:
case inr
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ba : b ≤ a
⊢ b ≤ a
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
h : s ≠ 0
⊢ s.gcdA 0 = 1

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  simp [gcdA, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: a b : ℤ
ha : a ≠ 0
⊢ IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b)

Tactic:
simp_rw [← gcd_dvd_iff]
  constructor
  · simpa [and_true, dvd_refl, Set.mem_ofPred_eq] using gcd_pos_of_ne_zero_left b ha
  · simp only [lowerBounds, and_imp, Set.mem_ofPred_eq]
    exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
⊢ b * a = b * 0 ↔ a = 0

Tactic:
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
⊢ a * b = 0 * b ↔ a = 0

Tactic:
exact ⟨fun h ↦ hb h, fun ha ↦ by rw [ha]⟩

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

Goal state before:
pp: case ofNat
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.ofNat a✝).log = Int.ofNat a✝ • x.log

Tactic:
simp [log_pow, log_inv]

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

Goal state before:
pp: case negSucc
G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
a✝ : ℕ
⊢ (x ^ Int.negSucc a✝).log = Int.negSucc a✝ • x.log

Tactic:
simp [log_pow, log_inv]

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

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
⊢ f (1 x) = 1 x

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  · rw [one_apply_of_ne_zero hx, one_apply_of_ne_zero hx, map_one]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + (c + (b - c))

Tactic:
add_tsub_cancel_of_le h₂,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + b
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
⊢ ⊥ < ⊥ ↔ ⊥ ≤ ⊥ ∧ ¬⊥ ≤ ⊥

Tactic:
simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ⊥ < ↑a✝ ↔ ⊥ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ⊥

Tactic:
simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝ : α
⊢ ↑a✝ < ⊥ ↔ ↑a✝ ≤ ⊥ ∧ ¬⊥ ≤ ↑a✝

Tactic:
simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : Preorder α
a✝¹ a✝ : α
⊢ ↑a✝¹ < ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ ∧ ¬↑a✝ ≤ ↑a✝¹

Tactic:
simp [lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
⊢ ⌈0⌉₊ = 0

Tactic:
by rw [← Nat.cast_zero, ceil_natCast]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
x y z : WithTop α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
cases x <;> cases y <;> cases z <;> simp [← WithTop.coe_inf, ← WithTop.coe_sup]

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝ : DistribLattice α
a✝² a✝¹ a✝ : α
⊢ (a✝² ⊔ a✝¹) ⊓ (a✝² ⊔ a✝) ≤ a✝² ⊔ a✝¹ ⊓ a✝
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌊a⌋₊| ≤ 1

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - ↑⌊a⌋₊

case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - ↑⌊a⌋₊ ≤ 1
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}

Tactic:
Set.pair_comm

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ |a - ↑⌈a⌉₊| ≤ 1

Tactic:
refine abs_le.mpr ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ -1 ≤ a - ↑⌈a⌉₊

case refine_2
R : Type u_1
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ a - ↑⌈a⌉₊ ≤ 1
Module: Mathlib.Algebra.Group.Invertible.Defs

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible a
h : ⅟a = b
⊢ a * b = 1

Tactic:
rw [← h, mul_invOf_self]

Goal state after: