mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Nontrivial.Defs

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

Tactic:
by
  obtain ⟨f, g, h⟩ := exists_pair_ne (α → β)
  rw [ne_eq, funext_iff, Classical.not_forall] at h
  obtain ⟨a, h⟩ := h
  exact nontrivial_of_ne _ _ h

Goal state after:
Module: Mathlib.Logic.Nontrivial.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
⊢ Nontrivial α

Tactic:
rcases hf y with ⟨y', hy'⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Nontrivial β
f : α → β
hf : Surjective f
x y : β
h : x ≠ y
x' : α
hx' : f x' = x
y' : α
hy' : f y' = y
⊢ Nontrivial α
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
b a : α
motive : (a_1 : α) → ReflTransGen r a_1 a → Prop
refl : motive a ⋯
head : ∀ {a_1 c : α} (h' : r a_1 c) (h : ReflTransGen r c a), motive c h → motive a_1 ⋯
⊢ motive a ⋯

Tactic:
exact refl

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_3
r : α → α → Prop
iseqv✝¹ : Equivalence r
p : α → α → Prop
iseqv✝ : Equivalence p
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := p, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }

Tactic:
have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
     subst this
     rfl

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

Goal state before:
pp: α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ RightTotal R ↔ IsEmpty β

Tactic:
by
  simp only [RightTotal, IsEmpty.exists_iff, isEmpty_iff]

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

Goal state before:
pp: case a
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) b

Tactic:
have : a + 1 = b ∨ a + 1 < b := by lia
      rcases this with (rfl | h)
      · exact ha _
      apply diag_induction P ha hb hd (a + 1) b h

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases yx : y ≤ x

Goal state after:
case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x
Module: Mathlib.Order.Compare

Goal state before:
pp: case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x

Tactic:
by_cases yx : y ≤ x

Goal state after:
case pos
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x

case neg
α : Type u_3
inst✝² : LE α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x
Module: Mathlib.Order.Compare

Goal state before:
pp: case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
⊢ cmpLE x y = cmp x y

Tactic:
by_cases yx : y ≤ x

Goal state after:
case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
Module: Mathlib.Order.Compare

Goal state before:
pp: case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
⊢ cmpLE x y = cmp x y

Tactic:
by_cases yx : y ≤ x

Goal state after:
case pos
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : y ≤ x
⊢ cmpLE x y = cmp x y

case neg
α : Type u_3
inst✝³ : Preorder α
inst✝² : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝¹ : DecidableLE α
inst✝ : DecidableLT α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ cmpLE x y = cmp x y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁

Tactic:
exact h_anti h₁

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : DecidableLE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
⊢ (fun x1 x2 ↦ x1 ⊔ x2) = maxDefault

Tactic:
by
  ext x y
  unfold maxDefault
  split_ifs with h'
  exacts [sup_of_le_right h', sup_of_le_left <| (total_of (· ≤ ·) x y).resolve_left h']

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

Goal state before:
pp: case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
h2 : e (some x) = none
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_none _ h1]

Goal state after:
case none.none
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
h2 : e (some x) = none
⊢ e.symm none = some x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : β
hxt : x✝ ∈ t
x : α
hxs : x ∈ s
⊢ f x = f' x

Tactic:
have h' := h <| mk_mem_prod hxs hxt

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : β
hxt : x✝ ∈ t
x : α
hxs : x ∈ s
h' : Prod.map f g (x, x✝) = Prod.map f' g' (x, x✝)
⊢ f x = f' x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : α
hxs : x✝ ∈ s
x : β
hxt : x ∈ t
⊢ g x = g' x

Tactic:
have h' := h <| mk_mem_prod hxs hxt

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f f' : α → γ
g g' : β → δ
h : EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
x✝ : α
hxs : x✝ ∈ s
x : β
hxt : x ∈ t
h' : Prod.map f g (x✝, x) = Prod.map f' g' (x✝, x)
⊢ g x = g' x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ {x | x i ∈ s} ∩ univ = eval i ⁻¹' s

Tactic:
inter_univ,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ {x | x i ∈ s} = eval i ⁻¹' s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Disjoint s (range f)
⊢ f ⁻¹' s = ∅

Tactic:
by
  simpa using h.preimage f

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

Goal state before:
pp: case refine_2.inr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update f i x j ∈ t j

Tactic:
rw [update_of_ne h]
      exact hf j hj h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : N
⊢ g (x * y) = g (f (g x) * f (g y))

Tactic:
h₂ x,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
G : Type u_7
H : Type u_8
F : Type u_9
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
g : N → M
h₁ : LeftInverse g ⇑f
h₂ : RightInverse g ⇑f
x y : N
⊢ g (x * y) = g (x * f (g y))
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : IsMulCommutative M
a b : N
⊢ a * b = b * a

Tactic:
have ⟨a', ha'⟩ := is_surj a

Goal state after:
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : IsMulCommutative M
a b : N
a' : M
ha' : f a' = a
⊢ a * b = b * a
Module: Mathlib.Data.Set.Function

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

Tactic:
by
  rw [hf.image_inter']
  refine Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))
  rintro _ ⟨h₁, x, hx, rfl⟩; exact ⟨⟨h₁, by rwa [hf hx]⟩, mem_image_of_mem _ hx⟩

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ g ⁻¹' s → x ∈ f '' s

Tactic:
intro hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
⊢ x ∈ f '' s
Module: Mathlib.Algebra.Group.Torsion

Goal state before:
pp: case inl
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
a : M
⊢ a ^ 0 = 1 ↔ a = 1 ∨ 0 = 0

Tactic:
simp [pow_eq_one_iff_left, *]

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

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsMulTorsionFree M
n : ℕ
a : M
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ n = 0

Tactic:
simp [pow_eq_one_iff_left, *]

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

Goal state before:
pp: a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((- -[m+1] - 1) / (↑n + 1) + 1)

Tactic:
show (- -[m+1] : ℤ) = (m + 1 : ℤ) by rfl

Goal state after:
a b : ℤ
m n : ℕ
Ha : -[m+1] < 0
Hb : 0 < ↑n + 1
⊢ -[m+1].ediv (↑n + 1) = -((↑m + 1 - 1) / (↑n + 1) + 1)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)

Goal state after:
case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ

case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)

Goal state after:
case inl
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s

case inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a / (b * a) = b⁻¹

Tactic:
by rw [← inv_div, mul_div_cancel_right]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
← zpow_add,

Goal state after:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m + n) = a ^ n * a ^ m
Module: Mathlib.Algebra.Group.Units.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
h : Bijective fun x ↦ a * x
⊢ (fun x ↦ a * x) (⋯.choose * a) = (fun x ↦ a * x) 1

Tactic:
by simpa [mul_assoc] using congr_arg (· * a) (h.2 1).choose_spec

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

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0

Tactic:
exact ha.elim ih id

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

Goal state before:
pp: α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ -(0 * 0) = 0 * 0

Tactic:
← neg_mul,

Goal state after:
α : Type u
R : Type v
inst✝¹ : MulZeroClass α
inst✝ : HasDistribNeg α
⊢ -0 * 0 = 0 * 0
Module: Mathlib.Algebra.Group.Semiconj.Units

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

Tactic:
by rw [Units.inv_mul_cancel_left]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)

Tactic:
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y

Tactic:
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

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

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

Tactic:
grw [← le_add_tsub]

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

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

Tactic:
by grw [← le_add_tsub]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a * b⁻¹ * b ≤ c * b ↔ a ≤ c * b

Tactic:
by rw [inv_mul_cancel_right]

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ c * b ≤ a * b⁻¹ * b ↔ c * b ≤ a

Tactic:
by rw [inv_mul_cancel_right]

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 : α
⊢ c * b < a * b⁻¹ * b ↔ c * b < a

Tactic:
by rw [inv_mul_cancel_right]

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

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

Tactic:
intro ab nab

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

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

Tactic:
exact mul_neg_of_pos_of_neg ha (ab ha.le)

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₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : 0 ≤ n
⊢ a ^ n ≤ 1

Tactic:
by
  simpa using zpow_right_anti₀ ha₀ ha₁ hn

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₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : n ≤ 0
⊢ 1 ≤ a ^ n

Tactic:
by
  simpa using zpow_right_anti₀ ha₀ ha₁ hn

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a b : α
⊢ r a b ↔ (⇑f ⁻¹'o s) a b

Tactic:
exact f.map_rel_iff.symm

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

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ -(a * b) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
← neg_mul,

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ 0 ≤ -a * b ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ y

Tactic:
← f.apply_symm_apply y,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : PartialOrder β
f : α ≃o β
x : α
y : β
hx : ∀ (x' : α), x ≤ x'
hy : ∀ (y' : β), y ≤ y'
⊢ f x ≤ f (f.symm y)
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * -(↑k + 1) + 1) = -a ^ (2 * -(↑k + 1) + 1)

Tactic:
show 2 * -(↑k + 1) + (1 : ℤ) = - (1 + k*2) by grind,

Goal state after:
case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (-(1 + ↑k * 2)) = -a ^ (-(1 + ↑k * 2))
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ IsLeftRegular 0

Tactic:
isLeftRegular_zero_iff_subsingleton,

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ Subsingleton R
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ x ≠ 0 → f x ≠ 0

Tactic:
intro hx

Goal state after:
G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
hx : x ≠ 0
⊢ f x ≠ 0
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x y : WithBot α
hx : x ≠ ⊥
h : x ≤ y
⊢ unbotD a x ≤ unbotD a y

Tactic:
lift x to α using hx
  cases y <;> simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d

Tactic:
← inv_le_inv₀ ha.pos hc

Goal state after:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
h : a * b < c * d
hc : 0 < c
hh : a⁻¹ ≤ c⁻¹
ha : a ≠ 0
⊢ b < d
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
x : α
hx : 0 < x
hx' : x < 1
⊢ Nontrivial αˣ

Tactic:
exact ⟨Units.mk0 x hx.ne', 1, by simpa [Units.ext_iff] using hx'.ne⟩

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

Goal state before:
pp: case succ
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
| succ k ihk =>

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
x y : WithZero α
a : α
hx : x ≠ 0
h : x ≤ y
⊢ unzeroD a x ≤ unzeroD a y

Tactic:
lift x to α using hx
  cases y <;> simp_all

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
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

Tactic:
rw [ceil_le, Nat.cast_add, Nat.cast_one]

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a ≤ ↑⌊a⌋₊ + 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
rcases le_or_gt 0 a with (ha | ha)
  · rw [floor_lt ha]
    exact h.trans_le (le_ceil _)
  · rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]

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

Goal state before:
pp: G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
⊢ a ≠ 0 → f a ≠ 0

Tactic:
intro hx

Goal state after:
G₀ : Type u_3
M₀' : Type u_4
F : Type u_6
inst✝⁴ : GroupWithZero G₀
inst✝³ : MulZeroOneClass M₀'
inst✝² : Nontrivial M₀'
inst✝¹ : FunLike F G₀ M₀'
inst✝ : MonoidWithZeroHomClass F G₀ M₀'
f : F
a : G₀
hx : a ≠ 0
⊢ f a ≠ 0
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b x : α
⊢ x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b

Tactic:
by simp [and_right_comm, ← lt_iff_le_and_ne, eq_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iic a ⊆ s

Tactic:
by rw [← Iio_union_right, union_subset_iff]; simp [*]

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

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

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 .inl ⟨DirectedOn.of_isCofinalFor h subset_union_left hts.union_right, hts⟩

Goal state after:
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
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'

Tactic:
simp only [termg, h₁.symm, add_zsmul, h₂.symm]

Goal state after:
α : Type u_1
inst✝ : AddCommGroup α
n₁ : ℤ
x a₁ : α
n₂ : ℤ
a₂ : α
n' : ℤ
a' : α
h₁ : n₁ + n₂ = n'
h₂ : a₁ + a₂ = a'
⊢ n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
x a : α
⊢ termg 0 x a = a

Tactic:
by
  simp [termg, zero_zsmul]

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝

Tactic:
← neg_mul,

Goal state after:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -↑num✝ * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : c < a
⊢ AntitoneOn (fun x ↦ (x - c)⁻¹) (Set.Icc a b)

Tactic:
by
  by_cases hab : a ≤ b
  · exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
  · simp [hab, Set.Subsingleton.antitoneOn]

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

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
l✝ : List M
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → l.prod = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ (i :: l).prod = 1

Tactic:
rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]

Goal state after: