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

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
⊢ IsMulCommutative M ↔ ∀ (a b : M), a * b = b * a

Tactic:
grind [IsMulCommutative, Std.Commutative]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ b * a * a⁻¹ = c

Tactic:
show b * a = c * a from h,

Goal state after:
G : Type u_1
inst✝ : Group G
a✝ b✝ a b c : G
h : (fun x ↦ x * a) b = (fun x ↦ x * a) c
⊢ c * a * a⁻¹ = c
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝ : Nontrivial α
b : β
a₁ a₂ : α
h : a₁ ≠ a₂
⊢ ∃ a b_1, b = b ∧ a ≠ b_1

Tactic:
exact ⟨a₁, a₂, rfl, h⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
γ : Sort u_6
f : α → β
g : β → Option α
h : β → γ
i : γ → Option β
hf : IsPartialInv f g
hh : IsPartialInv h i
⊢ IsPartialInv (h ∘ f) fun x ↦ (i x).bind g

Tactic:
intros a b
  simp [Option.bind_eq_some_iff, hh _, hf _]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
e' : β → γ
b : β
hb : ¬∃ a, f a = b
⊢ extend f g e' b = e' b

Tactic:
classical
  simp [Function.extend_def, hb]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : Monoid P
inst✝³ : MulAction P Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
q : Q
⊢ (m • n) • q = m • n • q

Tactic:
rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
⊢ a < b

Tactic:
by
  inhabit ι
  exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

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

Goal state before:
pp: m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction of_succ self ⋯ = of_succ m smn (decreasingInduction of_succ self smn)

Tactic:
decreasingInduction_trans (n := m + 1) (Nat.le_succ m),

Goal state after:
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ decreasingInduction (fun x x_1 ↦ of_succ x ⋯) (decreasingInduction of_succ self ?hnk) ⋯ =
    of_succ m smn (decreasingInduction of_succ self smn)

case hnk
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
⊢ m + 1 ≤ n
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
hx : ¬p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
simpa [hx, hy] using hg h

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

Goal state before:
pp: case succ
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
ihn : r (f a) (f (a + ↑n.succ))
⊢ r (f a) (f (a + ↑(n + 1).succ))

Tactic:
rw [Int.natCast_succ, ← Int.add_assoc]; exact _root_.trans ihn (h _)

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

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

Tactic:
simp only [subset_def, not_forall, exists_prop]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ (s = ∅ ∨ ∃ x, s = {x}) → s.Subsingleton

Tactic:
rintro (_ | ⟨_, rfl⟩) <;> simp_all

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

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

Tactic:
by
  rw [← sup_sdiff_left_self, ← @sup_sdiff_left_self _ _ _ b]
  exact sdiff_le_sdiff_right h

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

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.14
β : Type ?u.13
p : α ⊕ β → Prop
⊢ LeftInverse
    (fun x ↦
      match x with
      | inl a => ⟨inl ↑a, ⋯⟩
      | inr b => ⟨inr ↑b, ⋯⟩)
    fun x ↦
    match x with
    | ⟨inl a, h⟩ => inl ⟨a, h⟩
    | ⟨inr b, h⟩ => inr ⟨b, h⟩

Tactic:
rintro ⟨a | b, h⟩

Goal state after:
case inl
α✝ : 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.14
β : Type ?u.13
p : α ⊕ β → Prop
a : α
h : p (inl a)
⊢ (fun x ↦
        match x with
        | inl a => ⟨inl ↑a, ⋯⟩
        | inr b => ⟨inr ↑b, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨inl a, h⟩ => inl ⟨a, h⟩
          | ⟨inr b, h⟩ => inr ⟨b, h⟩)
        ⟨inl a, h⟩) =
    ⟨inl a, h⟩

case inr
α✝ : 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.14
β : Type ?u.13
p : α ⊕ β → Prop
b : β
h : p (inr b)
⊢ (fun x ↦
        match x with
        | inl a => ⟨inl ↑a, ⋯⟩
        | inr b => ⟨inr ↑b, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨inl a, h⟩ => inl ⟨a, h⟩
          | ⟨inr b, h⟩ => inr ⟨b, h⟩)
        ⟨inr b, h⟩) =
    ⟨inr b, h⟩
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: case inr
α✝ : 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.17
β : Type ?u.16
inst✝ : IsEmpty β
x : β
⊢ inl (Sum.elim id (fun a ↦ isEmptyElim a) (inr x)) = inr x

Tactic:
· exact isEmptyElim x

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

Goal state before:
pp: α : Type u
x : α
inst✝¹ : BooleanAlgebra α
inst✝ : Nontrivial α
⊢ xᶜ < x ↔ x = ⊤

Tactic:
simpa using lt_compl_self (a := xᶜ)

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
by
  simp_rw [inf_comm _ c, inf_symmDiff_distrib_left]

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

Goal state before:
pp: α : Sort u_1
inst✝ : DecidableEq α
a c d : α
h : (fun x ↦ swap a x) c = (fun x ↦ swap a x) d
⊢ c = d

Tactic:
simp only at h
  rw [← Equiv.swap_apply_left a c, h, Equiv.swap_apply_left]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (Membership.mem ∘ preimage f) ↔ Surjective f

Tactic:
← Injective.of_comp_iff' _ Set.ofPred_bijective

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective ((Membership.mem ∘ preimage f) ∘ ofPred) ↔ Surjective f
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬(s = ∅ ∨ t = ∅)

Tactic:
← Set.prod_eq_empty_iff

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ ¬s ×ˢ t = ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t → s = t

pp: case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t

Tactic:
· intro h
    apply Subset.antisymm
    · rw [← preimage_subset_preimage_iff hs, h]
    · rw [← preimage_subset_preimage_iff ht, h]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ range f ∪ s ∩ range g)

Tactic:
← inter_union_distrib_left,

Goal state after:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = h '' (s ∩ (range f ∪ range g))
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
f : OneHom N P
⊢ f.comp 1 = 1

Tactic:
ext
  simp only [map_one, OneHom.coe_comp, Function.comp_apply, OneHom.one_apply]

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

Goal state before:
pp: case refine_3
α : 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)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t

Tactic:
← h.image_eq

Goal state after:
case refine_3
α : 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)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by rw [mul_eq_one_iff_eq_inv, inv_inj]

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

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

Tactic:
by rw [Units.mul_inv, mul_one]

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

Goal state before:
pp: M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1

Tactic:
exact zero_ne_one

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬0 = 1

Tactic:
exact zero_ne_one

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑(match n✝ + 1 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
cast_negSucc,

Goal state after:
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ -↑(n✝ + 1) = ↑m - ↑n
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m - ↑n.succ = ↑m + ↑-[n+1]

Tactic:
cast_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m - ↑n.succ = ↑m + -↑(n + 1)
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n - ↑m.succ = ↑-[m+1] + ↑n

Tactic:
cast_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑n - ↑m.succ = -↑(m + 1) + ↑n
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑-[m + n + 1+1] = ↑-[m+1] + ↑-[n+1]

Tactic:
cast_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = ↑-[m+1] + ↑-[n+1]
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = ↑-[m+1] + ↑-[n+1]

Tactic:
cast_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = -↑(m + 1) + ↑-[n+1]
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = -↑(m + 1) + ↑-[n+1]

Tactic:
cast_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ -↑(m + n + 1 + 1) = -↑(m + 1) + -↑(n + 1)
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: a n : ℕ
h : a ≤ n + n
⊢ (n ^ 2 + a).sqrt = n

Tactic:
simpa [Nat.pow_two] using sqrt_add_eq n h

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

Goal state before:
pp: case zero
A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ f 0 = g 0

Tactic:
simp_rw [map_zero f, map_zero g]

Goal state after:
Module: Mathlib.Data.Int.Cast.Lemmas

Goal state before:
pp: case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0

Tactic:
cast_negSucc,

Goal state after:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : -↑(a✝ + 1) = 0
⊢ -[a✝+1] = 0
Module: Mathlib.Algebra.Order.Monoid.Defs

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

Tactic:
rw [add_comm c, add_comm c]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ a + c ≤ b + c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a / a ≤ 1

Tactic:
by obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : Preorder G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
⊢ a⁻¹ * a ≤ 1

Tactic:
by obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
disjoint_iff_inf_le,

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ f a ⊓ f 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
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ (k + 1) ≤ b ^ (k + 1)

Tactic:
rw [pow_succ, pow_succ]
    exact mul_le_mul' (pow_le_pow_left' hab k) hab

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 : G
⊢ |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b

Tactic:
by rw [mabs_le', and_comm, inv_le']

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 : G
⊢ |a|ₘ ≤ |b|ₘ * |b * a|ₘ

Tactic:
by simpa using mabs_mul_le b⁻¹ (b * a)

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

Goal state before:
pp: k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k) % ↑k).toNat = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k

Tactic:
← Int.natCast_mod,

Goal state after:
k n : ℕ
hk : n.gcd k < k
hk' : ↑k ≠ 0
key : (↑(n.gcd k % k)).toNat = (↑n * n.gcdA k % ↑k).toNat
⊢ ∃ m, m < k ∧ n * m % k = n.gcd k
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n.natAbs = ↑|n|

Tactic:
rw [← natCast_natAbs, Int.cast_natCast]

Goal state after:
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:
by rw [← Nat.succ_pred_eq_of_pos n0, pow_succ']; exact .of_mul

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ IsAddUnit a → a ≠ ⊤

Tactic:
by rintro ⟨⟨b, c, hbc, -⟩, rfl⟩ rfl; simp [LinearOrderedAddCommGroupWithTop.top_add'] at hbc

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
by
  obtain rfl | hb := eq_or_ne b ⊤
  · simp
  · simp [← sub_self_eq_zero_of_ne_top hb, hb]

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

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

Tactic:
← hc.add_tsub_assoc_of_le hcb,

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
hcb : c ≤ b
⊢ a + c + b - c = a + b
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - min a b

Tactic:
min_eq_right h

Goal state after:
case inr
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - b
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
hf : Monotone ⇑f
⊢ Monotone ⇑(map' f)

Tactic:
by simpa [Monotone, WithZero.forall]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

Tactic:
· obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

pp: case inr.inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Tactic:
· use e i
    simp [Function.extend_apply' _ _ _ hb]

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)
Module: Mathlib.Order.Directed

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

Tactic:
rw [Set.pair_comm]

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

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

Tactic:
by
  rw [← mul_right_inj_of_invertible (c := ⅟c), invOf_mul_cancel_left]

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

Goal state before:
pp: case refine_1
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = 1 ∧ v = 1
⊢ u * v = 1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Goal state after:
case refine_1
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_2
u v : ℤ
h : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
H : u = -1 ∧ v = -1
⊢ u * v = 1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Goal state after:
case refine_2
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_1
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = 1 ∧ v = -1
⊢ u * v = -1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Goal state after:
case refine_1
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case refine_2
u v : ℤ
h : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1
H : u = -1 ∧ v = 1
⊢ u * v = -1

Tactic:
obtain ⟨rfl, rfl⟩ := H

Goal state after:
case refine_2
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ image2 f s (t ∩ t') = image2 f s t ∩ image2 f s t'

Tactic:
by
  simp_rw [← image_uncurry_prod, prod_inter, image_inter hf.uncurry]

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

Goal state before:
pp: α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove (range fun i ↦ F i a)

Tactic:
simp only [bddAbove_pi, ← range_comp]

Goal state after:
α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ (∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i ↦ F i a)
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
⊢ Acc r y

Tactic:
by_contra hy'

Goal state after:
α : Type u_1
r : α → α → Prop
h : ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m
x : α
hx : ¬Acc r x
m : α
hm : m ∈ {x | ¬Acc r x}
hm' : ∀ (x : α), x ∈ {x | ¬Acc r x} → ¬r x m
y : α
hy : r y m
hy' : ¬Acc r y
⊢ False
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h : p i then update v j x (e ⟨i, h⟩) else w i) =
    update (fun i ↦ if h : p i then v (e ⟨i, h⟩) else w i) (↑(EquivLike.inv e j)) x i

Tactic:
simp only [h, update_apply]

Goal state after:
case pos
α : Type u_1
E : Type u_2
β : Sort u_3
γ : Sort u_4
p : α → Prop
inst✝³ : EquivLike E { x // p x } β
e : E
v : β → γ
w : α → γ
j : β
x : γ
inst✝² : DecidableEq β
inst✝¹ : DecidableEq α
inst✝ : (j : α) → Decidable (p j)
i : α
h : p i
⊢ (if h_1 : True then if e ⟨i, ⋯⟩ = j then x else v (e ⟨i, ⋯⟩) else w i) =
    if i = ↑(EquivLike.inv e j) then x else if h_1 : True then v (e ⟨i, ⋯⟩) else w i
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
f g : α ≃o β
⊢ f.symm.symm = g.symm.symm

Tactic:
Subsingleton.elim f.symm

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
f g : α ≃o β
⊢ symm ?m.34 = g.symm.symm

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : WellFoundedLT β
inst✝ : Preorder α
f g : α ≃o β
⊢ β ≃o α