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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n % 2 = b.toNat

Tactic:
by
  cases b <;> simp [bit_val]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b : G
h : Commute a b
n : ℕ
⊢ (a * b) ^ ↑n = a ^ ↑n * b ^ ↑n

Tactic:
simp [zpow_natCast, h.mul_pow n]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! x, p (f x)
x : α
hpx : (fun x ↦ p (f x)) x
hx : ∀ (y : α), (fun x ↦ p (f x)) y → y = x
y : β
hy : (fun y ↦ p y) y
z : α
hz : f z = y
⊢ (fun x ↦ p (f x)) z

Tactic:
by simpa [hz]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Bijective f
g : α → γ
⊢ (fun g ↦ g ∘ f) (g ∘ surjInv ⋯) = g

Tactic:
by simp only [comp_assoc g _ f, (leftInverse_surjInv hf).comp_eq_id, comp_id]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case tail.single
α : Type u_1
r : α → α → Prop
a✝¹ b✝ c : α
h : ∀ (a b c : α), r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d
hac : ReflTransGen r a✝¹ c
d e : α
a✝ : ReflTransGen r a✝¹ d
hde : r d e
b : α
hdb : ReflTransGen r d b
hcb : ReflTransGen r c b
a : α
hea : ReflTransGen r e a
hba : r b a
⊢ Join (ReflTransGen r) e c

Tactic:
exact ⟨a, hea, hcb.tail hba⟩

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g⁻¹ • g • a = a

Tactic:
rw [smul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
h : ∀ (x : M) (y : N), x • 1 * y = x • y
x : M
y z : N
⊢ (x • y) • z = x • y • z

Tactic:
rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ ¬Nonempty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β

Tactic:
not_nonempty_iff,

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ ¬IsEmpty α ∧ ¬Nonempty β

Tactic:
not_nonempty_iff,

Goal state after:
α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ ¬IsEmpty α ∧ IsEmpty β
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) → Semigroup (f i)
⊢ ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c)

Tactic:
intros; ext; exact mul_assoc _ _ _

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Goal state after:
case inl.inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : x < z
⊢ False

case inl.inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : y < z
h₃ : z < x
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Goal state after:
case inl.inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : x < z
⊢ False

case inl.inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : x < y
h₂ : z < y
h₃ : z < x
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Goal state after:
case inr.inl.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : x < z
⊢ False

case inr.inl.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : y < z
h₃ : z < x
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
⊢ False

Tactic:
rcases hne.2.2.lt_or_gt with h₃ | h₃

Goal state after:
case inr.inr.inl
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : x < z
⊢ False

case inr.inr.inr
α : Type u_2
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
hne : x ≠ y ∧ y ≠ z ∧ x ≠ z
h₁ : y < x
h₂ : z < y
h₃ : z < x
⊢ False
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
by rw [eq_bot_iff, sup_le_iff]; simp

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.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 < g 0

Tactic:
exact hg Nat.zero_lt_one

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

Goal state before:
pp: α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then ∅ else t h) ↔ ∃ h, x ∈ t h

Tactic:
simp only [mem_dite, mem_empty_iff_false, imp_false]
  exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩

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

Goal state before:
pp: α : Type u_1
s : Set α
x : α
⊢ s = ∅ ∧ s ≠ {x} ∨ False ↔ s = ∅

Tactic:
or_false,

Goal state after:
α : Type u_1
s : Set α
x : α
⊢ s = ∅ ∧ s ≠ {x} ↔ s = ∅
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⊔ b ⇨ c ↔ d ≤ (a ⇨ c) ⊓ (b ⇨ c)

Tactic:
rw [le_inf_iff, le_himp_comm, sup_le_iff]
    simp_rw [le_himp_comm]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
by rw [sup_comm]; exact le_himp_iff

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a \ c ⊔ (b ⊔ c \ b)

Tactic:
sup_sdiff_self,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a \ c ⊔ (b ⊔ c)
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬(e (some x)).isSome = true
⊢ (e none).isSome = true

Tactic:
rw [← Option.ne_none_iff_isSome]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : ¬(e (some x)).isSome = true
⊢ e none ≠ none
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
by rw [sup_comm]; exact le_himp_iff

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
⊢ HeytingAlgebra α

Tactic:
apply e.injective.heytingAlgebra <;> intros

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊤ = ⊤

case map_bot
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := ⋯
bot : Bot α := ⋯
compl : Compl α := ⋯
⊢ e ⊥ = ⊥

case map_compl
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ : α
⊢ e a✝ᶜ = (e a✝)ᶜ

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : HeytingAlgebra β
generalizedHeytingAlgebra : GeneralizedHeytingAlgebra α := e.generalizedHeytingAlgebra
bot : Bot α := e.bot
compl : Compl α := e.compl
a✝ b✝ : α
⊢ e (a✝ ⇨ b✝) = e a✝ ⇨ e b✝
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : f x = x✝
⊢ x✝ ∈ range fun x ↦ f ↑x

Tactic:
exact ⟨⟨x, h1⟩, h2⟩

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : RightCancelMonoid N
f : M →ₙ* N
⊢ f 1 = 1

Tactic:
have h : 1 * f 1 = f 1 * f 1 := by simpa using f.map_mul' 1 1

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
M✝ : Type u_4
N✝ : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝⁵ : MulOne M✝
inst✝⁴ : MulOne N✝
inst✝³ : FunLike F M✝ N✝
inst✝² : MonoidHomClass F M✝ N✝
M : Type u_10
N : Type u_11
inst✝¹ : Monoid M
inst✝ : RightCancelMonoid N
f : M →ₙ* N
h : 1 * f 1 = f 1 * f 1
⊢ f 1 = 1
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
⊢ ∃ s', s' ⊆ s ∧ BijOn f s' t

Tactic:
have : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩

Goal state after:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s', s' ⊆ s ∧ BijOn f s' t
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:
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 : α
n : ℕ
⊢ a⁻¹ * a⁻¹ ^ n = (a ^ n * a)⁻¹

Tactic:
inv_pow _ n,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ * (a ^ n)⁻¹ = (a ^ n * a)⁻¹
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
rw [h, mul_inv_cancel_left]

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

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

Tactic:
rw [h, mul_inv_cancel_left]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ c / d = 1 ↔ c = d

Tactic:
div_eq_one

Goal state after:
G : Type u_3
inst✝ : Group G
a b c d : G
H : a / b = c / d
⊢ c = d ↔ c = d
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
u : αˣ
⊢ a * (↑u⁻¹ * ↑u) = a

Tactic:
by rw [Units.inv_mul, mul_one]

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

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

Tactic:
rw [h, mul_inv_cancel_left]

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

Goal state before:
pp: case pred
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)

Tactic:
zpow_sub_one₀ ha,

Goal state after:
case pred
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * (a ^ (-↑n) * a⁻¹)
Module: Mathlib.Algebra.Group.Int.Defs

Goal state before:
pp: m : ℕ
n : ℤ
⊢ ↑m.succ • n = ↑m • n + n

Tactic:
simp only [HSMul.hSMul, SMul.smul, natCast_succ, Int.add_mul, Int.add_comm, Int.one_mul]

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
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.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
    fun k x ↦ Int.strongRec lt ge k

Tactic:
revert ih

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
hn : m ≤ n
⊢ (∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m : ℤ
n : ℕ
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
by
  obtain hn | hn := natAbs_eq m <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.neg_dvd]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: n : ℕ
⊢ Even ↑n ↔ Even n

Tactic:
even_iff

Goal state after:
n : ℕ
⊢ ↑n % 2 = 0 ↔ Even n
Module: Mathlib.Algebra.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
⊢ [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE

Tactic:
by
  simp_rw [isLeftCancelMulZero_iff, isRightCancelMulZero_iff, isCancelMulZero_iff_forall_isRegular,
    isLeftRegular_iff_right_eq_zero_of_mul, isRightRegular_iff_left_eq_zero_of_mul,
    isRegular_iff_eq_zero_of_mul]
  tfae_have 1 ↔ 2 := noZeroDivisors_iff_right_eq_zero_of_mul
  tfae_have 1 ↔ 3 := noZeroDivisors_iff_left_eq_zero_of_mul
  tfae_have 1 ↔ 4 := noZeroDivisors_iff_eq_zero_of_mul
  tfae_finish

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

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b c d : M
hbd : Commute b d
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
by
  rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, hbd.right_comm,
    hd.div_mul_cancel]

Goal state after:
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑(n + 1) • b = (n + 1) • b

Tactic:
rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

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

Goal state before:
pp: case inl
k : ℕ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
use k

Goal state after:
case h
k : ℕ
⊢ Xor (k + k = 2 * k) (k + k = 2 * k + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
use k

Goal state after:
case h
k : ℕ
⊢ Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b⁻¹ * a < c ↔ a < b * c

Tactic:
rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2
a : α
ha : 0 ≤ a
b c : α
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
by
        obtain ha | ha := ha.eq_or_lt
        · simp [← ha]
        · exact @CovariantClass.elim α>0 α (fun x y => y * x) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
⊢ (fun x1 x2 ↦ x1 < x2) b c

Tactic:
by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha] at h
        · exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False

Tactic:
apply not_lt_of_ge hab _

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ a * b < 0
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 / c < b / c ↔ a < b

Tactic:
by
  rw [div_lt_iff₀ hc, div_mul_cancel₀ _ hc.ne']

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
⊢ b < x ∧ x < a → a < x ∧ x < b

Tactic:
exact And.imp h.trans_lt h.trans_lt'

Goal state after:
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
r : α → α → Prop
s : β → β → Prop
h₁ : α = β
h₂ : r ≍ s
a b : α
⊢ s ((Equiv.cast h₁) a) ((Equiv.cast h₁) b) ↔ r a b

Tactic:
subst h₁
    rw [eq_of_heq h₂]
    rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)

Tactic:
inv_inf,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹))
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
ha : 1 ≤ a
k : ℕ
⊢ 1 ≤ a ^ k * a

Tactic:
exact one_le_mul (one_le_pow_of_le ha k) ha

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 + 1)

Tactic:
by
    rw [pow_succ]
    exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

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

Goal state before:
pp: a b : ℤ
H1 : 0 ≤ a
H2✝ : a < |b|
n : ℕ
H2 : a < ↑-[n+1].natAbs
⊢ -(a / -[n+1]) = -0

Tactic:
rw [← Int.ediv_neg]; exact ediv_eq_zero_of_lt H1 H2

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

Goal state before:
pp: case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
use k

Goal state after:
case h
k : ℤ
⊢ Xor (k + k = 2 * k) (k + k = 2 * k + 1)
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
use k

Goal state after:
case h
k : ℤ
⊢ Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑(a.toNat * (p + 1)) + ↑(b.toNat * (q + 1)) = ↑n

Tactic:
Nat.cast_mul,

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑a.toNat * ↑(p + 1) + ↑(b.toNat * (q + 1)) = ↑n
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑a.toNat * ↑(p + 1) + ↑(b.toNat * (q + 1)) = ↑n

Tactic:
Nat.cast_mul,

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
⊢ ↑a.toNat * ↑(p + 1) + ↑b.toNat * ↑(q + 1) = ↑n
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: case inr.inl
α : Type u
inst✝² : Monoid α
inst✝¹ : LinearOrder α
inst✝ : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
hc : a ≤ c
⊢ min a (b * c) = min a (min a b * min a c)

Tactic:
simp [hc, le_mul_left]

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✝ : PartialOrder α
a✝¹ a✝ : α
⊢ a✝¹ ≤ a✝ → a✝ ≤ a✝¹ → a✝¹ = a✝

Tactic:
simpa using le_antisymm

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

Goal state before:
pp: x : WithZero (Multiplicative ℤ)
hx : x ≠ 0
y : WithZero (Multiplicative ℤ)
hnz : y ≠ 0
hyx : y < x
⊢ -y.log ≤ ↑(-y.log).toNat

Tactic:
exact Int.self_le_toNat _

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, floor_natCast]

Goal state after: