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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ x ∈ xs

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
x : α
⊢ x ∈ xs
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_1.e_x
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ pempty = x✝

Tactic:
;

Goal state after:
case h_1.e_x
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ pempty = x✝
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) α

Tactic:
;

Goal state after:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
| recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) α
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
⊢ ↑((fun x ↦ ⟨List.idxOf x xs, ⋯⟩) (xs.get i)) = ↑i

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
h : ∀ (x : α), x ∈ xs
h' : xs.Nodup
i : Fin xs.length
⊢ ↑((fun x ↦ ⟨List.idxOf x xs, ⋯⟩) (xs.get i)) = ↑i
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ ∃ a, equiv.symm a = x

Tactic:
;

Goal state after:
α : Type u
inst✝ : FinEnum α
x : α
⊢ ∃ a, equiv.symm a = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ equiv.symm (equiv x) = x

Tactic:
;

Goal state after:
α : Type u
inst✝ : FinEnum α
x : α
⊢ equiv.symm (equiv x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
⊢ (List.map (⇑equiv.symm) (List.finRange (card α))).Nodup

Tactic:
;

Goal state after:
α : Type u
inst✝ : FinEnum α
⊢ (List.map (⇑equiv.symm) (List.finRange (card α))).Nodup
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.19
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ x✝ ∈ List.map f (toList β)

Tactic:
;

Goal state after:
α : Type u
β✝ : α → Type v
β : Type ?u.19
f : β → α
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Surjective f
x✝ : α
⊢ x✝ ∈ List.map f (toList β)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case mk
α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ∈ toList α ×ˢ toList β

Tactic:
;

Goal state after:
case mk
α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ∈ toList α ×ˢ toList β
Module: Mathlib.Data.FinEnum.Option

Goal state before:
pp: case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = (card α).pred.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin (card α).pred)) ↑↑(finChoice (card α).pred)) inst✝ ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
;

Goal state after:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = (card α).pred.succ
⊢ (let fN := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin (card α).pred)) ↑↑(finChoice (card α).pred)) inst✝ ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} ↦ congr) empty (fun {α} ↦ option) (ULift.{u, 0} (Fin (card α - 1)))))
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ List.filterMap (fun x ↦ if h : p x then some ⟨x, h⟩ else none) (toList α)

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝¹ : FinEnum α
p : α → Prop
inst✝ : DecidablePred p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ List.filterMap (fun x ↦ if h : p x then some ⟨x, h⟩ else none) (toList α)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
x : Sigma β
⊢ x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
;

Goal state after:
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
x : Sigma β
⊢ x ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case mk
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
fst✝ : α
snd✝ : β fst✝
⊢ ⟨fst✝, snd✝⟩ ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)

Tactic:
;

Goal state after:
case mk
α : Type u
β✝ β : α → Type v
inst✝¹ : FinEnum α
inst✝ : (a : α) → FinEnum (β a)
fst✝ : α
snd✝ : β fst✝
⊢ ⟨fst✝, snd✝⟩ ∈ List.flatMap (fun a ↦ List.map (Sigma.mk a) (toList (β a))) (toList α)
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : α
⊢ x✝ ∈ map equiv.symm.toEmbedding univ

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : α
⊢ x✝ ∈ map equiv.symm.toEmbedding univ
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case e_3
α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ (α ≃ Fin (card α)) = (α ≃ Fin 0)

Tactic:
exact congrArg (α ≃ Fin ·) <| card_eq_zero

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt8
⊢ UInt8.ofFin x.toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : UInt8
⊢ UInt8.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (UInt8.ofFin x).toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (UInt8.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt16
⊢ UInt16.ofFin x.toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : UInt16
⊢ UInt16.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (UInt16.ofFin x).toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (UInt16.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt32
⊢ UInt32.ofFin x.toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : UInt32
⊢ UInt32.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (UInt32.ofFin x).toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (UInt32.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : UInt64
⊢ UInt64.ofFin x.toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : UInt64
⊢ UInt64.ofFin x.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (UInt64.ofFin x).toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (UInt64.ofFin x).toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int8
⊢ (Int8.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int8.toBitVec) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Int8
⊢ (Int8.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int8.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (BitVec.toFin ∘ Int8.toBitVec) ((Int8.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 8)
⊢ (BitVec.toFin ∘ Int8.toBitVec) ((Int8.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int16
⊢ (Int16.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int16.toBitVec) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Int16
⊢ (Int16.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int16.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (BitVec.toFin ∘ Int16.toBitVec) ((Int16.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 16)
⊢ (BitVec.toFin ∘ Int16.toBitVec) ((Int16.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int32
⊢ (Int32.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int32.toBitVec) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Int32
⊢ (Int32.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int32.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (BitVec.toFin ∘ Int32.toBitVec) ((Int32.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 32)
⊢ (BitVec.toFin ∘ Int32.toBitVec) ((Int32.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Int64
⊢ (Int64.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int64.toBitVec) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Int64
⊢ (Int64.ofBitVec ∘ BitVec.ofFin) ((BitVec.toFin ∘ Int64.toBitVec) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (BitVec.toFin ∘ Int64.toBitVec) ((Int64.ofBitVec ∘ BitVec.ofFin) x) = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
x : Fin (2 ^ 64)
⊢ (BitVec.toFin ∘ Int64.toBitVec) ((Int64.ofBitVec ∘ BitVec.ofFin) x) = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
x : BitVec n
⊢ { toFin := x.toFin } = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
n : ℕ
x : BitVec n
⊢ { toFin := x.toFin } = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
x : Fin (2 ^ n)
⊢ { toFin := x }.toFin = x

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
n : ℕ
x : Fin (2 ^ n)
⊢ { toFin := x }.toFin = x
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))

Tactic:
;

Goal state after:
α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : p
x : (hp : p) → α hp
⊢ x ∈ map (fun x x_1 ↦ x) (FinEnum.toList (α hp))
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => (#[].push a).toListAppend (lookmap.go f l #[])) =
    a :: lookmap.go f l #[]

Tactic:
;

Goal state after:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => (#[].push a).toListAppend (lookmap.go f l #[])) =
    a :: lookmap.go f l #[]
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b

Tactic:
;

Goal state after:
case h
α : Type u_1
f : α → Option α
h : ∀ (a b : α), b ∈ f a → a = b
l : List α
⊢ ∀ (a b : α), b ∈ f a → id a = id b
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case h
α : Type u_1
f : α → Option α
l : List α
⊢ ∀ (a b : α), b ∈ f a → () = ()

Tactic:
;

Goal state after:
case h
α : Type u_1
f : α → Option α
l : List α
⊢ ∀ (a b : α), b ∈ f a → () = ()
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a : α
l₁✝ l₂✝ : List α
p : l₁✝ ~ l₂✝
IH : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) l₁✝ → lookmap f l₁✝ ~ lookmap f l₂✝
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (a :: l₁✝)
⊢ lookmap f (a :: l₁✝) ~ lookmap f (a :: l₂✝)

Tactic:
cases h : f a
    · simpa [h] using IH (pairwise_cons.1 H).2
    · simp [lookmap_cons_some _ _ h, p]

Goal state after:
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs.entries = ys.entries)

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
xs ys : AList β
⊢ Decidable (xs.entries = ys.entries)
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ ⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
p : s₁.entries ~ s₂.entries
⊢ ⟨a, b⟩ :: kerase a s₁.entries ~ ⟨a, b⟩ :: kerase a s₂.entries
Module: Mathlib.Data.List.AList

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup k' (insert k' v l) = none ↔ k' ≠ k' ∧ lookup k' l = none

Tactic:
;

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : AList β
k' : α
v : β k'
⊢ lookup k' (insert k' v l) = none ↔ k' ≠ k' ∧ lookup k' l = none
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ ⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ ⟨a', b'⟩ :: kerase a' (⟨a, b⟩ :: kerase a s.entries) ~ ⟨a, b⟩ :: kerase a (⟨a', b'⟩ :: kerase a' s.entries)
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (dlookup a s.entries, kerase a s.entries).snd.NodupKeys

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ (dlookup a s.entries, kerase a s.entries).snd.NodupKeys
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
i✝ : ℕ
a✝ : Sigma β
⊢ (insert a b (s₁ ∪ s₂)).entries[i✝]? = some a✝ ↔ (insert a b s₁ ∪ s₂).entries[i✝]? = some a✝

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
i✝ : ℕ
a✝ : Sigma β
⊢ (insert a b (s₁ ∪ s₂)).entries[i✝]? = some a✝ ↔ (insert a b s₁ ∪ s₂).entries[i✝]? = some a✝
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ (keys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)).Nodup ↔ NodupKeys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)

Tactic:
;

Goal state after:
case mk
α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
l : List ((a : α) × β a)
⊢ (keys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)).Nodup ↔ NodupKeys (Quot.mk (⇑(isSetoid ((a : α) × β a))) l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys
b : β a
⊢ dlookup a l₁ = some b ↔ dlookup a l₂ = some b

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys
b : β a
⊢ dlookup a l₁ = some b ↔ dlookup a l₂ = some b
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) a)
⊢ C { entries := Quot.mk (⇑(isSetoid (Sigma β))) a, nodupKeys := h }

Tactic:
;

Goal state after:
case mk
α : Type u
β : α → Type v
C : Finmap β → Prop
H : ∀ (a : AList β), C ⟦a⟧
entries✝ : Multiset (Sigma β)
a : List (Sigma β)
h : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) a)
⊢ C { entries := Quot.mk (⇑(isSetoid (Sigma β))) a, nodupKeys := h }
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
x y : α
b : β y
⊢ x ∈ singleton y b ↔ x = y

Tactic:
by
  simp [singleton, mem_def]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l)
⊢ b ∈ lookup a { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl } ↔
    ⟨a, b⟩ ∈ { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl }.entries

Tactic:
;

Goal state after:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
entries✝ : Multiset (Sigma β)
l : List (Sigma β)
hl : Multiset.NodupKeys (Quot.mk (⇑(isSetoid (Sigma β))) l)
⊢ b ∈ lookup a { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl } ↔
    ⟨a, b⟩ ∈ { entries := Quot.mk (⇑(isSetoid (Sigma β))) l, nodupKeys := hl }.entries
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll a (⟨a, b⟩ :: l)).head? = dlookup a (⟨a, b⟩ :: l)

Tactic:
;

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll a (⟨a, b⟩ :: l)).head? = dlookup a (⟨a, b⟩ :: l)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑T'.toTop
⊢ (ConcreteCategory.hom (π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ })) x =
    (ConcreteCategory.hom (𝟙 T')) x

Tactic:
;

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑T'.toTop
⊢ (ConcreteCategory.hom (π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ })) x =
    (ConcreteCategory.hom (𝟙 T')) x
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : (lookupAll a l).length ≤ 1
⊢ lookupAll a l = (lookupAll a l).head?.toList

Tactic:
;

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : (lookupAll a l).length ≤ 1
⊢ lookupAll a l = (lookupAll a l).head?.toList
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hsf.toFinset, x < b) ∧ ∀ y ∈ htf.toFinset, b < y

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Set α
hsf : s.Finite
hs : s.Nonempty
htf : t.Finite
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hsf.toFinset, x < b) ∧ ∀ y ∈ htf.toFinset, b < y
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hs.toFinset, x < b) ∧ ∀ y ∈ ht.toFinset, b < y

Tactic:
;

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
s t : Set α
hs : s.Finite
ht : t.Finite
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ (fun b ↦ (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y) = fun b ↦ (∀ x ∈ hs.toFinset, x < b) ∧ ∀ y ∈ ht.toFinset, b < y