mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k✝ : ℕ
m : M
k : ℕ
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m

Tactic:
rw [npowBinRec.go_spec, npowRec_eq]

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

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * (b * a) = b

Tactic:
rw [mul_comm, mul_inv_cancel_right]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b

Tactic:
rw [exists_prop]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a b : α
⊢ (∃ h, a ≠ b) ↔ P ∧ a ≠ b

Tactic:
rw [exists_prop]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
hf : Injective f
hg : Injective g
r : α → β → Prop
a : α
b : β
⊢ Relation.Map r f g (f a) (g b) ↔ r a b

Tactic:
by simp [Relation.Map, hf.eq_iff, hg.eq_iff]

Goal state after:
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) → InvolutiveInv (f i)
⊢ ∀ (x : (i : I) → f i), x⁻¹⁻¹ = x

Tactic:
intros; ext; exact inv_inv _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
⊢ ∀ {a b : α × β}, Prod.Lex r s a b ∨ a = b ∨ Prod.Lex r s b a

Tactic:
intro ⟨i, a⟩ ⟨j, b⟩
    obtain hij | rfl | hji := trichotomous_of r i j
    { exact Or.inl (Lex.left _ _ hij) }
    { exact (trichotomous_of (s) a b).imp3 (Lex.right _) (congr_arg _) (Lex.right _) }
    { exact Or.inr (Or.inr <| Lex.left _ _ hji) }

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

Goal state before:
pp: α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤

Tactic:
cases PartialOrder.ext H

Goal state after:
case refl
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ ⊤ = ⊤
Module: Mathlib.Order.BoundedOrder.Basic

Goal state before:
pp: α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥

Tactic:
← coe_bot hbot,

Goal state after:
α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ↑⊥ ↔ x = ⊥
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
⊢ ∀ (a' : α), a' ≤ a → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)

Tactic:
a'

Goal state after:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a a' : α
⊢ a' ≤ a → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictAntiOn f s

Tactic:
rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
by
  let : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf Pinf
  let : OrderBot (Subtype pr) := Subtype.orderBot hbot
  rw [disjoint_iff, disjoint_iff, ← Subtype.coe_inf Pinf, ← Subtype.coe_bot hbot]
  exact Subtype.coe_inj.symm

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: case mk.mk
α : Type u_1
toPartialOrder✝¹ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
toPartialOrder✝ : PartialOrder α
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toPartialOrder := toPartialOrder✝¹, sup := sup✝¹, le_sup_left := le_sup_left✝¹, le_sup_right := le_sup_right✝¹,
      sup_le := sup_le✝¹ } =
    { toPartialOrder := toPartialOrder✝, sup := sup✝, le_sup_left := le_sup_left✝, le_sup_right := le_sup_right✝,
      sup_le := sup_le✝ }

Tactic:
cases PartialOrder.ext H

Goal state after:
case mk.mk.refl
α : Type u_1
toPartialOrder✝ : PartialOrder α
sup✝¹ : α → α → α
le_sup_left✝¹ : ∀ (a b : α), a ≤ sup✝¹ a b
le_sup_right✝¹ : ∀ (a b : α), b ≤ sup✝¹ a b
sup_le✝¹ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝¹ a b ≤ c
sup✝ : α → α → α
le_sup_left✝ : ∀ (a b : α), a ≤ sup✝ a b
le_sup_right✝ : ∀ (a b : α), b ≤ sup✝ a b
sup_le✝ : ∀ (a b c : α), a ≤ c → b ≤ c → sup✝ a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ { toPartialOrder := toPartialOrder✝, sup := sup✝¹, le_sup_left := le_sup_left✝¹, le_sup_right := le_sup_right✝¹,
      sup_le := sup_le✝¹ } =
    {
      toPartialOrder :=
        { toPartialOrder := toPartialOrder✝, sup := sup✝¹, le_sup_left := le_sup_left✝¹, le_sup_right := le_sup_right✝¹,
            sup_le := sup_le✝¹ }.toPartialOrder,
      sup := sup✝, le_sup_left := le_sup_left✝, le_sup_right := le_sup_right✝, sup_le := sup_le✝ }
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : c < f N
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b

Tactic:
replace hN : f N = c + 1 := by specialize hc N; lia

Goal state after:
case neg
f : ℕ → ℕ
mono_f : Monotone f
c : ℕ
ih : (∀ (n : ℕ), f n ≤ c) → ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
hc : ∀ (n : ℕ), f n ≤ c + 1
N : ℕ
hN : f N = c + 1
⊢ ∃ b N, ∀ (n : ℕ), n ≥ N → f n = b
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) = none
hn : e none = none
⊢ False

Tactic:
← hn

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : Option α ≃ Option β
x : α
h : e (some x) = e none
hn : e none = none
⊢ False
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:
by
    rw [← le, map_top]
    exact le_top

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := e.lattice
top : Top α := e.top
himp : HImp α := e.himp
⊢ GeneralizedHeytingAlgebra α

Tactic:
apply e.injective.generalizedHeytingAlgebra

Goal state after:
case le
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ {x y : α}, e x ≤ e y ↔ x ≤ y

case lt
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ {x y : α}, e x < e y ↔ x < y

case map_sup
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⊔ b) = e a ⊔ e b

case map_inf
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⊓ b) = e a ⊓ e b

case map_top
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ e ⊤ = ⊤

case map_himp
ι : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : GeneralizedHeytingAlgebra β
lattice : Lattice α := ⋯
top : Top α := ⋯
himp : HImp α := ⋯
⊢ ∀ (a b : α), e (a ⇨ b) = e a ⇨ e b
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ = y ↔ yᶜ = x

Tactic:
by
  rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x = yᶜ ↔ y = xᶜ

Tactic:
by
  rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
p : α → Prop
q : Subtype p → Prop
a : Subtype q
⊢ q ⟨↑↑a, ⋯⟩

Tactic:
rcases a with ⟨⟨a, hap⟩, haq⟩
      exact haq

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s \ t)

Tactic:
union_sdiff_self

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = f '' univ \ f '' s

Tactic:
← image_sdiff hf,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = f '' (univ \ s)
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a

Tactic:
simp only [mem_powerset_iff]

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

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

Tactic:
refine subset_antisymm (subset_sdiff.2 ⟨image_mono sdiff_subset, ?_⟩)
    (sdiff_subset_iff.2 (by rw [← image_union, inter_union_sdiff]))
  exact Disjoint.image disjoint_sdiff_inter h sdiff_subset inter_subset_left

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ (f '' s₁ ∩ t') \ t

Tactic:
union_sdiff_self

Goal state after:
case refine_4
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ t ∪ f '' s₁ ∩ t'
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
eq_div_iff_mul_eq',

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
hab : a * b = 1
inv_val✝ : b * a = 1
⊢ ∃ b_1, ↑{ val := a, inv := b, val_inv := hab, inv_val := inv_val✝ } * b_1 = 1

Tactic:
exact ⟨b, hab⟩

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

Goal state before:
pp: α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| 1 * (a * b)

Tactic:
← hc,

Goal state after:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
| c * b * (a * b)
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = ↑0 ↔ n = 0

Tactic:
cast_inj

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ n = 0 ↔ n = 0
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = ↑1 ↔ n = 1

Tactic:
cast_inj

Goal state after:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ n = 1 ↔ n = 1
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • y - b • x + x

Tactic:
Convex.combo_self h

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + x = b • y - b • x + x
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ a * b = c

Tactic:
rwa [← eq_mul_inv_iff_mul_eq₀]

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ b ≠ 0
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = ↑1 ↔ n = 1

Tactic:
cast_inj

Goal state after:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ n = 1 ↔ n = 1
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * b * c ≤ a * b * d

Tactic:
by rw [mul_assoc, mul_assoc]; exact mul_le_mul_right hcd _

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

Goal state before:
pp: α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
⊢ ∃ a, 1 < a

Tactic:
obtain h | h := hy.lt_or_gt

Goal state after:
case inl
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ a, 1 < a

case inr
α : Type u
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ a, 1 < a
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddMonoidWithOne R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono R
n : ℕ
⊢ ↑n < ↑(n + 1)

Tactic:
rw [Nat.cast_succ]; apply lt_add_one

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
c : α
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
hc : c ≠ a
hb : f c ≠ b
⊢ (f.setValue a b) c = f c

Tactic:
by
  simp [setValue, hc, 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 b : G₀
ha : 0 < a
⊢ a⁻¹ * b ≤ 1 ↔ b ≤ a

Tactic:
inv_mul_le_iff₀ ha,

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ b ≤ a * 1 ↔ b ≤ 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 : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← inv_mul_le_iff₀ ha, mul_one]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
by
  iterate 3 rw [mul_nonneg_iff]
  have or_a := le_total 0 a
  have or_b := le_total 0 b
  have or_c := le_total 0 c
  aesop

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

Goal state before:
pp: case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

Tactic:
exact RelHomClass.wellFounded (Quotient.mkRelHom H)

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

Goal state before:
pp: case inl
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 : d ≤ b
⊢ |b / d|ₘ ≤ max (c / d) (d / a)

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_one_le <| one_le_div'.mpr h]
    exact le_max_of_le_left <| div_le_div_right' hcd _

Goal state after:
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)
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ r % k % k = r % k

Tactic:
mod_mod

Goal state after:
case right
k n r : ℕ
hkn : n.Coprime k
hk✝ : k ≠ 0
hk : 1 < k
m : ℕ
hm : n * m % k = 1
⊢ r % k = r % k
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: k n r : ℕ
hkn : n.Coprime k
hk : k ≠ 0
⊢ ∃ m, m < k ∧ n * m % k = r % k

Tactic:
by
  obtain rfl | hk : k = 1 ∨ 1 < k := by lia
  · simp [mod_one]
  obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hkn hk
  use (m * r) % k, mod_lt _ (by lia)
  rw [mul_mod, mod_mod, ← mul_mod, ← mul_assoc, mul_mod, hm, one_mul, mod_mod]

Goal state after:
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
hb : ¬0 ≤ b
⊢ False

Tactic:
replace hb : b ≤ -1 := by lia

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
hb : b ≤ -1
⊢ False
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n) → IsLeftRegular a

Tactic:
← Nat.succ_pred_eq_of_pos n0,

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsLeftRegular (a ^ n.pred.succ) → IsLeftRegular a
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a

Tactic:
← Nat.succ_pred_eq_of_pos n0,

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n.pred.succ) → IsRightRegular a
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a = b

Tactic:
exact left_neg_eq_right_neg (a := a) (by simp [neg_add_cancel_of_ne_top, *]) h

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊤
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using le_of_add_le_add_left

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a - (a - b) = min a b

Tactic:
tsub_eq_tsub_min _ b,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
⊢ a - (a - min a b) = min a b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
hx : x ≠ ⊥
⊢ x + y ≤ x + z → y ≤ z

Tactic:
lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using le_of_add_le_add_left

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
⊢ 0 < ⌈a⌉₊ ↔ 0 < a

Tactic:
rw [lt_ceil, cast_zero]

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
⊢ 0 < ⌈a⌉ ↔ 0 < a

Tactic:
rw [lt_ceil, cast_zero]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x.log ≤ y.log ↔ x ≤ y

Tactic:
log_le_iff_le_exp hx,

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≤ exp y.log ↔ x ≤ y
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → f a = f b

Tactic:
rintro a ha b hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a = f b
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u : ℤˣ
⊢ (↑u⁻¹).natAbs * (↑u).natAbs = 1

Tactic:
rw [← natAbs_mul, Units.inv_mul]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n : ℕ
inst✝ : IsOrderedRing α
⊢ |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n

Tactic:
induction n with | zero => simp [geomSum] | succ n ih => ?_
  refine (abs_add_le ..).trans ?_
  rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]
  refine add_le_add ?_ (pow_le_pow_left₀ (abs_nonneg _) le_sup_right _)
  rw [pow_succ, ← mul_assoc, mul_comm |a|]
  gcongr
  exacts [abs_nonneg _, (abs_nonneg _).trans ih, le_sup_left]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : g a < f a
⊢ f a = g a

Tactic:
← hc,

Goal state after:
case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : f c < f a
⊢ f a = g a
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑(s ∪ t \ s) ⊕ ↑(s ∩ t)

Tactic:
union_sdiff_self

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑(s ∪ t) ⊕ ↑(s ∩ t)
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
hst : IsCofinalFor s t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
exact .inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩

Goal state after: