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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)

Tactic:
by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a ↦ p a) a
he : ∀ (y : α), (fun a ↦ p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ ⟨b, hb⟩ = default

Tactic:
by
      congr
      exact he b hb

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

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y z : α
h : f z = g y
⊢ f z = g z

Tactic:
Subsingleton.elim y z

Goal state after:
case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
inst✝ : Subsingleton α
g : α → β
x y z : α
h : f z = g z
⊢ f z = g z
Module: Mathlib.Logic.Relation

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)

Tactic:
| intro a _ ih =>

Goal state after:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
inst✝² : (i : ι) → One (M i)
inst✝¹ : (i : ι) → One (N i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i
hf' : ∀ (i : ι), f' i 1 = 1
i : ι
x : M i
j : ι
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j

Tactic:
simpa only [Pi.one_apply, hf', mulSingle] using! Function.apply_update f' 1 i x j

Goal state after:
Module: Mathlib.Algebra.Notation.Pi.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
subst h
    simp only [mulSingle_eq_same]

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

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
n : ℤ
⊢ (g • a) ^ n = g ^ n • a ^ n

Tactic:
cases n <;> simp [smul_pow, smul_inv]

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

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ z • x₁ • y = x₁ • y • z

Tactic:
← smul_comm,

Goal state after:
R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ x₁ • z • y = x₁ • y • z
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ y • x • 1 = x • y

Tactic:
← smul_comm,

Goal state after:
M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : SMulCommClass M N N
x : M
y : N
⊢ x • y • 1 = x • y
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ False

Tactic:
by rw [e] at h; exact irrefl _ h

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b = b ↔ a ⊓ b = a

Tactic:
by rw [sup_eq_right, ← inf_eq_left]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ b ∨ a ≤ c

Tactic:
or_iff_right h

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬a ≤ b
⊢ a ≤ c ↔ a ≤ c
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = y ↔ x = ⊥ ∧ y = ⊥

Tactic:
by
  rw [disjoint_sdiff_self_left.eq_iff]; simp_all

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

Goal state before:
pp: case pos
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
right

Goal state after:
case pos
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t ∈ insert a '' 𝒫 s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x✝ : α
⊢ (∃ y, f y = x✝) ↔ x✝ = y

Tactic:
by simp_rw [h, exists_const, eq_comm]

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

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

Tactic:
right

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

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

Tactic:
right

Goal state after:
case neg
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
h : ¬x ∈ s
⊢ s.piecewise f g x ∈ g '' sᶜ
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)
ht : t.Nonempty
⊢ EqOn f f' s

Tactic:
by
  obtain ⟨x, hxt⟩ := ht
  intro x hxs
  have h' := h <| mk_mem_prod hxs hxt
  grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s

Tactic:
← preimage_sumElim,

Goal state after:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.elim Sum.inl Sum.inr ⁻¹' s = s
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}

Tactic:
ext ⟨x, hx⟩
  simp

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

Goal state before:
pp: case intro
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Subsingleton β
inst✝ : Nonempty β
val✝ : Unique β
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
simp [univ_unique, Subsingleton.elim (f _) default, Set.Nonempty]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : IsMulTorsionFree G
a : G
⊢ a⁻¹ = a ↔ a = 1

Tactic:
by rw [eq_comm, self_eq_inv]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n * a * (b * b ^ n) = a ^ n * (a * b) * b ^ n

Tactic:
by simp only [mul_assoc]

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

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

Tactic:
by
  rw [div_mul_eq_div_div_swap]; simp only [mul_div_cancel_right]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β), x <* y = Function.const β <$> x <*> y

Tactic:
intros
    casesm Sum _ _ <;> rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : α → β) (x : e ⊕ α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x

Tactic:
intros
    casesm Sum _ _ <;> rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : e ⊕ (α → β)) (x : e ⊕ α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      f <*> x

Tactic:
intros
    casesm Sum _ _ <;> rfl

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (x : e ⊕ α) (f : α → e ⊕ β) (g : β → e ⊕ γ), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
intros
    casesm Sum _ _ <;> rfl

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

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
⊢ (a • if p then b else 0) = if p then a • b else 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
⊢ g • x⁻¹ = (g • x)⁻¹

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : x = 0
⊢ g • x⁻¹ = (g • x)⁻¹

case neg
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
x : β
hx : ¬x = 0
⊢ g • x⁻¹ = (g • x)⁻¹
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝¹ : AddGroupWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by
  simpa only [OfNat.ofNat] using! AddGroupWithOne.intCast_ofNat (R := R) n

Goal state after:
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⁻¹ * y = ↑a⁻¹ * (y * ↑a * ↑a⁻¹)

Tactic:
by rw [Units.mul_inv_cancel_right]

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

Goal state before:
pp: case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
by_cases hx : x = 0

Goal state after:
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
u : M₀ˣ
a : M₀
h : ↑u * a = 0
⊢ a = 0

Tactic:
simpa using mul_eq_zero_of_right (↑u⁻¹) h

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd a

Tactic:
← sub_add_cancel a 1

Goal state after:
α : Type u_2
inst✝ : Ring α
h : IsUnit 2
a : α
⊢ Odd (a - 1 + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Even n
⊢ f^[n] = id

Tactic:
obtain ⟨m, rfl⟩ := hn

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[m + m] = id
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f

Tactic:
obtain ⟨m, rfl⟩ := hn

Goal state after:
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]

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

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

Tactic:
rw [mul_comm c, mul_comm c]

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ b * c
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
by
    contrapose! hab
    obtain ha | ha := hab.1.lt_or_gt <;> obtain hb | hb := hab.2.lt_or_gt
    exacts [(mul_pos_of_neg_of_neg ha hb).ne', (mul_neg_of_neg_of_pos ha hb).ne,
      (mul_neg_of_pos_of_neg ha hb).ne, (mul_pos ha hb).ne']

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

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a : R
ha : a ≠ 0
x✝¹ x✝ : R
h : (fun x ↦ a * x) x✝¹ = (fun x ↦ a * x) x✝
⊢ x✝¹ = x✝

Tactic:
obtain ha | ha := ha.lt_or_gt
    exacts [(strictAnti_mul_left ha).injective h, (strictMono_mul_left_of_pos ha).injective h]

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✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b ^ 2 = b ^ 2 + a * (a + b)

Tactic:
rw [← hab, mul_zero, add_zero]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hb, one_mul]

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₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
← inv_lt_inv₀ hb (inv_pos.2 ha),

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ < a⁻¹⁻¹ ↔ b⁻¹ < a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ (2 + 2) * r ^ 2 ≤ (a + b) * (a + b)

Tactic:
two_add_two_eq_four

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b r : R
ha : 0 ≤ a
hb : 0 ≤ b
ht : r ^ 2 ≤ a * b
⊢ 4 * r ^ 2 ≤ (a + b) * (a + b)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
q : Quotient x✝¹
h : Quotient.lift₂ r H q ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) q

Tactic:
obtain ⟨a', rfl⟩ := q.exists_rep

Goal state after:
case mpr.intro
α : Type u_1
x✝¹ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a x✝ : α
h✝ : ∀ (y : α), r y x✝ → Acc r y
IH : ∀ (y : α), r y x✝ → Acc (Quotient.lift₂ r H) ⟦y⟧
a' : α
h : Quotient.lift₂ r H ⟦a'⟧ ⟦x✝⟧
⊢ Acc (Quotient.lift₂ r H) ⟦a'⟧
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
⊢ Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂

Tactic:
by
  intro h x h₁ h₂
  rw [← f.le_iff_le] at h₁ h₂ ⊢
  calc
    f x ≤ ⊥ := h h₁ h₂
    _ ≤ f ⊥ := bot_le

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ✝ : Type u_5
inst✝⁷ : LE α✝
inst✝⁶ : LE β✝
inst✝⁵ : LE γ✝
inst✝⁴ : LE δ✝
α : Type ?u.19
β : Type ?u.21
γ : Type ?u.23
δ : Type ?u.25
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α ≃o γ
g : β ≃o δ
p : γ →o δ
⊢ (⇑g ∘ ⇑g.symm) ∘ ⇑p ∘ ⇑f ∘ ⇑f.symm = ⇑p

Tactic:
simp only [← OrderIso.coe_trans, Function.id_comp,
               OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f x) ↔ IsMax x

Tactic:
refine ⟨f.strictMono.isMax_of_apply, ?_⟩
  conv_lhs => rw [← f.symm_apply_apply x]
  exact f.symm.strictMono.isMax_of_apply

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

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ |b|ₘ

Tactic:
mabs_of_le_one (hab.trans ha)

Goal state after:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ b⁻¹
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inl
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rw [Nat.sub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
    exact mono_cast h

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
    rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
m n : ℕ
⊢ -↑m = ↑n ↔ m = 0 ∧ n = 0

Tactic:
simp [neg_eq_iff_add_eq_zero, ← cast_add]

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

Goal state before:
pp: case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

pp: case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
· cases m
    · rwa [h]
    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim

Goal state after:
case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.bot
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMinOrder α
h : DenselyOrdered (WithBot α)
a b : α
hab : a < b
hc : ↑a < ⊥ ∧ ⊥ < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
simp at hc

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp.top
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
hc : ↑a < ⊤ ∧ ⊤ < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
simp at hc

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

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Semiring R
inst✝ : LinearOrder R
H₁ H₂ : FloorSemiring R
this : FloorSemiring.ceil = FloorSemiring.ceil
a : R
h : a < 0
⊢ FloorSemiring.floor a = FloorSemiring.floor a

Tactic:
rw [H₁.floor_of_neg, H₂.floor_of_neg] <;> exact h

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
inst✝ : ExistsAddOfLE R
k : ℕ
h₀ : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
rw [pow_add, mul_self_pos, pow_ne_zero_iff (by simpa using h₀)]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f s t ⊆ image2 f s' t'

Tactic:
by
  rintro _ ⟨a, ha, b, hb, rfl⟩
  exact mem_image2_of_mem (hs ha) (ht hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬(image2 f s t).Nonempty ↔ s = ∅ ∨ t = ∅

Tactic:
image2_nonempty_iff,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
⊢ ¬(s.Nonempty ∧ t.Nonempty) ↔ s = ∅ ∨ t = ∅
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact mul_self_lt_mul_self_iff (abs_nonneg a) (abs_nonneg b)

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

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

Tactic:
refine (abs_add_le ..).trans ?_

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a * geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)
Module: Mathlib.Data.Set.NAry

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

Tactic:
inter_subset_right

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s t ∪ image2 f s' t' ⊆ image2 f s t ∪ image2 f s' t'
Module: Mathlib.Data.Set.NAry

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

Tactic:
inter_subset_right

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f s t ∪ image2 f s' t' ⊆ image2 f s t ∪ image2 f s' t'
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsGreatest (f '' s) (f a) ↔ IsGreatest s a

Tactic:
simp [IsGreatest, hf.injective.eq_iff, hf.mem_upperBounds_image]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
⊢ {b | p (e.symm b)} = ⇑e.symm ⁻¹' {a | p a}

Tactic:
preimage_ofPred_eq

Goal state after:
α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
⊢ {b | p (e.symm b)} = {a | p (e.symm a)}
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : β
h : Sum.inr val✝ ∈ range Sum.inl
⊢ False

Tactic:
rcases h with ⟨x, h'⟩

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : β
x : α
h' : Sum.inl x = Sum.inr val✝
⊢ False
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : α
h : Sum.inl val✝ ∈ range Sum.inr
⊢ False

Tactic:
rcases h with ⟨x, h'⟩

Goal state after:
α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
val✝ : α
x : β
h' : Sum.inr x = Sum.inl val✝
⊢ False
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ j = i ∨ Iio i = Iic j

Tactic:
right

Goal state after:
case inr
γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
hj_lt_i : j < i
⊢ Iio i = Iic j
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [div_le_iff₀ hb, one_mul]

Goal state after: