mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩

pp: case cons
α : Type u_1
n i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, h⟩).get ⟨i, ih⟩ = get ⟨head✝ :: tail✝, h⟩ ⟨i + 1, ⋯⟩

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
n i : ℕ
ih : i < n - 1
h : [].length = n
⊢ (tail ⟨[], h⟩).get ⟨i, ih⟩ = get ⟨[], h⟩ ⟨i + 1, ⋯⟩

case cons
α : Type u_1
n i : ℕ
ih : i < n - 1
head✝ : α
tail✝ : List α
h : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, h⟩).get ⟨i, ih⟩ = get ⟨head✝ :: tail✝, h⟩ ⟨i + 1, ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (a ::ᵥ v).get 0 = a

Tactic:
simp [get_zero]

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

Goal state before:
pp: case ha
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ a ∉ Finset.univ → f a = 1

pp: case hb
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ b ∉ Finset.univ → f b = 1

Tactic:
<;>

Goal state after:
case ha
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ a ∉ Finset.univ → f a = 1

case hb
α : Type u_1
M : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ b ∉ Finset.univ → f b = 1
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case inl
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
j : ι
a : α j
ha : a ∈ s j
⊢ #(Function.update s j {a} j) = Function.update (fun j ↦ #(s j)) j 1 j

pp: case inr
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
hji : j ≠ i
⊢ #(Function.update s i {a} j) = Function.update (fun j ↦ #(s j)) i 1 j

Tactic:
<;>

Goal state after:
case inl
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
j : ι
a : α j
ha : a ∈ s j
⊢ #(Function.update s j {a} j) = Function.update (fun j ↦ #(s j)) j 1 j

case inr
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
hji : j ≠ i
⊢ #(Function.update s i {a} j) = Function.update (fun j ↦ #(s j)) i 1 j
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) ↑(fill a m.fst m.snd) = ↑m.snd

Tactic:
coe_fill

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Encodable α
⊢ decodeList (encodeList []) = some []

pp: case cons
α : Type u_1
inst✝ : Encodable α
head✝ : α
tail✝ : List α
tail_ih✝ : decodeList (encodeList tail✝) = some tail✝
⊢ decodeList (encodeList (head✝ :: tail✝)) = some (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : Encodable α
⊢ decodeList (encodeList []) = some []

case cons
α : Type u_1
inst✝ : Encodable α
head✝ : α
tail✝ : List α
tail_ih✝ : decodeList (encodeList tail✝) = some tail✝
⊢ decodeList (encodeList (head✝ :: tail✝)) = some (head✝ :: tail✝)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case isTrue
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
h✝ : ↑i ≤ n
⊢ n + 1 = n + 1

pp: case isFalse
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
h✝ : ¬↑i ≤ n
⊢ n = n + 1

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
h✝ : ↑i ≤ n
⊢ n + 1 = n + 1

case isFalse
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
h✝ : ¬↑i ≤ n
⊢ n = n + 1
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg.refine_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map Subtype.val (decode (Sum.inr s)).attach

pp: case neg.refine_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s

Tactic:
<;>

Goal state after:
case neg.refine_1
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map Subtype.val (decode (Sum.inr s)).attach

case neg.refine_2
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

pp: case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : i = j
⊢ (v.set i a).get j = a

case neg
α : Type u_1
n : ℕ
v : Vector α n
i j : Fin n
a : α
h✝ : ¬i = j
⊢ (v.set i a).get j = v.get j
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
α β : Type u_6
f : α → β
⊢ traverseAux (pure ∘ f) [] = pure ⟨List.map f [], ⋯⟩

pp: case cons
α β : Type u_6
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : traverseAux (pure ∘ f) tail✝ = pure ⟨List.map f tail✝, ⋯⟩
⊢ traverseAux (pure ∘ f) (head✝ :: tail✝) = pure ⟨List.map f (head✝ :: tail✝), ⋯⟩

Tactic:
<;>

Goal state after:
case nil
α β : Type u_6
f : α → β
⊢ traverseAux (pure ∘ f) [] = pure ⟨List.map f [], ⋯⟩

case cons
α β : Type u_6
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : traverseAux (pure ∘ f) tail✝ = pure ⟨List.map f tail✝, ⋯⟩
⊢ traverseAux (pure ∘ f) (head✝ :: tail✝) = pure ⟨List.map f (head✝ :: tail✝), ⋯⟩
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a✝ : α
h : r a✝ a✝
⊢ False

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b✝ : β
h : s b✝ b✝
⊢ False

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a✝ : α
h : r a✝ a✝
⊢ False

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b✝ : β
h : s b✝ b✝
⊢ False
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl a✝ = inl c✝

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr b✝ = inr d✝

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a✝ c✝ : α
hab : r a✝ c✝
hba : r c✝ a✝
⊢ inl a✝ = inl c✝

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b✝ d✝ : β
hab : s b✝ d✝
hba : s d✝ b✝
⊢ inr b✝ = inr d✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a₁✝ : α
h : r a₁✝ a₁✝
⊢ False

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b₁✝ : β
h : s b₁✝ b₁✝
⊢ False

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a₁✝ : α
h : r a₁✝ a₁✝
⊢ False

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b₁✝ : β
h : s b₁✝ b₁✝
⊢ False
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₁✝ = inl a₂✝

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₁✝ = inr b₂✝

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
hba : r a₂✝ a₁✝
⊢ inl a₁✝ = inl a₂✝

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Antisymm r
inst✝ : Std.Antisymm s
b₁✝ b₂✝ : β
hab : s b₁✝ b₂✝
hba : s b₂✝ b₁✝
⊢ inr b₁✝ = inr b₂✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ≤ (Equiv.sumAssoc α β γ) b ↔ inl (inl val✝) ≤ b

pp: case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ≤ (Equiv.sumAssoc α β γ) b ↔ inl (inr val✝) ≤ b

pp: case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inr val✝) ≤ (Equiv.sumAssoc α β γ) b ↔ inr val✝ ≤ b

Tactic:
<;>

Goal state after:
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ≤ (Equiv.sumAssoc α β γ) b ↔ inl (inl val✝) ≤ b

case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ≤ (Equiv.sumAssoc α β γ) b ↔ inl (inr val✝) ≤ b

case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inr val✝) ≤ (Equiv.sumAssoc α β γ) b ↔ inr val✝ ≤ b
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False

Tactic:
exact hc.not_ge (hb <| hs ((hb ha).trans hc.le) ha)

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

Goal state before:
pp: case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
b : (α ⊕ₗ β)ᵒᵈ
a : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) b ↔ inl a ≤ b

pp: case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
b : (α ⊕ₗ β)ᵒᵈ
a : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) b ↔ inr a ≤ b

Tactic:
<;>

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
b : (α ⊕ₗ β)ᵒᵈ
a : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) b ↔ inl a ≤ b

case inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
b : (α ⊕ₗ β)ᵒᵈ
a : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) b ↔ inr a ≤ b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithBot α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithBot α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ b

Tactic:
<;>

Goal state after:
case bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithBot α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithBot α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithTop α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b

pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithTop α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝ ≤ b

Tactic:
<;>

Goal state after:
case top
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithTop α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b

case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
b : WithTop α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ True)
      (match ↑a✝, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ↑a✝ ≤ b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≺i Sum.Lex r s
g : s ≺i Sum.Lex r s
h : Sum.Lex r s g.top f.top
⊢ Nonempty ((r ≼i s) ⊕ (s ≼i r))

Tactic:
· exact ⟨Sum.inr <| (g.codRestrict {x | Sum.Lex r s x f.top}
          (fun a => _root_.trans (g.lt_top a) h) h).transRelIso f.subrelIso⟩

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

Goal state before:
pp: case mp
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂

pp: case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂

Tactic:
<;>

Goal state after:
case mp
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) →
    ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂

case mpr
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
⊢ (∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂) →
    ∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom

case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption.isSome = true ↔ o.Dom
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : o.Dom
⊢ o.toOption = none ↔ ¬o.Dom

case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
h : ¬o.Dom
⊢ o.toOption = none ↔ ¬o.Dom
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ a.toOption.elim b f = f (a.get h)

Tactic:
h.toOption

Goal state after:
case pos
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : a.Dom
⊢ (Option.some (a.get h)).elim b f = f (a.get h)
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
h : ¬a.Dom
⊢ a.toOption.elim b f = b

Tactic:
· rw [Part.toOption_eq_none_iff.2 h]
    rfl

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case none
α : Type u_1
⊢ (↑Option.none).toOption = Option.none

pp: case some
α : Type u_1
val✝ : α
⊢ (↑(Option.some val✝)).toOption = Option.some val✝

Tactic:
<;>

Goal state after:
case none
α : Type u_1
⊢ (↑Option.none).toOption = Option.none

case some
α : Type u_1
val✝ : α
⊢ (↑(Option.some val✝)).toOption = Option.some val✝
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy : z ≤ y
⊢ f z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
<;>

Goal state after:
case image_self_subset_self.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hzy : z ≤ y
⊢ f z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f z ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y

pp: case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y

Tactic:
<;>

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ x >>= f ≤ y → ∀ (a : α), a ∈ x → f a ≤ y

case mpr
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
⊢ (∀ (a : α), a ∈ x → f a ≤ y) → x >>= f ≤ y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case zero
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) 0 = (pair (a₁, b₁) (a₂, b₂) ⋯) 0

pp: case succ
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n✝ : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) (n✝ + 1) = (pair (a₁, b₁) (a₂, b₂) ⋯) (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) 0 = (pair (a₁, b₁) (a₂, b₂) ⋯) 0

case succ
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
n✝ : ℕ
⊢ ((pair a₁ a₂ ha).zip (pair b₁ b₂ hb)) (n✝ + 1) = (pair (a₁, b₁) (a₂, b₂) ⋯) (n✝ + 1)