mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝¹ : LT α
inst✝ : WellFoundedLT α
a x✝² : α
x✝¹ : ∀ (y : α), y < x✝² → Acc (fun x1 x2 ↦ x1 < x2) y
ih : ∀ (y : α), y < x✝² → Acc (fun x1 x2 ↦ x1 < x2) ↑y
x✝ : ⊥ < ↑x✝²
⊢ ∀ (y : WithBot α), y < ⊥ → Acc (fun x1 x2 ↦ x1 < x2) y

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a * a⁻¹ = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : GroupWithZero α
a : α
inst✝ : Invertible a
⊢ a⁻¹ * a = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LE α
inst✝¹ : NoTopOrder α
inst✝ : Nonempty α
a : α
⊢ ¬↑a ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a✝ b : α
inst✝² : LT α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
a : α
⊢ ⊥ < ↑a

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Mul R
inst✝² : One R
inst✝¹ : HasDistribNeg R
a : R
inst✝ : Invertible a
⊢ -⅟a * -a = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Mul R
inst✝² : One R
inst✝¹ : HasDistribNeg R
a : R
inst✝ : Invertible a
⊢ -a * -⅟a = 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
inst✝² : HasDistribNeg R
a : R
inst✝¹ : Invertible a
inst✝ : Invertible (-a)
⊢ -a * -⅟a = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LE α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ⊥ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LE α
a✝ : α
⊢ WithBot.toDual ↑a✝ ≤ WithBot.toDual ⊥ ↔ ⊥ ≤ ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LE α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ ≤ WithBot.toDual ↑a✝ ↔ ↑a✝ ≤ ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

Tactic:
by
  rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LT α
⊢ WithBot.toDual ⊥ < WithBot.toDual ⊥ ↔ ⊥ < ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ⊥ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : α
⊢ WithBot.toDual ↑a✝ < WithBot.toDual ⊥ ↔ ⊥ < ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : α
⊢ WithBot.toDual ↑a✝¹ < WithBot.toDual ↑a✝ ↔ ↑a✝ < ↑a✝¹

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.bot
α : Type u_1
inst✝ : LT α
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ⊥ ↔ ⊥ < ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot.coe
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ⊥ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝ : LT α
a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝ < WithBot.ofDual ⊥ ↔ ⊥ < ↑a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝ : LT α
a✝¹ a✝ : αᵒᵈ
⊢ WithBot.ofDual ↑a✝¹ < WithBot.ofDual ↑a✝ ↔ ↑a✝ < ↑a✝¹

Tactic:
simp

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

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ 0 * (a ⊓ b) = 0 * a ⊓ 0 * b

Tactic:
simp

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

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ 0 * (a ⊔ b) = 0 * a ⊔ 0 * b

Tactic:
simp

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

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ (a ⊓ b) * 0 = a * 0 ⊓ b * 0

Tactic:
simp

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

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ (a ⊔ b) * 0 = a * 0 ⊔ b * 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : Monoid M
inst✝³ : GroupWithZero G₀
inst✝² : FunLike F G₀ M₀
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : Nontrivial M₀
f : F
⊢ f 0 ≠ 1

Tactic:
simp

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 b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 0 ≤ 2 ^ (0 - 1) * (a ^ 0 + b ^ 0)

Tactic:
simp

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 b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ (a + b) ^ 1 ≤ 2 ^ (1 - 1) * (a ^ 1 + b ^ 1)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g x✝ : G
⊢ (fun x ↦
        match x with
        | ⟨val, h⟩ => Exists.choose h)
      ((fun a ↦ ⟨g * a, ⋯⟩) x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
G : Type u_4
inst✝ : LeftCancelSemigroup G
g w✝ : G
⊢ (fun a ↦ ⟨g * a, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨val, h⟩ => Exists.choose h)
        ⟨g * w✝, ⋯⟩) =
    ⟨g * w✝, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝ : DivisionRing K
⊢ 0⁻¹ = 0 ↔ 0 = -1 ∨ 0 = 0 ∨ 0 = 1

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
⊢ a ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℤ
⊢ a ^ (-n) = (a ^ n)⁻¹

Tactic:
simp

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
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ a ^ n + c ^ n + d ^ n = d ^ n

Tactic:
hn.pow_add_pow_eq_zero hac.symm,

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ 0 + d ^ n = d ^ n
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Set α
t : Set β
⊢ ∀ (x : α × β), x ∈ image2 Prod.mk s t ↔ x ∈ s ×ˢ t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
⊢ ∀ (x : γ), x ∈ image2 f ∅ t ↔ x ∈ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ image2 f s ∅ ↔ x ∈ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a : α
⊢ |a * a| = a * a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
a : α
⊢ 1 ≤ |a| + 1

Tactic:
simp

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

Goal state before:
pp: case e'_2
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = |a| ^ n

pp: case e'_3
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ 1 = 1 ^ n

Tactic:
exacts [(pow_abs _ _).symm, (one_pow _).symm]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
a : α
x : γ
⊢ x ∈ image2 f {a} t ↔ x ∈ f a '' t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
b : β
x : γ
⊢ x ∈ image2 f s {b} ↔ x ∈ (fun a ↦ f a b) '' s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
a : α
b : β
⊢ image2 f {a} {b} = {f a b}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
x✝ : δ
⊢ x✝ ∈ image2 f (g '' s) t ↔ x✝ ∈ image2 (fun a b ↦ f (g a) b) s t

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → γ → δ
g : β → γ
x✝ : δ
⊢ x✝ ∈ image2 f s (g '' t) ↔ x✝ ∈ image2 (fun a b ↦ f a (g b)) s t

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * max |a| |b| ^ (0 - 1)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddAbove t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddAbove s → BddBelow t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Monotone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
⊢ BddBelow s → BddBelow t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Antitone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddAbove (image2 f s t)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddBelow s → BddAbove t → BddAbove (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ lowerBounds s
b : β
hb : b ∈ upperBounds t
⊢ BddAbove (image2 f s t)
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
s : Set (α × β)
x : ↑s
⊢ (↑x).2 ∈ {y | ((↑x).1, y) ∈ s}

Tactic:
simp

Goal state after:
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
e : α ≃ β
s : Set α
x : ↑s
⊢ e ↑x ∈ ⇑e '' s

Tactic:
simp

Goal state after:
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 ∧ (m = x ∨ r m x)
a b : α
⊢ {a, b}.Nonempty

Tactic:
simp

Goal state after:
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
e : α ≃ β
s : Set α
x : ↑s
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun x ↦ ⟨e ↑x, ⋯⟩) x) = x

Tactic:
simp

Goal state after:
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
e : α ≃ β
s : Set α
y : ↑(⇑e '' s)
⊢ (fun x ↦ ⟨e ↑x, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
⊢ f ∈ {f | StrictMono f} → ∀ ⦃x₂ : β → γ⦄, x₂ ∈ {f | StrictMono f} → range f = range x₂ → f = x₂

Tactic:
hf

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
⊢ ∀ ⦃x₂ : β → γ⦄, x₂ ∈ {f | StrictMono f} → range f = range x₂ → f = x₂
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
H : Disjoint s t
a : ↑s
⊢ ↑a ∈ s ∪ t

Tactic:
simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
H : Disjoint s t
a : ↑t
⊢ ↑a ∈ s ∪ t

Tactic:
simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
H : ¬a ∈ s
⊢ insert a s = s ∪ {a}

Tactic:
simp

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

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
x✝ : ↑S
⊢ x✝ ∈ (fun x ↦ Subtype.val ⁻¹' ↑x) ((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) x) ↔ x✝ ∈ x

Tactic:
simp

Goal state after:
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
f : α → β
s : Set ↑(range f)
x : ↑(rangeSplitting f '' s)
⊢ f ↑x ∈ range f

Tactic:
simp

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

Goal state before:
pp: α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf) ((ofInjective f hf).symm ⟨f a, ⋯⟩) = (ofInjective f hf) a

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x✝ : α
⊢ ↑((ofLeftInverse f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑((ofLeftInverse' f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬a ∈ Iio a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ a ∈ Iic a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ ¬a ∈ Ioo a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ ¬a ∈ Ioc a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB (⇑f '' s) x
⊢ ∀ {x y : α}, f y ≤ f x ↔ y ≤ x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : β
h : IsLUB s (f.symm x)
⊢ ∀ {x y : β}, f.symm y ≤ f.symm x ↔ y ≤ x

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Iio 1 ↔ x✝ ∈ ∅

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ IsEmpty ↑(Iio 1)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Ici 1 ↔ x✝ ∈ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a ∈ Icc a a

Tactic:
simp

Goal state after:
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.toOrderEmbedding = ⇑g.toOrderEmbedding

Tactic:
DFunLike.coe_fn_eq,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Preorder β
f g : α ≃o β
⊢ f.toOrderEmbedding = g.toOrderEmbedding
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
⊢ BddAbove s → BddAbove t → BddAbove (s ∪ t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
⊢ BddAbove (s ∪ t)
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Iic x)
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun y ↦ ⟨e ↑y, ⋯⟩) y) = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Iic (e x))
⊢ (fun y ↦ ⟨e ↑y, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : ↑(Iic x)},
    { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Ici x)
⊢ (fun y ↦ ⟨e.symm ↑y, ⋯⟩) ((fun y ↦ ⟨e ↑y, ⋯⟩) y) = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
y : ↑(Ici (e x))
⊢ (fun y ↦ ⟨e ↑y, ⋯⟩) ((fun y ↦ ⟨e.symm ↑y, ⋯⟩) y) = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x : α
⊢ ∀ {a b : ↑(Ici x)},
    { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun y ↦ ⟨e ↑y, ⋯⟩, invFun := fun y ↦ ⟨e.symm ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_4
α : Type u_5
inst✝ : SemilatticeSup α
f g : ι → α
h : BddAbove (range fun x ↦ f x ⊔ g x)
⊢ BddAbove (range f)

Tactic:
have ⟨b, hb⟩ := h
  exact ⟨b, fun a ⟨i, ha⟩ ↦ ha ▸ le_sup_left.trans (hb ⟨i, rfl⟩)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y✝ : α
y : ↑(Icc x y✝)
⊢ (fun z ↦ ⟨e.symm ↑z, ⋯⟩) ((fun z ↦ ⟨e ↑z, ⋯⟩) y) = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y✝ : α
y : ↑(Icc (e x) (e y✝))
⊢ (fun z ↦ ⟨e ↑z, ⋯⟩) ((fun z ↦ ⟨e.symm ↑z, ⋯⟩) y) = y

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
⊢ ∀ {a b : ↑(Icc x y)},
    { toFun := fun z ↦ ⟨e ↑z, ⋯⟩, invFun := fun z ↦ ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun z ↦ ⟨e ↑z, ⋯⟩, invFun := fun z ↦ ⟨e.symm ↑z, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : BoundedOrder α
⊢ Icc ⊥ ⊤ = univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α × β
⊢ Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = ↑a✝

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝)

Tactic:
simp

Goal state after: