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

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n / 2 = n

Tactic:
by
  rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
  · cases b <;> decide
  · decide

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ : p x
y : α
property✝ : p y
⊢ ⟨x, property✝¹⟩ = ⟨y, property✝⟩

Tactic:
by cases Subsingleton.elim x y; rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α₁ α₂ : Sort u
β₁ : α₁ → Sort v
β₂ : α₂ → Sort v
f₁ : (a : α₁) → β₁ a
f₂ : (a : α₂) → β₂ a
a₁ : α₁
a₂ : α₂
hargs : a₁ ≍ a₂
ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂
hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂
⊢ f₁ a₁ ≍ f₂ a₂

Tactic:
cases hargs
  cases funext fun v => ht v v .rfl
  cases hf rfl .rfl
  rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : α
s : p → β
t : ¬p → β
⊢ (a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h

Tactic:
by_cases h : p <;> simp [h]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Membership α β
p : Prop
inst✝ : Decidable p
a : p → α
b : ¬p → α
s : β
⊢ (if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s

Tactic:
by_cases h : p <;> simp [h]

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

Goal state before:
pp: case neg
γ : Sort u_3
α₁ : Sort u_4
α₂ : Sort u_5
α₃ : Sort u_6
f₁₂ : α₁ → α₂
h₁₂ : Injective f₁₂
f₂₃ : α₂ → α₃
h₂₃ : Injective f₂₃
g : α₁ → γ
e' : α₃ → γ
a : α₃
h₃ : ¬∃ b, f₂₃ b = a
⊢ extend (f₂₃ ∘ f₁₂) g e' a = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' a

Tactic:
· rw [extend_apply' _ _ _ h₃, extend_apply']
    exact fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y

Tactic:
reflTransGen_iff_eq_or_transGen,

Goal state after:
α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ y = x ∨ TransGen r x y
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a

Tactic:
obtain h | h := Nat.le_total m n
  { simp [Nat.sub_eq_zero_of_le h] }
  { exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy x (r • a) (r • b)

Tactic:
rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]

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

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy (r • x) a b

Tactic:
rw [SemiconjBy, mul_smul_comm, smul_mul_assoc, h.eq]

Goal state after:
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMinOrder β
x✝ : α × β
a : α
b : β
⊢ ∃ b_1, b_1 < (a, b)

Tactic:
by
    obtain ⟨c, h⟩ := exists_lt b
    exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : OrderTop α
a : α
⊢ (∃ b, a < b) ↔ a < ⊤

Tactic:
exact ⟨fun ⟨b, hb⟩ ↦ hb.trans_le le_top, fun h ↦ ⟨⊤, h⟩⟩

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

Goal state before:
pp: case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction of_succ self ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn

Tactic:
decreasingInduction_succ _ _ (Nat.le_trans hmn hnk),

Goal state after:
case step
m n k : ℕ
hmn : m ≤ n
m✝ : ℕ
hnk : n.le m✝
ih :
  ∀ {motive : (m : ℕ) → m ≤ m✝ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m✝) → motive (k + 1) h → motive k ⋯)
    (self : motive m✝ ⋯),
    decreasingInduction of_succ self ⋯ =
      decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m✝.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m✝.succ) → motive (k + 1) h → motive k ⋯
self : motive m✝.succ ⋯
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (of_succ m✝ ⋯ self) ⋯ =
    decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ⋯) hmn
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:
apply le_antisymm
  · rw [h_fa]; exact h_mon h₂
  · exact h_mon h₁

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ Disjoint ↑a ↑b ↔ Disjoint a b

Tactic:
rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ f (max x y) = f x ⊔ f y

Tactic:
simp only [h, hf h, sup_of_le_right]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Max α
inst✝⁵ : Min α
inst✝⁴ : LE α
inst✝³ : LT α
inst✝² : Top α
inst✝¹ : HImp α
inst✝ : GeneralizedHeytingAlgebra β
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_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ a ≤ ⊤

Tactic:
rw [← le, map_top]
    exact le_top

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

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

Tactic:
rw [sdiff_eq, sdiff_eq, inter_right_comm]

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:
by rcases s with (_ | ⟨⟨⟩⟩) <;> rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
e : α ≃ β
inst✝ : GeneralizedBooleanAlgebra β
bot : Bot α := e.bot
sdiff : SDiff α := e.sdiff
distribLattice : DistribLattice α := e.distribLattice
⊢ GeneralizedBooleanAlgebra α

Tactic:
apply e.injective.generalizedBooleanAlgebra <;> intros <;>
  first | rfl | exact e.apply_symm_apply _

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

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
α : Type ?u.18
β : Type ?u.17
γ : Type ?u.15
⊢ LeftInverse (fun s ↦ Sum.elim (Prod.map inl id) (Prod.map inr id) s) fun p ↦
    Sum.map (fun x ↦ (x, p.snd)) (fun x ↦ (x, p.snd)) p.fst

Tactic:
by
      rintro ⟨_ | _, _⟩ <;> rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Tactic:
simp only [inter_comm, image_inter_preimage]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
x : α
⊢ Sum.inl x ∈ range Sum.inl ⊔ range Sum.inr

Tactic:
left

Goal state after:
case inl
α : Type u_1
β : Type u_2
x : α
⊢ Sum.inl x ∈ range Sum.inl
Module: Mathlib.Data.Set.Piecewise

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

Tactic:
left

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : x ∈ s
⊢ s.piecewise f g x ∈ f '' s
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
⊢ BijOn f (s ∩ f ⁻¹' r) r

Tactic:
refine ⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩
  obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)
  exact ⟨y, ⟨hy, hx⟩, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : M →* G
a b : M
⊢ (f (a * b))⁻¹ = (f a)⁻¹ * (f b)⁻¹

Tactic:
← mul_inv,

Goal state after:
α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : CommGroup G
inst✝ : CommGroup H
f : M →* G
a b : M
⊢ (f (a * b))⁻¹ = (f a * f b)⁻¹
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
k n : ℕ
x✝ : M
⊢ (fun x ↦ x ^ k)^[n + 1] x✝ = x✝ ^ k ^ (n + 1)

Tactic:
simp [pow_iterate, Nat.pow_succ', pow_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ (1 / a) ^ n = 1 / a ^ n

Tactic:
by simp only [one_div, inv_pow]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℕ
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
simp only [div_eq_mul_inv, mul_pow, inv_pow]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b
Module: Mathlib.Control.Basic

Goal state before:
pp: F : Type → Type v
inst✝ : Alternative F
h : Decidable True
⊢ guard True = pure ()

Tactic:
by simp [guard]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑(subtypeCongrHom p)

Tactic:
by
  rintro ⟨⟩ ⟨⟩ h
  rw [Prod.mk_inj]
  constructor <;> ext i <;> simpa using Equiv.congr_fun h i

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * (a⁻¹ * a)

Tactic:
inv_mul_cancel₀ ha,

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹ * 1
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i

Tactic:
by rw [zpow_add₀ h, zpow_one]

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

Goal state before:
pp: α : Type u
R : Type v
inst✝ : NonUnitalNonAssocRing α
a b : α
⊢ a * -b + a * b = 0

Tactic:
rw [← left_distrib, neg_add_cancel, mul_zero]

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

Goal state before:
pp: R : Type x
inst✝ : Semiring R
a : Rˣ
b : R
⊢ ↑a + b = ↑a * (1 + ↑a⁻¹ * b)

Tactic:
by
  rw [mul_add, mul_one, ← mul_assoc, Units.mul_inv, one_mul]

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

Goal state before:
pp: k : ℕ
⊢ 2 ∣ k * (k - 1)

Tactic:
rcases k with rfl | k

Goal state after:
case zero
⊢ 2 ∣ 0 * (0 - 1)

case succ
k : ℕ
⊢ 2 ∣ (k + 1) * (k + 1 - 1)
Module: Mathlib.Order.MinMax

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

Tactic:
rw [min_assoc, min_comm b, ← min_assoc]

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 : α
inst✝ : AddLeftMono α
h : a ≤ b
c : α
⊢ c - b ≤ c - a

Tactic:
by
  grw [tsub_le_iff_left, ← h, ← le_add_tsub]

Goal state after:
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:
by rw [tsub_le_iff_left, add_zero]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
rw [← le, mul, mul]; exact mul_le_mul_of_nonneg_left (le.2 hbc) (by rwa [← zero, le])

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ a * b < a * c

Tactic:
by
    rw [← lt, mul, mul]; exact mul_lt_mul_of_pos_left (lt.2 hbc) (by rwa [← zero, lt])

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulRightStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ c * a = b * a ↔ c = b

Tactic:
refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_left (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_left (h.lt_of_ne h') a |>.ne

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

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

Tactic:
by
  rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d ∨ a < a ∨ b < d

Tactic:
left

Goal state after:
case inr.inl
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = a * d
⊢ a = a ∧ b = d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

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

Goal state before:
pp: α : Type u_1
inst✝² : MulZeroClass α
a b : α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b ≤ 0

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

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

Tactic:
by
  suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_left _ ha.le
  apply lt_of_mul_lt_mul_left _ ha.le
  simpa [ha.ne']

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
⊢ Injective fun a' ↦ if a' = a then b else if f a' = b then f a else f a'

Tactic:
intro x y h
    grind

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ (mulRight a).symm = mulRight a⁻¹

Tactic:
ext x
  rfl

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ (mulLeft a).symm = mulLeft a⁻¹

Tactic:
ext x
  rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ (refl α).trans e = e

Tactic:
ext x
  rfl

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ e.trans (refl β) = e

Tactic:
ext x
  rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ |a / c|ₘ = |a / b * (b / c)|ₘ

Tactic:
rw [div_mul_div_cancel]

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 α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
simp [mabs_of_le_one h]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hn : n < 0
⊢ x + ↑n ≤ 0

Tactic:
have := _root_.add_le_add (le_of_abs_le hx) (cast_le_neg_one_of_neg hn)
    rwa [add_neg_cancel] at this

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : unzero ha ≤ ofAdd b
⊢ toAdd (unzero ha) ≤ b

Tactic:
← toAdd_le,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : toAdd (unzero ha) ≤ toAdd (ofAdd b)
⊢ toAdd (unzero ha) ≤ b
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]

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
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

Tactic:
cast_one.symm,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌈a + ↑1⌉₊ = ⌈a⌉₊ + 1
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LT α
inst✝ : WellFoundedGT α
a x✝¹ : α
x✝ : ∀ (y : α), x✝¹ < y → Acc (fun x1 x2 ↦ x2 < x1) y
ih : ∀ (y : α), x✝¹ < y → Acc (fun x1 x2 ↦ x1 > x2) ↑y
⊢ ∀ (y : WithBot α), y > ↑x✝¹ → Acc (fun x1 x2 ↦ x1 > x2) y

Tactic:
by simpa [WithBot.forall]

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✝¹ : LT α
inst✝ : WellFoundedGT α
acc_some : ∀ (a : α), Acc (fun x1 x2 ↦ x1 > x2) ↑a
⊢ ∀ (y : WithBot α), ⊥ < y → Acc (fun x1 x2 ↦ x2 < x1) y

Tactic:
by simpa [WithBot.forall]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered α
⊢ ∀ (a₁ a₂ : WithTop α), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
· simpa [WithTop.exists, WithTop.forall, exists_gt] using DenselyOrdered.dense

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
⊢ DenselyOrdered (WithTop α) ↔ DenselyOrdered α

Tactic:
by
  constructor <;> intro h <;> constructor
  · intro a b hab
    obtain ⟨c, hc⟩ := exists_between (WithTop.coe_lt_coe.mpr hab)
    induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩
  · simpa [WithTop.exists, WithTop.forall, exists_gt] using DenselyOrdered.dense

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

Goal state before:
pp: case inl
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : a ≤ b
⊢ a * b + b * a ≤ a * a + b * b

pp: case inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : b ≤ a
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
· exact mul_add_mul_le_mul_add_mul ‹_› ‹_›

Goal state after:
case inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : b ≤ a
⊢ a * b + b * a ≤ a * a + b * b
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
have : ∀ b ∈ s, a < b → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
by
  simp only [le_antisymm_iff, sq_le_sq]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (s ∪ t) t

Tactic:
exact hc.union_left

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨z, hz, hxz, hyz⟩ := hd x (hst hx) y (hst hy)

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ t
hxz : x ≤ z
hyz : y ≤ z
⊢ ∃ z ∈ s, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ a = c ∧ b = d

Tactic:
obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
⊢ a = c ∧ b = d
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : ℕ → Prop
n : ℕ
inst✝ : DecidablePred p
⊢ (∀ k < n, ¬p k) ↔ n ∈ lowerBounds {n | p n}

Tactic:
by
    simp [mem_lowerBounds, @imp_not_comm _ (p _)]

Goal state after: