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

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

Tactic:
npowRec_add 1 n hn a ha,

Goal state after:
M : Type u
inst✝¹ : One M
inst✝ : Semigroup M
n : ℕ
hn : n ≠ 0
a : M
ha : 1 * a = a
⊢ npowRec 1 a * npowRec n a = a * npowRec n a
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : f ≠ g
⊢ Nontrivial β

Tactic:
rw [ne_eq, funext_iff, Classical.not_forall] at h

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Nontrivial (α → β)
f g : α → β
h : ∃ x, ¬f x = g x
⊢ Nontrivial β
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Type u_1
inst1 inst2 : BEq α
beq1 : α → α → Bool
h : ∀ (x y : α), (x == y) = (x == y)
x y : α
⊢ beq1 x y = (x == y)

Tactic:
exact h x y

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:
by rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
⊢ a < min b c

Tactic:
cases le_total b c

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : b ≤ c
⊢ a < min b c

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h✝ : c ≤ b
⊢ a < min b c
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case zero
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n ≤ f (n + 0)

Tactic:
Nat.add_zero

Goal state after:
case zero
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n ≤ f n
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp.refine_1
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ x.snd

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp.refine_2
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ (a, ⊥).snd ≤ y.snd

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp.refine_3
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ x.fst

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: case mp.refine_4
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ (⊥, b).fst ≤ y.fst

Tactic:
exact bot_le

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

Goal state before:
pp: α : Type u
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
⊢ False

Tactic:
let ⟨y, hy, hya⟩ := H

Goal state after:
α : Type u
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False
Module: Mathlib.Data.Set.Subsingleton

Goal state before:
pp: α : Type u
s : Set α
⊢ (¬∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y

Tactic:
not_forall,

Goal state after:
α : Type u
s : Set α
⊢ (∃ x h x_1 x_2, ¬x = x_1) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y
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✝² : Bot α
inst✝¹ : SDiff α
inst✝ : GeneralizedCoheytingAlgebra β
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_bot : f ⊥ = ⊥
map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b
a : α
⊢ ⊥ ≤ f a

Tactic:
exact bot_le

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✝³ : Bot α
inst✝² : Compl α
inst✝¹ : HImp α
inst✝ : HeytingAlgebra β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
map_compl : ∀ (a : α), f aᶜ = (f a)ᶜ
map_himp : ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
a : α
⊢ ⊥ ≤ f a

Tactic:
exact bot_le

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : x ⊔ y \ x = z ⊔ y \ x
⊢ ⊥ ≤ z ⊓ y \ x

Tactic:
exact bot_le

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)

Tactic:
rw [sup_inf_self, sup_sdiff_left, ← sup_assoc, sup_inf_left, sdiff_sup_self',
            inf_sup_right, sup_comm y, inf_sdiff_sup_right, inf_sup_left x z y]

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

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

Tactic:
rw [← h]
    exact isCompl_compl

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

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

Tactic:
by
  rw [← le_compl_iff_disjoint_left, compl_compl]

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

Goal state before:
pp: case mp
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' u
x_in_v : ⟨x, x_in_s⟩ ∈ Subtype.val ⁻¹' v
⊢ False

Tactic:
exact eq_empty_iff_forall_notMem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ ¬s.pi t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i

Tactic:
rw [← Ne, ← nonempty_iff_ne_empty]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
h : s.pi t₁ ⊆ s.pi t₂
⊢ (s.pi t₁).Nonempty → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case neg
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ cast ⋯
      (match z - 1 - b with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match z - b with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))

Tactic:
rw! [show z - 1 - b = -[(b - z).toNat+1] by lia, show z - b = -[(b - z - 1).toNat+1] by lia]

Goal state after:
case neg
motive : ℤ → Sort u_1
z b : ℤ
zero : motive b
succ : (k : ℤ) → b ≤ k → motive k → motive (k + 1)
pred : (k : ℤ) → k ≤ b → motive k → motive (k - 1)
hz : z ≤ b
h✝ : ¬z = b
⊢ cast ⋯
      (match -[(b - z).toNat+1] with
      | ofNat n => inductionOn'.pos b zero succ n
      | -[n+1] =>
        match n with
        | 0 => pred b ⋯ zero
        | n.succ => cast ⋯ (pred (b + -[n+1]) ⋯ (inductionOn'.neg b zero pred n))) =
    pred z hz
      (cast ⋯
        (match -[(b - z - 1).toNat+1] with
        | ofNat n => inductionOn'.pos b zero succ n
        | -[n+1] => inductionOn'.neg b zero pred n))
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d

Tactic:
Int.mul_ediv_cancel_left _ hb

Goal state after:
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
Module: Mathlib.Data.Int.Init

Goal state before:
pp: a b c : ℤ
ha : 0 < a
hab : a ∣ c - b
⊢ a + b ≤ c ↔ b < c

Tactic:
by
  rw [Int.add_le_iff_le_sub, ← Int.sub_pos, le_iff_pos_of_dvd ha hab]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : IsUnit b
⊢ a * b = 1 * b ↔ a = 1

Tactic:
rw [h.mul_left_inj]

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

Goal state before:
pp: α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
⊢ x = y

Tactic:
ext a b

Goal state after:
α : Type u_7
β : α → Type u_8
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
a : α
b : β a
⊢ (x a) b = (y a) b
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case inr.inr
G₀ : Type u_4
G₀' : Type u_5
inst✝⁴ : GroupWithZero G₀
inst✝³ : GroupWithZero G₀'
inst✝² : MulActionWithZero G₀ G₀'
inst✝¹ : SMulCommClass G₀ G₀' G₀'
inst✝ : IsScalarTower G₀ G₀' G₀'
c : G₀
x : G₀'
hc : c ≠ 0
hx : x ≠ 0
⊢ (c • x)⁻¹ = c⁻¹ • x⁻¹

Tactic:
· refine inv_eq_of_mul_eq_one_left ?_
    rw [smul_mul_smul_comm, inv_mul_cancel₀ hc, inv_mul_cancel₀ hx, one_smul]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ 0 = n

Tactic:
rw [H n]

Goal state after:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
by simp [← Int.natCast_add]

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

Goal state before:
pp: case zero
⊢ IsSquare (sign 0) ↔ 0 ≤ 0

Tactic:
simpa using ⟨0, by simp⟩

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case cons
c : Prop
l : List Prop
IH : ∀ {a b : Prop}, IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: l) → (l.getLastD b → a) → (a :: b :: l).TFAE
a b : Prop
h_chain : IsChain (fun x1 x2 ↦ x1 → x2) (a :: b :: c :: l)
h_last : (c :: l).getLastD b → a
⊢ (a :: b :: c :: l).TFAE

Tactic:
simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *

Goal state after:
case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (b :: l) → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ IsChain (fun x1 x2 ↦ x1 → x2) (c :: l)
h_last : l.getLastD c → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE
Module: Mathlib.Algebra.Group.Semiconj.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ SemiconjBy (↑u) x (↑u * x * ↑u⁻¹)

Tactic:
unfold SemiconjBy; rw [Units.inv_mul_cancel_right]

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

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

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ ↑u * (↑u)⁻¹ʳ = 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

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

Tactic:
rcases h with ⟨u, rfl⟩

Goal state after:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
⊢ (↑u)⁻¹ʳ * ↑u = 1
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (b + c) = a - c - b

Tactic:
tsub_add_eq_tsub_tsub_swap

Goal state after:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - c - b = a - c - b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
by
  rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
rcases h with ha' | hb'

Goal state after:
case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ (n + 1) ≤ a ^ n

Tactic:
rw [← mul_one (a ^ n), pow_succ]

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
n : ℕ
this : ZeroLEOneClass M₀
⊢ a ^ n * a ≤ a ^ n * 1
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
⊢ r = ⇑f ⁻¹'o s

Tactic:
ext a b

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (⇑f ⁻¹'o s) a b
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
h : x < 1
k : ℕ
hn : 0 < k.succ
⊢ x ^ k * x < 1

Tactic:
exact mul_lt_one_of_le_of_lt (pow_le_one_of_le h.le) h

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 1) * a ≤ b ^ n * a * a

Tactic:
pow_le_pow_mul_of_sq_le_mul hab (by lia)

Goal state after:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ (n + 1 - 1) * a * a ≤ b ^ n * a * a
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a|ₘ / |b|ₘ ≤ |a / b|ₘ

Tactic:
apply div_le_iff_le_mul.2

Goal state after:
case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ |a|ₘ ≤ |a / b|ₘ * |b|ₘ
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Mul α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ (∃ c, b = a * c) → a ≤ b

Tactic:
rintro ⟨c, rfl⟩
    exact le_self_mul

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsLeftRegular 0 ↔ Nontrivial R

Tactic:
by
  rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]
  push Not
  exact Iff.rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
x y : WithTop G
⊢ x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
by
  cases x <;> cases y <;> simp [← coe_sub]

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

Goal state before:
pp: case refine_1
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
⊢ Nat.find hₘ + n ≤ m

pp: case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ ≤ Nat.find hₘ + n

Tactic:
· have hnm : n ≤ m := le_trans hn (find_le hpm)
    refine Nat.add_le_of_le_sub hnm (find_le ?_)
    rwa [Nat.sub_add_cancel hnm]

Goal state after:
case refine_2
n : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ ≤ Nat.find hₘ + n
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ∀ (k : ℕ), ↑(n + k) = ↑n
⊢ False

Tactic:
have h : n + (floor (n : α) + 1) ≤ floor (n : α) := (gc_floor (natCast_nonneg n)).mpr (hn _).le

Goal state after:
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ∀ (k : ℕ), ↑(n + k) = ↑n
h : n + (floor ↑n + 1) ≤ floor ↑n
⊢ False
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
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:
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ |a| ≤ |b|

Tactic:
← sq_le_sq

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
h : a ^ 2 ≤ b ^ 2
hb : 0 ≤ b
⊢ a ^ 2 ≤ b ^ 2
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Tactic:
image2_swap g,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun a b ↦ g b a) t s) u = image2 g' (image2 f' s u) t
Module: Mathlib.Order.BoundedOrder.Monotone

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : Preorder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p

Tactic:
exact bot_le

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (Icc a b).Nontrivial

Tactic:
exact ⟨a, ⟨le_refl _, h.le⟩, b, ⟨h.le, le_refl _⟩, h.ne⟩

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

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

Tactic:
obtain h | h := directedOn_or_directedOn_of_union h
  · obtain rfl | hs := s.eq_empty_or_nonempty
    · aesop
    · exact .inl ⟨h, hs⟩
  · obtain rfl | ht := t.eq_empty_or_nonempty
    · aesop
    · exact .inr ⟨h, ht⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ (¬∀ x ∈ s, x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ (∃ x, ∃ (_ : x ∈ s), ¬x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x : List α
n : ℕ
⊢ x = take n x ↔ x.length ≤ n

Tactic:
Eq.comm,

Goal state after:
α : Type u
x : List α
n : ℕ
⊢ take n x = x ↔ x.length ≤ n
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹

Tactic:
convert (one_div a).le.trans (inv_anti₀ zero_lt_two a2)

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
x : α
y : β
hx : (x, y) ∈ (a✝ :: l₁✝).zip (b✝ :: l₂✝)
⊢ R x y

Tactic:
by
    rw [zip, zipWith, mem_cons] at hx
    match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃

Goal state after:
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
insertIdx_of_length_lt hn

Goal state after:
case inl
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
l₁ : List α
hl1 : Forall₂ R l₁ []
⊢ SublistForall₂ R [] []

Tactic:
exact SublistForall₂.nil

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)

Tactic:
exact SublistForall₂.nil

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ [] (head✝ :: tail✝)

Tactic:
exact SublistForall₂.nil

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

Goal state before:
pp: α : Type u
a : α
L : List α
⊢ L ⊆ [a] ↔ ∃ n, L = replicate n a

Tactic:
simp only [eq_replicate_iff, subset_def, mem_singleton, exists_eq_left']

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ (if b = true then mkRat (↑(OfNat.ofNat m)) (10 ^ OfNat.ofNat d) else ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d)) =
    ↑(m * 10 ^ d)

Tactic:
if_neg ‹_›

Goal state after:
case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑(OfNat.ofNat m * 10 ^ OfNat.ofNat d) = ↑(m * 10 ^ d)
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y x ↔ SemiconjBy a x y

Tactic:
by
  simp_rw [SemiconjBy, eq_mul_inv_iff_mul_eq, mul_assoc, inv_mul_eq_iff_eq_mul, eq_comm]

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₃ : R
a₁ a₃ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b₁ b₂ : R
a₁ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b₁ b₃ : R
a₁ a₃ : ℤ
a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
b₁ b₂ : R
a₁ a₂ : ℤ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₂ = b₂
⊢ ↑(a₁ + a₂) = b₁ + b₂

Tactic:
subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a b : R
x✝ : -1 * a = b
⊢ -a = b

Tactic:
subst_vars; simp

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ : R
a₂ : ℕ
a₃ b : R
x✝ : -a₃ = b
⊢ -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b

Tactic:
subst_vars; simp

Goal state after: