mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < ⊤
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) ⊤

Tactic:
simp [← coe_mul, mul_top h₀.ne']

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c✝ : WithTop α
b c : α
hbc : ↑b < ↑c
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) ↑c

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
a : α
h₀ : 0 < ↑a
c✝ : WithTop α
b c : α
hbc : ↑b < ↑c
⊢ (fun x ↦ ↑a * x) ↑b < (fun x ↦ ↑a * x) ↑c
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < ⊤
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) ⊤

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c : WithTop α
b : α
hbc : ↑b < ⊤
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c✝ : WithTop α
b c : α
hbc : ↑b < ↑c
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) ↑c

Tactic:
| =>

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
a : α
h₀ : 0 < ↑a
c✝ : WithTop α
b c : α
hbc : ↑b < ↑c
⊢ (fun x ↦ x * ↑a) ↑b < (fun x ↦ x * ↑a) ↑c
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inr.coe.coe.top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
hc : ⊤ ≠ 0
⊢ ↑a * ↑b * ⊤ = ⊤

Tactic:
rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb

Goal state after:
case inr.inr.inr.coe.coe.top
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a : α
ha : ¬a = 0
b : α
hb : ¬b = 0
hc : ⊤ ≠ 0
⊢ ↑a * ↑b * ⊤ = ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inr.coe.coe.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
c : α
hc : ↑c ≠ 0
⊢ ↑a * ↑b * ↑c = ↑a * (↑b * ↑c)

Tactic:
| coe c =>

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

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

Tactic:
| coe c =>

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

Goal state before:
pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

Tactic:
| coe c =>

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

Goal state before:
pp: case neg.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithBot α
hb : ¬b = 0
ha : ¬⊥ = 0
⊢ unbotD 0 (⊥ * b) = unbotD 0 ⊥ * unbotD 0 b

Tactic:
rw [bot_mul hb, unbotD_bot, zero_mul]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ False

Tactic:
rw [not_covBy_iff] at this

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ∃ c, ⟨b, ⋯⟩ < c ∧ c < a
⊢ False

α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ ⟨b, ⋯⟩ < a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax (succ^[n] a)

pp: case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)

Tactic:
· exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)

Goal state after:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
← Iio_inter_Ioi,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Iio (succ b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : LinearOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x < 2 ↔ x ≤ 1

Tactic:
by
  rw [← one_add_one_eq_two, lt_add_one_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
⊢ a ≤
    match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

Tactic:
obtain - | a := a

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
⊢ none ≤
    match none with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

case some
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : α
⊢ Option.some a ≤
    match Option.some a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h : ⟨x, hx⟩ ≤ if h : pred x ∈ s then ⟨pred x, h⟩ else ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
split_ifs at h with h'

Goal state after:
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : ⟨x, hx⟩ ≤ ⟨pred x, h'⟩
⊢ IsMin ⟨x, hx⟩

case neg
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∉ s
h : ⟨x, hx⟩ ≤ ⟨x, hx⟩
⊢ IsMin ⟨x, hx⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ
n : WithTop ℕ∞
h : ↑m < ⊤
⊢ ↑(m + 1) ≤ ⊤

Tactic:
| =>

Goal state after:
m : ℕ
n : WithTop ℕ∞
h : ↑m < ⊤
⊢ ↑(m + 1) ≤ ⊤
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ
n : WithTop ℕ∞
h : ↑m < ↑⊤
⊢ ↑(m + 1) ≤ ↑⊤

Tactic:
| =>

Goal state after:
m : ℕ
n : WithTop ℕ∞
h : ↑m < ↑⊤
⊢ ↑(m + 1) ≤ ↑⊤
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ
n✝ : WithTop ℕ∞
n : ℕ
h : ↑m < ↑n
⊢ ↑(m + 1) ≤ ↑n

Tactic:
| =>

Goal state after:
m : ℕ
n✝ : WithTop ℕ∞
n : ℕ
h : ↑m < ↑n
⊢ ↑(m + 1) ≤ ↑n
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : WithTop ℕ∞
⊢ ⊤ + 1 = ↑⊤ ↔ ⊤ = ↑⊤

Tactic:
| =>

Goal state after:
n : WithTop ℕ∞
⊢ ⊤ + 1 = ↑⊤ ↔ ⊤ = ↑⊤
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : WithTop ℕ∞
⊢ ↑⊤ + 1 = ↑⊤ ↔ ↑⊤ = ↑⊤

Tactic:
| =>

Goal state after:
n : WithTop ℕ∞
⊢ ↑⊤ + 1 = ↑⊤ ↔ ↑⊤ = ↑⊤
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n✝ : WithTop ℕ∞
n : ℕ
⊢ ↑n + 1 = ↑⊤ ↔ ↑n = ↑⊤

Tactic:
| =>

Goal state after:
n✝ : WithTop ℕ∞
n : ℕ
⊢ ↑n + 1 = ↑⊤ ↔ ↑n = ↑⊤
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑(g' i) = f i

pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩

pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a

Tactic:
hg' _ hi

Goal state after:
case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ f i = f i

case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩

case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })

Tactic:
Fintype.card_sum

Goal state after:
α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card { x // p x } + card { x // q x }
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
⊢ (↑s + ↑s').card = n + n'

Tactic:
rw [Multiset.card_add, s.2, s'.2]

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

Goal state before:
pp: case zero.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
w : Vector β 0
⊢ C ⟨[], ⋯⟩ w

Tactic:
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩

Goal state after:
case zero.nil.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
⊢ C ⟨[], ⋯⟩ ⟨[], ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero.nil.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
w : Vector γ 0
⊢ C ⟨[], ⋯⟩ ⟨[], ⋯⟩ w

Tactic:
rcases w with ⟨_ | ⟨-, -⟩, - | -⟩

Goal state after:
case zero.nil.nil.nil
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
⊢ C ⟨[], ⋯⟩ ⟨[], ⋯⟩ ⟨[], ⋯⟩
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List α
⊢ map id l = l

Tactic:
List.map_id

Goal state after:
α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List α
⊢ l = l
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ map id l = l

Tactic:
List.map_id

Goal state after:
α : Type ?u.9
β : Type ?u.10
e : α ≃ β
l : List β
⊢ l = l
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match none with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
| =>

Goal state after:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match none with
    | some y => ↑y
    | none => default) ∈
    insert default s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
val : ↑s
⊢ (match some val with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
| =>

Goal state after:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
val : ↑s
⊢ (match some val with
    | some y => ↑y
    | none => default) ∈
    insert default s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match decode n with
    | some y => ↑y
    | none => default) ∈
    insert default s

Tactic:
match @decode s (Countable.toEncodable h) n with
  | none => exact mem_insert _ _
  | some val => simp

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : α
⊢ ∃ b, b < a

Tactic:
by
        obtain ⟨b | b, h⟩ := exists_lt (inl a : α ⊕ β)
        · exact ⟨b, inl_lt_inl_iff.1 h⟩
        · exact (not_inr_lt_inl h).elim

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
hs : IsUpperSet s
ht : IsUpperSet t
⊢ s ⊆ t ∨ t ⊆ s

Tactic:
grind [isUpperSet_iff_forall_lt]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(IsWellFounded.fix r
        (fun a IH ↦
          have H := ⋯;
          ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
        a) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH ↦
                  have H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}

Tactic:
IsWellFounded.fix_eq

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
⊢ ↑(have H := ⋯;
      ⟨⋯.min
          {b |
            ∀ (a_1 : α) (h : r a_1 a),
              s
                (↑((fun y x ↦
                      IsWellFounded.fix r
                        (fun a IH ↦
                          have H := ⋯;
                          ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                        y)
                    a_1 h))
                b}
          ⋯,
        ⋯⟩) ∈
    {b |
      ∀ (a' : α),
        r a' a →
          s
            (↑(IsWellFounded.fix r
                (fun a IH ↦
                  have H := ⋯;
                  ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
                a'))
            b}
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(IsWellFounded.fix r
          (fun a IH ↦
            have H := ⋯;
            ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩)
          a)

Tactic:
IsWellFounded.fix_eq

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
a : α
b : β
h : ∀ (a' : α), r a' a → s (↑(collapseF f a')) b
⊢ ¬s b
      ↑(have H := ⋯;
        ⟨⋯.min
            {b |
              ∀ (a_1 : α) (h : r a_1 a),
                s
                  (↑((fun y x ↦
                        IsWellFounded.fix r
                          (fun a IH ↦
                            have H := ⋯;
                            ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩)
                          y)
                      a_1 h))
                  b}
            ⋯,
          ⋯⟩)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : LT α
f : α ≤i β
⊢ IsLowerSet (Set.range ⇑f)

Tactic:
rintro _ b h ⟨a, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : LT α
f : α ≤i β
b : β
a : α
h : b ≤ f a
⊢ b ∈ Set.range ⇑f
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b

Tactic:
IsLUB,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (upperBounds {a, b}) b
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB ((fun x ↦ (f x, g x)) '' d) ((fun x ↦ (f x, g x)) a)

Tactic:
IsLUB,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLeast (upperBounds ((fun x ↦ (f x, g x)) '' d)) ((fun x ↦ (f x, g x)) a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ((fun x ↦ (f x, g x)) a).1 ≤ (p₁, p₂).1

Tactic:
isLUB_le_iff (hf hd₁ hd₂ hd₃ hda),

Goal state after:
case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ (p₁, p₂).1 ∈ upperBounds (f '' d)
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Tactic:
have hx := hx _ h₀

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx✝ : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
hx : b ∈ z
⊢ b' ∈ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ f '' bot x f ⊆ bot x f

Tactic:
rintro _ ⟨y, hy, rfl⟩ s hs

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : y ∈ bot x f
s : Set α
hs : s ∈ {s | IsAdmissible x f s}
⊢ f y ∈ s
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : b ∈ x >>= f → b ∈ y
⊢ b ∈ f a → b ∈ y

Tactic:
simp only [and_imp, bind_eq_bind, mem_bind_iff, exists_imp] at h

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h✝ : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
h : ∀ (x_1 : α), x_1 ∈ x → b ∈ f x_1 → b ∈ y
⊢ b ∈ f a → b ∈ y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
⊢ some a ∈ c

Tactic:
have h' := Classical.choose_spec h_1

Goal state after:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
⊢ range h = univ

Tactic:
range_piecewise,

Goal state after:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
⊢ f '' s ∪ g' '' sᶜ = univ
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: ⊢ StrictMonoOn (⇑toENat) (Iic ℵ₀)

Tactic:
simp only [← range_ofENat, StrictMonoOn, forall_mem_range, toENat_ofENat, ofENat_lt_ofENat]

Goal state after:
⊢ ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m + ↑n < ℵ₀

Tactic:
rw [← Nat.cast_add]; apply natCast_lt_aleph0

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
rw [← image_eq_range]
    exact bddAbove_image.{u, u} _ bddAbove_Iio

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : A
⊢ { toFun := fun r ↦ r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := fun r ↦ r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
by simp [h₁, h₂]

Goal state after: