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

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).toList = List.map f (toList ⟨val✝, property✝⟩)

Tactic:
;

Goal state after:
case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).toList = List.map f (toList ⟨val✝, property✝⟩)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
val✝ : List α
property✝ : val✝.length = n
hp : ∀ (x : α), x ∈ toList ⟨val✝, property✝⟩ → p x
⊢ (pmap f ⟨val✝, property✝⟩ hp).toList = List.pmap f (toList ⟨val✝, property✝⟩) hp

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
val✝ : List α
property✝ : val✝.length = n
hp : ∀ (x : α), x ∈ toList ⟨val✝, property✝⟩ → p x
⊢ (pmap f ⟨val✝, property✝⟩ hp).toList = List.pmap f (toList ⟨val✝, property✝⟩) hp
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head = v.head ∨ v.head ∈ v.tail.toList

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head = v.head ∨ v.head ∈ v.tail.toList
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x = v.head ∨ x ∈ v.tail.toList

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
x : α
hx : x ∈ v.tail.toList
⊢ x = v.head ∨ x ∈ v.tail.toList
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : ∀ (a : α), Uncountable (π a)
inhabited_h : Inhabited α
⊢ Uncountable (Sigma π)

Tactic:
;

Goal state after:
α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : ∀ (a : α), Uncountable (π a)
inhabited_h : Inhabited α
⊢ Uncountable (Sigma π)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
i : Fin n
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).get i = f (get ⟨val✝, property✝⟩ i)

Tactic:
;

Goal state after:
case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
i : Fin n
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).get i = f (get ⟨val✝, property✝⟩ i)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨↑⟨i, ih⟩ + 1, ⋯⟩

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
x : Vector α n
i : ℕ
ih : i < n - 1
⊢ x.tail.get ⟨i, ih⟩ = x.get ⟨↑⟨i, ih⟩ + 1, ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).toList[i] = get ⟨a :: l, e⟩ ⟨i + 1, ⋯⟩

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
a : α
l : List α
e : (a :: l).length = n.succ
i : ℕ
h : i < n
⊢ (tail ⟨a :: l, e⟩).toList[i] = get ⟨a :: l, e⟩ ⟨i + 1, ⋯⟩
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x ↦ x) s) = ↑s

Tactic:
;

Goal state after:
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map (fun x ↦ x) s) = ↑s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s

Tactic:
;

Goal state after:
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s

Tactic:
;

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
m✝ : Fin (0 + 1)
⊢ (scanl f b nil).get m✝ = (b ::ᵥ nil).get m✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
m✝ : Fin (0 + 1)
⊢ (scanl f b nil).get m✝ = (b ::ᵥ nil).get m✝
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ (scanl f b (x ::ᵥ v)).toList = (b ::ᵥ scanl f (f b x) v).toList

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
x : α
⊢ (scanl f b (x ::ᵥ v)).toList = (b ::ᵥ scanl f (f b x) v).toList
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:
Multiset.card_add,

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
⊢ (↑s).card + (↑s').card = n + n'
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (0 + 1)
i : Fin (0 + 1)
i0 : i = 0
⊢ (b ::ᵥ f b v.head ::ᵥ nil).get 1 = f b v.head

Tactic:
;

Goal state after:
case succ.zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (0 + 1)
i : Fin (0 + 1)
i0 : i = 0
⊢ (b ::ᵥ f b v.head ::ᵥ nil).get 1 = f b v.head
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
val✝ : Multiset α
l : List α
h : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk (⇑(List.isSetoid α)) l, h⟩) =
    ⟨Quot.mk (⇑(List.isSetoid α)) l, h⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
val✝ : Multiset α
l : List α
h : Multiset.card (Quot.mk (⇑(List.isSetoid α)) l) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk (⇑(List.isSetoid α)) l, h⟩) =
    ⟨Quot.mk (⇑(List.isSetoid α)) l, h⟩
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b : α
val✝ : Multiset α
a : α
h : Multiset.card (Quot.mk ⇑(List.isSetoid α) [a]) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩) =
    ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a✝ b : α
val✝ : Multiset α
a : α
h : Multiset.card (Quot.mk ⇑(List.isSetoid α) [a]) = 1
⊢ (fun a ↦ ⟨{a}, ⋯⟩)
      ((fun s ↦
          ((Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x.length = 1) (fun x ↦ Multiset.card x = 1) ⋯ ⋯)
                s).liftOn
            (fun l ↦ (↑l).head ⋯) ⋯)
        ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩) =
    ⟨Quot.mk ⇑(List.isSetoid α) [a], h⟩
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ a ≠ x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m

Tactic:
;

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b (filter (fun x ↦ a ≠ x) ↑m + ↑(replicate (count a ↑m) a)) = count b ↑m
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ Option.map (fun x1 x2 ↦ x1 :: x2) (decode v₁) <*> decodeList v₂ =
    Option.map (fun x1 x2 ↦ x1 :: x2) (decode v₁) <*> decode v₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ Option.map (fun x1 x2 ↦ x1 :: x2) (decode v₁) <*> decodeList v₂ =
    Option.map (fun x1 x2 ↦ x1 :: x2) (decode v₁) <*> decode v₂
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ some [], encodeList a = 0

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Denumerable α
⊢ ∃ a ∈ some [], encodeList a = 0
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
this : Countable ↑s
⊢ (range fun x ↦ f ↑x).Countable

Tactic:
apply countable_range

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

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a

Tactic:
;

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x

Tactic:
;

Goal state after:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x} ↔ p x
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝

Tactic:
;

Goal state after:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
x✝ : α
⊢ x✝ ∈ {x | p x} ↔ p x✝
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (range fun a ↦ ↑a.snd).Countable

Tactic:
apply countable_range

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

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
i : Fin n
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get i = a

Tactic:
;

Goal state after:
case mk
α : Type u_1
n : ℕ
i : Fin n
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get i = a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
n : ℕ
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get ⟨val✝, isLt✝⟩ = a

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
n : ℕ
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get ⟨val✝, isLt✝⟩ = a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get j = get ⟨val✝, property✝⟩ j

Tactic:
;

Goal state after:
case mk
α : Type u_1
n : ℕ
i j : Fin n
h : i ≠ j
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (set ⟨val✝, property✝⟩ i a).get j = get ⟨val✝, property✝⟩ j
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
n : ℕ
j : Fin n
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝, isLt✝⟩ ≠ j
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get j = get ⟨val✝¹, property✝⟩ j

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
n : ℕ
j : Fin n
a : α
val✝¹ : List α
property✝ : val✝¹.length = n
val✝ : ℕ
isLt✝ : val✝ < n
h : ⟨val✝, isLt✝⟩ ≠ j
⊢ (set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get j = get ⟨val✝¹, property✝⟩ j
Module: Mathlib.Data.Vector.Basic

Goal state before:
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 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: F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ ⟨xs, ⋯⟩) = cons <$> f x <*> Vector.traverse f ⟨xs, ⋯⟩

Tactic:
;

Goal state after:
F : Type u → Type u
inst✝ : Applicative F
α β : Type u
f : α → F β
x : α
xs : List α
⊢ Vector.traverse f (x ::ᵥ ⟨xs, ⋯⟩) = cons <$> f x <*> Vector.traverse f ⟨xs, ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u
x : List α
⊢ Vector.traverse pure ⟨x, ⋯⟩ = pure ⟨x, ⋯⟩

Tactic:
;

Goal state after:
α : Type u
x : List α
⊢ Vector.traverse pure ⟨x, ⋯⟩ = pure ⟨x, ⋯⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ : Type u
x : flip Vector n α✝
⊢ id <$> x = x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ : Type u
x : flip Vector n α✝
⊢ id <$> x = x
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ : Type u
val✝ : List α✝
property✝ : val✝.length = n
⊢ id <$> ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ : Type u
val✝ : List α✝
property✝ : val✝.length = n
⊢ id <$> ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x : flip Vector n α✝
⊢ (h✝ ∘ g✝) <$> x = h✝ <$> g✝ <$> x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x : flip Vector n α✝
⊢ (h✝ ∘ g✝) <$> x = h✝ <$> g✝ <$> x
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : List α✝
property✝ : val✝.length = n
⊢ (h✝ ∘ g✝) <$> ⟨val✝, property✝⟩ = h✝ <$> g✝ <$> ⟨val✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : List α✝
property✝ : val✝.length = n
⊢ (h✝ ∘ g✝) <$> ⟨val✝, property✝⟩ = h✝ <$> g✝ <$> ⟨val✝, property✝⟩
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨val✝, property✝⟩ ++ nil = ⟨val✝, property✝⟩

Tactic:
;

Goal state after:
case mk
α : Type u_1
n : ℕ
val✝ : List α
property✝ : val✝.length = n
⊢ ⟨val✝, property✝⟩ ++ nil = ⟨val✝, property✝⟩
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Ici x ↔ x✝ ∈ {y | ¬y < x}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Ici x ↔ x✝ ∈ {y | ¬y < x}
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Iic x ↔ x✝ ∈ {y | ¬x < y}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y x✝ : α
⊢ x✝ ∈ Iic x ↔ x✝ ∈ {y | ¬x < y}
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit (sSup s)

Tactic:
csSup_of_not_bddAbove hlim,

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
hlim : ¬BddAbove s
⊢ IsSuccPrelimit (sSup ∅)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α₁ : 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 γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ α₂
⊢ ((e₁.sumCongr e₂).trans (f₁.sumCongr f₂)) x✝ = ((e₁.trans f₁).sumCongr (e₂.trans f₂)) x✝

Tactic:
;

Goal state after:
α₁ : 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 γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ α₂
⊢ ((e₁.sumCongr e₂).trans (f₁.sumCongr f₂)) x✝ = ((e₁.trans f₁).sumCongr (e₂.trans f₂)) x✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ β
⊢ ((refl α).sumCongr (refl β)) x✝ = (refl (α ⊕ β)) x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ β
⊢ ((refl α).sumCongr (refl β)) x✝ = (refl (α ⊕ β)) x✝
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h : t (g.toRelEmbedding b) (g (f a))
⊢ g.toRelEmbedding b ∈ Set.range (⇑g ∘ ⇑f)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a : α
b : β
h : t (g.toRelEmbedding b) (g (f a))
⊢ g.toRelEmbedding b ∈ Set.range (⇑g ∘ ⇑f)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : 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 : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ (a a_1 : α₁ ⊕ β₁),
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex a) ≤
        (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex a_1) ↔
      toLex a ≤ toLex a_1

Tactic:
;

Goal state after:
α : 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 : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ (a a_1 : α₁ ⊕ β₁),
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex a) ≤
        (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) (toLex a_1) ↔
      toLex a ≤ toLex a_1
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a a' : α
h✝ : t (g.toRelEmbedding (f.toRelEmbedding a')) (g (f a))
h : s (f.toRelEmbedding a') (f a)
⊢ g.toRelEmbedding (f.toRelEmbedding a') ∈ Set.range (⇑g ∘ ⇑f)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≼i s
g : s ≼i t
a a' : α
h✝ : t (g.toRelEmbedding (f.toRelEmbedding a')) (g (f a))
h : s (f.toRelEmbedding a') (f a)
⊢ g.toRelEmbedding (f.toRelEmbedding a') ∈ Set.range (⇑g ∘ ⇑f)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α₁ : 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 γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ₗ α₂
⊢ ((e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂)) x✝ = ((e₁.trans f₁).sumLexCongr (e₂.trans f₂)) x✝

Tactic:
;

Goal state after:
α₁ : 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 γ₂
e₁ : α₁ ≃o β₁
e₂ : α₂ ≃o β₂
f₁ : β₁ ≃o γ₁
f₂ : β₂ ≃o γ₂
x✝ : α₁ ⊕ₗ α₂
⊢ ((e₁.sumLexCongr e₂).trans (f₁.sumLexCongr f₂)) x✝ = ((e₁.trans f₁).sumLexCongr (e₂.trans f₂)) x✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ₗ β
⊢ ((refl α).sumLexCongr (refl β)) x✝ = (refl (α ⊕ₗ β)) x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LE α
inst✝ : LE β
x✝ : α ⊕ₗ β
⊢ ((refl α).sumLexCongr (refl β)) x✝ = (refl (α ⊕ₗ β)) x✝
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), f a ∈ p
a : α
x✝ : { x // x ∈ p }
a' : α
m : f a' ∈ p
h : Subrel s (fun x ↦ x ∈ p) ⟨f a', m⟩ ((RelEmbedding.codRestrict p f.toRelEmbedding H) a)
⊢ (RelEmbedding.codRestrict p f.toRelEmbedding H) a' = ⟨f a', m⟩

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
p : Set β
f : r ≼i s
H : ∀ (a : α), f a ∈ p
a : α
x✝ : { x // x ∈ p }
a' : α
m : f a' ∈ p
h : Subrel s (fun x ↦ x ∈ p) ⟨f a', m⟩ ((RelEmbedding.codRestrict p f.toRelEmbedding H) a)
⊢ (RelEmbedding.codRestrict p f.toRelEmbedding H) a' = ⟨f a', m⟩
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 γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨅ i, f i) x = (⨅ i, ⇑(f i)) x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨅ i, f i) x = (⨅ i, ⇑(f i)) x
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
s : Set α
a✝³ : s ∈ D
a : α
h✝ : a ∈ s
a✝² : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a✝¹ : α
a✝ : IsLUB s a✝¹
⊢ ∀ ⦃a : β⦄, (∀ a_1 ∈ s, x ≤ a) → x ≤ a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set α)
x : β
s : Set α
a✝³ : s ∈ D
a : α
h✝ : a ∈ s
a✝² : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a✝¹ : α
a✝ : IsLUB s a✝¹
⊢ ∀ ⦃a : β⦄, (∀ a_1 ∈ s, x ≤ a) → x ≤ a
Module: Mathlib.Order.Hom.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨆ i, f i) x = (⨆ i, ⇑(f i)) x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨆ i, f i) x = (⨆ i, ⇑(f i)) x
Module: Mathlib.Order.Hom.Order

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

Tactic:
;

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

Goal state before:
pp: case refl
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }

Tactic:
;

Goal state after:
case refl
α : Type u_1
od : Prop
o p : od → α
H1 : { Dom := od, get := o }.Dom ↔ { Dom := od, get := p }.Dom
H2 :
  ∀ (h₁ : { Dom := od, get := o }.Dom) (h₂ : { Dom := od, get := p }.Dom),
    { Dom := od, get := o }.get h₁ = { Dom := od, get := p }.get h₂
⊢ { Dom := od, get := o } = { Dom := od, get := p }