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

Goal state before:
pp: b : Bool
n : Nat
⊢ (2 * n + b.toNat) / 2 = n

Tactic:
Nat.add_comm,

Goal state after:
b : Bool
n : Nat
⊢ (b.toNat + 2 * n) / 2 = n
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: R : Type u_2
inst✝ : Mul R
⊢ IsLeftCancelMul R ∧ IsRightCancelMul R ↔ ∀ (r : R), IsRegular r

Tactic:
isLeftCancelMul_iff,

Goal state after:
R : Type u_2
inst✝ : Mul R
⊢ (∀ (a : R), IsLeftRegular a) ∧ IsRightCancelMul R ↔ ∀ (r : R), IsRegular r
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (n + 1) a = a * npowRec n a

Tactic:
Nat.add_comm,

Goal state after:
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec (1 + n) a = a * npowRec n a
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:
Nat.add_zero,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ m = a ^ m * a ^ 0
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f i ≍ Function.const α (f default) x✝¹

Tactic:
by rw [Subsingleton.elim i default]; rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : Prop → α → Prop
⊢ (fun x1 x2 ↦ x1 ↔ x2) ∘r r = r

Tactic:
by
  grind [eq_comp]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail
α : Type u_1
r : α → α → Prop
a b b✝ c✝ : α
a✝ : ReflTransGen r a b✝
hdb : r b✝ c✝
IH : ∀ {c : α}, r b✝ c → TransGen r a c
c : α
hbc : r c✝ c
⊢ TransGen r a c

Tactic:
| tail _ hdb IH =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ∃ b, ReflTransGen r a b ∧ r b c

Tactic:
| single hac =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
r : α → α → Prop
a c b✝ : α
hac : r a b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b b✝

Tactic:
| single hac =>

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ b✝ : α
hac : r a b✝
⊢ (TransGen p on f) a b✝

Tactic:
exact TransGen.single (h a _ hac)

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case single
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (p on f)
a i✝ b✝ : α
hac : r a b✝
⊢ (TransGen p on f) a b✝

Tactic:
| single hac =>

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

Goal state before:
pp: case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + 1 + k))

Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]

Goal state after:
case succ
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
n : ℕ
ihn : ∀ (k : ℕ), Semiconj f^[n] (g k) (g (n + k))
k : ℕ
⊢ Semiconj f^[n + 1] (g k) (g (n + (k + 1)))
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f.trans g = Equiv.refl α ↔ f.symm = g

Tactic:
trans_eq_refl_iff_eq_symm

Goal state after:
α : Sort u
β : Sort v
f : α ≃ β
g : β ≃ α
⊢ f = g.symm ↔ f.symm = g
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
· simp only [mulSingle_eq_of_ne h, hf']

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ b

Tactic:
rw [min_def]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
Nat.add_comm,

Goal state after:
m n : ℕ
⊢ ¬2 * n % 2 = (1 + 2 * m) % 2
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m✝ n✝ k : ℕ
p : ℕ → Prop
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
m : ℕ
mn : m ≤ n
⊢ motive m mn

Tactic:
induction mn using leRec with

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:
Nat.add_zero,

Goal state after:
case zero
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n ≤ f (n + 0)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
by
  apply le_antisymm
  · rw [h_fa]; exact h_mon h₂
  · exact h_mon h₁

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

Goal state before:
pp: case negSucc.zero
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < f 0

Tactic:
hf₀,

Goal state after:
case negSucc.zero
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ g 1 < default
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s✝ t u : Set α
p : α → Prop
s : Set { a // p a }
⊢ (fun s ↦ {a | ↑a ∈ ↑s}) ((fun s ↦ ⟨{a | ∃ h, ⟨a, h⟩ ∈ s}, ⋯⟩) s) = s

Tactic:
by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z

Tactic:
rw [← sup_inf_left]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : 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
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ⊔ b ≤ c

Tactic:
rw [← le] at *

Goal state after:
α : Type u
β : Type v
inst✝³ : Max α
inst✝² : LE α
inst✝¹ : LT α
inst✝ : SemilatticeSup β
f : α → β
hf_inj : 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
a b c : α
ha : f a ≤ f c
hb : f b ≤ f c
⊢ f (a ⊔ b) ≤ f c
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β γ : Type u₀
ab : α ≃ β
bc : β ≃ γ
x : f α
⊢ ((mapEquiv f ab).trans (mapEquiv f bc)) x = (mapEquiv f (ab.trans bc)) x

Tactic:
by simp [mapEquiv, map_trans']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

Tactic:
rcases h : e (some x) with a | a

Goal state after:
case none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : e (some x) = none
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x

case some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
a : β
h : e (some x) = some a
⊢ some (e.removeNone x) = e none ↔ e.symm none = some x
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ x ⊔ y \ x

Tactic:
by
        rw [sup_sdiff_cancel_right hx]
        grw [sdiff_le]
        rw [sup_eq_right.2 hz]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
a b : α✝
α : Type w
s : α ⊕ PUnit
⊢ (fun o ↦ o.elim (inr PUnit.unit) inl) ((fun s ↦ Sum.elim some (fun x ↦ none) s) s) = s

Tactic:
rcases s with (_ | ⟨⟨⟩⟩) <;> rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : BiheytingAlgebra β
⊢ BiheytingAlgebra α

Tactic:
by
  let heytingAlgebra := e.heytingAlgebra
  let coheytingAlgebra := e.coheytingAlgebra
  apply e.injective.biheytingAlgebra <;> intros <;> first | rfl | exact e.apply_symm_apply _

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 a ⊓ (f b)ᶜ = f a ⊓ f bᶜ

Tactic:
map_compl

Goal state after:
α : 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 a ⊓ (f b)ᶜ = f a ⊓ (f b)ᶜ
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 ⊔ f aᶜ

Tactic:
map_compl

Goal state after:
α : 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 ⊔ (f a)ᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅

Tactic:
simp only [eq_empty_iff_forall_notMem]
  exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ range val = s

Tactic:
rw [← image_univ]
  simp [-image_univ, coe_image]

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : ¬i ∈ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ (i : ι), i ∈ s → x i ∈ t i
⊢ (∀ (i_1 : ι), i_1 ∈ s → update x i xᵢ i_1 ∈ t i_1) ∧ update x i xᵢ i = xᵢ

Tactic:
simpa +contextual [(ne_of_mem_of_not_mem · hi)]

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

Goal state before:
pp: α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x✝ : ↑s
⊢ ↑((restrict f s s h)^[n] x✝) = ↑(restrict f^[n] s s ⋯ x✝)

Tactic:
simpa using coe_iterate_restrict _ _ _

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
⊢ b ∈ Pi.map f '' s.pi t

Tactic:
have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
    if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
f : (i : ι) → α i → β i
hf : ∀ (i : ι), ¬i ∈ s → Surjective (f i)
t : (i : ι) → Set (α i)
b : (i : ι) → β i
hb : b ∈ s.pi fun i ↦ f i '' t i
this : ∀ (i : ι), ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i)
⊢ b ∈ Pi.map f '' s.pi t
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: 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)⁻¹
a b : G
⊢ f (a / b) = f a / f b

Tactic:
grind [div_eq_mul_inv]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (m + (n - m)) = a ^ n

Tactic:
Nat.add_comm,

Goal state after:
M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m + m) = a ^ n
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by rw [inv_zpow, zpow_neg]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rab : r a b
⊢ f a c = f a b * f b c

Tactic:
exact hmul rab rbc pab pbc pac

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ (n + 1) • a = n • a + a

Tactic:
add_nsmul,

Goal state after:
α✝ : Type u_1
β : Type u_2
G : Type u_3
M : Type u_4
α : Type u_5
s : AddCommMonoid α
n : ℕ
a : α
⊢ n • a + 1 • a = n • a + a
Module: Mathlib.Algebra.GroupWithZero.Defs

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
⊢ ∀ (y : M₀), f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
intro y; rw [pow_succ', pow_succ', mul_assoc, mul_assoc, hx, hn]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
⊢ (if (k + 1) % 2 = 0 then ((k + 1) / 2).binCast + ((k + 1) / 2).binCast
    else ((k + 1) / 2).binCast + ((k + 1) / 2).binCast + 1) =
    ↑(k + 1)

Tactic:
conv => rhs; rw [← Nat.mod_add_div (k + 1) 2]
        rw [if_pos h, hk _ <| Nat.div_lt_self (Nat.succ_pos k) (Nat.le_refl 2), ← Nat.cast_add]
        rw [h, Nat.zero_add, Nat.succ_mul, Nat.one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ (m + (n - m))

Tactic:
Nat.add_comm,

Goal state after:
α : Type u_1
inst✝ : Monoid α
m n : ℕ
a : α
h : m ≤ n
⊢ a ^ n = a ^ (n - m + m)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ x⁻¹ʳ * (x * y) = y

Tactic:
by
  rw [← mul_assoc, inverse_mul_cancel x h, one_mul]

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

Goal state before:
pp: case inr
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
h✝ : Nontrivial M₀
⊢ IsUnit a

Tactic:
contrapose h
      rw [Ring.inverse_non_unit _ h]
      exact not_isUnit_zero

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
a b : α
u₁ u₂ : αˣ
⊢ a * ↑u₁⁻¹ + ↑u₂⁻¹ * b = a * ↑u₂ * (↑u₂⁻¹ * ↑u₁⁻¹) + ↑u₂⁻¹ * ↑u₁⁻¹ * (↑u₁ * b)

Tactic:
rw [← mul_assoc, ← mul_assoc, mul_assoc a, mul_assoc (↑u₂⁻¹ : α), mul_inv, inv_mul, mul_one,
    mul_one]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (2 + b) ≤ a + (a + a * b)

Tactic:
gcongr; exact le_mul_of_one_le_left b0 <| one_le_two.trans a2

Goal state after:
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
d : R
hcd : 0 = c + d
⊢ a * c + (b * d + a * d) ≤ b * c + (b * d + a * d)

Tactic:
calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := by gcongr; exact hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

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 + b + b * c ≤ c
⊢ 1 + a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]
  gcongr

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

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ (e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft) f a = (e₁₂.trans e₂₃).arrowCongrLeft f a

Tactic:
simp only [trans_apply, arrowCongrLeft_apply, Pi.default_def, coe_trans]

Goal state after:
α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a = extend (⇑e₂₃ ∘ ⇑e₁₂) f (fun a ↦ default) a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
by
  rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

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₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b < a ↔ b < c * a

Tactic:
by
  rw [← mul_lt_mul_iff_of_pos_left hc, mul_inv_cancel_left₀ hc.ne']

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀); simp only [← not_le, inv_nonneg]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ 0 < (x - a) * (x - b) ↔ x < a ∨ b < x

Tactic:
by
  rw [mul_pos_iff, sub_pos, sub_pos, sub_neg, sub_neg, and_iff_right_of_imp h.trans_lt,
    and_iff_left_of_imp h.trans_lt', or_comm]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ { toFun := fun p ↦ (↑g).comp (p.comp ↑f.symm), invFun := fun p ↦ (↑g.symm).comp (p.comp ↑f), left_inv := ⋯,
          right_inv := ⋯ }
        p ≤
      { toFun := fun p ↦ (↑g).comp (p.comp ↑f.symm), invFun := fun p ↦ (↑g.symm).comp (p.comp ↑f), left_inv := ⋯,
          right_inv := ⋯ }
        q ↔
    p ≤ q

Tactic:
simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe,
               OrderHomClass.coe_coe, Function.comp_apply, map_le_map_iff]

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p q : α →o β
⊢ (∀ (x : γ), p (f.symm x) ≤ q (f.symm x)) ↔ ∀ (x : α), p x ≤ q x
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
g : β →o α
h₁ : f.comp g = OrderHom.id
h₂ : g.comp f = OrderHom.id
a✝ b✝ : α
h :
  { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ } a✝ ≤
    { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ } b✝
⊢ a✝ ≤ b✝

Tactic:
by simpa [h₂] using show g.comp f _ ≤ g.comp f _ from map_rel g h

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x

Tactic:
exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
hac : a ≤ b
hcd : b ≤ c
d : G
h : b ≤ d
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

Tactic:
· rw [mabs_of_le_one <| div_le_one'.mpr h, inv_div]
    exact le_max_of_le_right <| div_le_div_left' hac _

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

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (t * k)) - ↑x * (k * s)

Tactic:
mul_comm k s,

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH :
  ∀ {s t s' t' : ℤ},
    ↑b % ↑a = ↑x * s + ↑y * t →
      ↑a = ↑x * s' + ↑y * t' →
        ↑((b % a).xgcdAux s t a s' t').1 =
          ↑x * ((b % a).xgcdAux s t a s' t').2.1 + ↑y * ((b % a).xgcdAux s t a s' t').2.2
s t s' t' : ℤ
p : ↑a = ↑x * s + ↑y * t
p' : ↑b = ↑x * s' + ↑y * t'
k : ℤ
⊢ ↑x * s' + ↑y * t' - (↑x * s * k + ↑y * t * k) = ↑x * s' + (↑y * t' - ↑y * (t * k)) - ↑x * (s * k)
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b

Tactic:
refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩

Goal state after:
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
by
  rintro (_ | b) (_ | c) <;> simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

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

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

Tactic:
by
  rintro (_ | b) (_ | c) <;> simp [none_eq_top, some_eq_coe, ← coe_add, ha.eq_iff]

Goal state after: