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

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ 0 * a ≤ 0 * b

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x * a ≤ x * b

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ x * a ≤ x * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
a b : WithBot α
h : a ≤ b
x0 : 0 ≤ 0
⊢ a * 0 ≤ b * 0

pp: case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ a * x ≤ b * x

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : a ≤ b
x0' : x ≠ 0
⊢ a * x ≤ b * x
Module: Mathlib.Order.SuccPred.WithBot

Goal state before:
pp: case bot
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
⊢ ⊥.succ = ⊥ ↔ ⊥ = ⊥

pp: case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
⊢ (↑a✝).succ = ⊥ ↔ ↑a✝ = ⊥

Tactic:
· simp

Goal state after:
case coe
α : Type u_2
inst✝³ : Nontrivial α
inst✝² : LinearOrder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a✝ : α
⊢ (↑a✝).succ = ⊥ ↔ ↑a✝ = ⊥
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (∃ n, succ^[n] a = b) → a ≤ b

Tactic:
rintro ⟨n, rfl⟩

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a : α
n : ℕ
⊢ a ≤ succ^[n] a
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
⊢ ¬IsMin ↑a

Tactic:
have := ha.1

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccLimit a
this : ¬IsMin a
⊢ ¬IsMin ↑a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

Tactic:
by_contra hba

Goal state after:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬b ≤ succ a
⊢ False
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ (x + ↑n) = x + ↑(n + 1)

Tactic:
Nat.cast_add,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + ↑n
⊢ succ (x + ↑n) = x + (↑n + ↑1)
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
⊢ succ^[n] x = x + ↑n

Tactic:
by
  induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred (x - ↑n) = x - ↑(n + 1)

Tactic:
Nat.cast_add,

Goal state after:
case succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - ↑n
⊢ pred (x - ↑n) = x - (↑n + ↑1)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ succ a = ⨅ b, ⨅ (_ : b > a), b

Tactic:
by
  rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]

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

Goal state before:
pp: case coe
m : ℕ
inst✝ : NeZero m
a✝ : ℕ
⊢ (↑a✝).toNat = m ↔ ↑a✝ = ↑m

Tactic:
· simp

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

Goal state before:
pp: case top.top
⊢ (⊤ * ⊤).toNat = ⊤.toNat * ⊤.toNat

pp: case top.coe
a✝ : ℕ
⊢ (⊤ * ↑a✝).toNat = ⊤.toNat * (↑a✝).toNat

pp: case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat

Tactic:
· simp

Goal state after:
case top.coe
a✝ : ℕ
⊢ (⊤ * ↑a✝).toNat = ⊤.toNat * (↑a✝).toNat

case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
a✝ : ℕ
⊢ motive ↑a✝

Tactic:
· exact A _

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

Goal state before:
pp: case top
a : ℕ∞
h : a < ⊤
⊢ a ≤ ⊤ - 1

pp: case coe
a : ℕ∞
a✝ : ℕ
h : a < ↑a✝
⊢ a ≤ ↑a✝ - 1

Tactic:
· simp

Goal state after:
case coe
a : ℕ∞
a✝ : ℕ
h : a < ↑a✝
⊢ a ≤ ↑a✝ - 1
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inl
c : ℕ∞
hc : c ≠ 0
hne : 0 ≠ ⊤
⊢ 0 ≤ 0 * c

pp: case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ a ≤ a * c

Tactic:
· simp

Goal state after:
case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ a ≤ a * c
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: 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⟩
y : α
hy : y ∈ s
h : ⟨y, hy⟩ ≤ ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
rcases h.lt_or_eq with h | h

Goal state after:
case neg.inl
α✝ : 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⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ < ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩

case neg.inr
α✝ : 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⟩
y : α
hy : y ∈ s
h✝ : ⟨y, hy⟩ ≤ ⟨x, hx⟩
h : ⟨y, hy⟩ = ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inl
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

pp: case inr
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
· simp

Goal state after:
case inr
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr.inl
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0

pp: case inr.inr
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
· simp

Goal state after:
case inr.inr
a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
this : ∀ (z : ℕ∞), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ a✝ < ↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
Nat.cast_add,

Goal state after:
case coe
m : ℕ
a✝ : ℕ∞
⊢ a✝ < ↑m + ↑1 ↔ ↑a✝ ≤ ↑m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥

pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝

Tactic:
· simp

Goal state after:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_1
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun x ↦ x ∈ s) = fun x ↦ x ∈ {x | x ∈ s}

pp: case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
· simp

Goal state after:
case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
η η' : ApplicativeTransformation F G
h : ∀ (α : Type u) (x : F α), (fun {α} ↦ η.app α) x = (fun {α} ↦ η'.app α) x
⊢ (fun {α} ↦ η.app α) = fun {α} ↦ η'.app α

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (∏ j, if h : i = j then f j h else 1) = f i ⋯

Tactic:
by
  rw [Finset.prod_dite_eq, if_pos (mem_univ _)]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j, if j = i then f j else 1) = f i

Tactic:
by
  rw [Finset.prod_ite_eq', if_pos (mem_univ _)]

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

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

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'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i

Tactic:
· simp

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
⊢ ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ↑(a ::ₛ ofVector v) = ↑(ofVector (a ::ᵥ v))

Tactic:
by
    cases v
    rfl

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

Goal state before:
pp: case succ.succ.refine_1
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)

pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)

Tactic:
· simp

Goal state after:
case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s

pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inl.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

pp: case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simp

Goal state after:
case inl.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inl ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : ¬r a x
b : α
hb : ¬r b x
⊢ r ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨a, ha⟩)) ((Equiv.sumCompl fun x_1 ↦ r x_1 x) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ r x_1 x) (Subrel r fun x_1 ↦ ¬r x_1 x) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simp

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

Goal state before:
pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simp

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
h : IsSuccPrelimit ⊥
⊢ sSup (Iio ⊥) = ⊥

pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x

Tactic:
· simp

Goal state after:
case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : IsSuccPrelimit x
hx : ⊥ < x
⊢ sSup (Iio x) = x
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f = g

Tactic:
by
  rw [← toRelEmbedding_inj]
  ext
  exact h _

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

Tactic:
rw [InitialSeg.transPrincipal]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)
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 : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' d)
⊢ f (Exists.choose hd₂) ∈ (fun x ↦ f '' x) d

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuousOn univ f
hg : ScottContinuousOn univ g
⊢ ∀ (a b : α), a ≤ b → {a, b} ∈ univ

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ lfp f
hmem : f (sSup s) ∈ s
⊢ sSup s = lfp f

Tactic:
exact h.antisymm (f.lfp_le <| le_sSup hmem)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
⊢ (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })) → ωScottContinuous f

Tactic:
intro hf _ ⟨c, hc⟩ _ _ _ hda

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
hf : ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })
d✝ : Set α
c : Chain α
hc : (fun c ↦ Set.range ⇑c) c = d✝
a✝² : d✝.Nonempty
a✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d✝
a✝ : α
hda : IsLUB d✝ a✝
⊢ IsLUB (f '' d✝) (f a✝)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ Cardinal.sum g
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < 2 ^ Cardinal.sum g

Tactic:
exact cantor _

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a ≤ lift.{v, u} ↑n ↔ a ≤ ↑n

Tactic:
lift_le

Goal state after:
a : Cardinal.{u}
n : ℕ
⊢ a ≤ ↑n ↔ a ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ lift.{v, u} ↑n ≤ lift.{v, u} a ↔ ↑n ≤ a

Tactic:
lift_le

Goal state after:
n : ℕ
a : Cardinal.{u}
⊢ ↑n ≤ a ↔ ↑n ≤ a
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x ≤ lift.{u, v} ↑m ↔ x ≤ ↑m

Tactic:
lift_le

Goal state after:
x : Cardinal.{v}
m : ℕ∞
⊢ x ≤ ↑m ↔ x ≤ ↑m
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} ↑m ≤ lift.{u, v} x ↔ ↑m ≤ x

Tactic:
lift_le

Goal state after:
x : Cardinal.{v}
m : ℕ∞
⊢ ↑m ≤ x ↔ ↑m ≤ x
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr.inl
y : Cardinal.{u}
hy : ℵ₀ ≤ y
hle : 0 ≤ y
⊢ (0 * y).toENatAux = toENatAux 0 * y.toENatAux

pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
· simp

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2.inr
s : Set Cardinal.{u_1}
ha : 0 ∈ s
⊢ sInf s = 0

Tactic:
· exact eq_bot_iff.2 (csInf_le' ha)

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

Goal state before:
pp: case inl
⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)

pp: case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
· simp

Goal state after:
case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d
⊢ False

Tactic:
lift_le

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬sSup s ≤ d
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ ℵ₀ < #α ↔ Uncountable α

Tactic:
by
  rw [← not_le, ← not_countable_iff, not_iff_not, mk_le_aleph0_iff]

Goal state after: