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

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys ↔ ∀ (s : Sigma β), s ∈ l → a ≠ s.fst

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ (s :: l).NodupKeys ↔ ¬s.fst ∈ l.keys ∧ l.NodupKeys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
s : Sigma β
⊢ (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
h : (s :: l).NodupKeys
⊢ ¬s.fst ∈ l.keys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
a : α
b b' : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : ⟨a, b'⟩ ∈ l
⊢ b = b'

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
L : List (List (Sigma β))
l : List (Sigma β)
x✝ : l ∈ L
⊢ Pairwise (fun s s' ↦ s.fst ≠ s'.fst) l ↔ l.NodupKeys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ L.flatten.NodupKeys ↔ (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise Disjoint (map keys L)

Tactic:
by

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

Goal state before:
pp: α : Type u
l : List α
⊢ (map Prod.snd l.zipIdx).Nodup

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
l₀ l₁ : List (Sigma β)
nd₀ : l₀.Nodup
nd₁ : l₁.Nodup
h : ∀ (x : Sigma β), x ∈ l₀ ↔ x ∈ l₁
⊢ l₀ ~ l₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
a : α
b : β a
s : Multiset (Sigma β)
⊢ (⟨a, b⟩ ::ₘ s).keys = a ::ₘ s.keys

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
m : Multiset ((a : α) × β a)
⊢ m.keys.Nodup ↔ m.NodupKeys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ (dlookup a l).isSome = true ↔ a ∈ l.keys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup a l = none ↔ ¬a ∈ l.keys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ b ∈ dlookup a l → ⟨a, b⟩ ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧ = ⟦s₂⟧ ↔ s₁.entries ~ s₂.entries

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ b ∈ dlookup a l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ Option.map (Sigma.mk a) (dlookup a l) = find? (fun s ↦ decide (a = s.fst)) l

Tactic:
by

Goal state after:
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₂
⊢ dlookup a l₁ = dlookup a l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₀ l₁ : List (Sigma β)
nd₀ : l₀.NodupKeys
nd₁ : l₁.NodupKeys
h : ∀ (x : α) (y : β x), y ∈ dlookup x l₀ ↔ y ∈ dlookup x l₁
⊢ l₀ ~ l₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Sort ?u.13
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ γ

Tactic:
by

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

Goal state before:
pp: α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
l : List (Sigma β)
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (Sigma.map f g) l) = Option.map (g a) (dlookup a l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ ⟦s⟧.liftOn f H = f s

Tactic:
by

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

Goal state before:
pp: α : Type u
α' : Type u'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
⊢ dlookup (f a) (map (Sigma.map f fun x ↦ id) l) = dlookup a l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type ?u.51
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
⊢ s₂.liftOn (f a₁) ⋯ = s₂.liftOn (f a₂) ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
h : (Sigma.map f (fun x ↦ id) hd).fst ∈ (map (Sigma.map f fun x ↦ id) tl).keys
⊢ hd.fst ∈ tl.keys

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C ⟦a⟧
⊢ C s

Tactic:
by

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

Goal state before:
pp: α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
l : List ((_ : α) × β)
nd : l.NodupKeys
⊢ (map (Sigma.map f fun x ↦ id) l).NodupKeys

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
l₁ : Multiset (Sigma β)
h₁ : l₁.NodupKeys
l₂ : Multiset (Sigma β)
nodupKeys✝ : l₂.NodupKeys
H : { entries := l₁, nodupKeys := h₁ }.entries = { entries := l₂, nodupKeys := nodupKeys✝ }.entries
⊢ { entries := l₁, nodupKeys := h₁ } = { entries := l₂, nodupKeys := nodupKeys✝ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧.keys = ⟦s₂⟧.keys ↔ s₁.keys ~ s₂.keys

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
⊢ (map (Sigma.map id f) l).keys = l.keys

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
nd : l.NodupKeys
⊢ (map (Sigma.map id f) l).NodupKeys

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup a s.toFinmap = dlookup a s

Tactic:
by

Goal state after:
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
⊢ IsEmpty ↑S'.toTop

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
⊢ dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ b ∈ lookup a s ↔ ⟨a, b⟩ ∈ s.entries

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
b : β a
nd₂ : l₂.NodupKeys
s : l₁ <+ l₂
mem : b ∈ dlookup a l₁
⊢ b ∈ dlookup a l₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ lookupAll a [] = [] ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
⊢ (s.keys.sigma fun i ↦ (lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ lookup a (singleton a b) = some b

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a', b⟩ :: l

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (lookupAll a []).head? = dlookup a []

Tactic:
by

Goal state after:
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 y : ↑(S' ⊗ ℕ∪{∞}).toTop), h.elim x = h.elim y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ s.max' hs < t.min' ht

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : s.Nonempty
ht : ¬t.Nonempty
p : α
hp : s.max' hs < p
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), lookup x ⟦s₁⟧ = lookup x ⟦s₂⟧
⊢ ⟦s₁⟧ = ⟦s₂⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : t.Nonempty
p : α
hp : p < t.min' ht
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ lookupAll a [] ↔ ⟨a, b⟩ ∈ []

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
⊢ b ∈ lookupAll a (⟨a', b'⟩ :: l) ↔ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
hs : ¬s.Nonempty
ht : ¬t.Nonempty
p : α
⊢ (∀ x ∈ s, x < p) ∧ ∀ y ∈ t, p < y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ map (Sigma.mk a) (lookupAll a []) <+ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val.NodupKeys

Tactic:
by

Goal state after:
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)
⊢ π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ } = 𝟙 T'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
f : Finmap β
⊢ ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ })
        ((fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩) f)).entries =
    f.entries

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finset.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
s t : Finset α
inst✝² : NoMaxOrder α
inst✝¹ : NoMinOrder α
inst✝ : Nonempty α
H : ∀ x ∈ s, ∀ y ∈ t, x < y
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
by

Goal state after:
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
⊢ hsf.toFinset.Nonempty

Tactic:
by

Goal state after:
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
⊢ htf.toFinset.Nonempty

Tactic:
by

Goal state after:
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
⊢ ∀ x ∈ hsf.toFinset, ∀ y ∈ htf.toFinset, x < y

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by

Goal state after:
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
⊢ ∀ x ∈ hs.toFinset, ∀ y ∈ ht.toFinset, x < y

Tactic:
by

Goal state after:
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
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), ((s, f).2 i).isSome = true ↔ i ∈ (s, f).1
⊢ (fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
      ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩) =
    ⟨(s, f), hf⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : Finmap β
⊢ (keysLookupEquiv.symm (keysLookupEquiv x✝)).keys = (↑(keysLookupEquiv x✝)).1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝¹ : Finmap β
x✝ : α
⊢ lookup x✝ (keysLookupEquiv.symm (keysLookupEquiv x✝¹)) = (↑(keysLookupEquiv x✝¹)).2 x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Multiset α), id <$> x = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (g : α → β) (h : β → γ) (x : Multiset α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x : α'
l₁ l₂ : List α'
a✝ : l₁ ~ l₂
h : ofList <$> Traversable.traverse f l₁ = ofList <$> Traversable.traverse f l₂
⊢ cons <$> f x <*> ofList <$> Traversable.traverse f l₁ = cons <$> f x <*> ofList <$> Traversable.traverse f l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (fun a b l ↦ ↑(a :: b :: l)) <$> f y <*> f x = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ Multiset α' → F (Multiset β')

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ replace a b ⟦s⟧ = ⟦AList.replace a b s⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ : Type u_1
x✝ : Multiset α✝
⊢ id <$> x✝ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
⊢ (replace a b ⟦s⟧).keys = ⟦s⟧.keys

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ β✝ : Type u_1
x✝¹ : α✝
x✝ : α✝ → Multiset β✝
⊢ pure x✝¹ >>= x✝ = x✝ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
s✝ : Finmap β
s : AList β
⊢ a' ∈ replace a b ⟦s⟧ ↔ a' ∈ ⟦s⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
α✝ β✝ : Type u_1
x✝¹ : α✝ → β✝
x✝ : Multiset α✝
⊢ (do
      let y ← x✝
      pure (x✝¹ y)) =
    x✝¹ <$> x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α β : Type u_1
h : α → β
⊢ Functor.map h ∘ ofList = ofList ∘ Functor.map h

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ || f x✝² x✝¹ || f x✝ b₂) = (x✝³ || f x✝ b₂ || f x✝² x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: α : Type u_1
x : Multiset α
⊢ traverse pure x = pure x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x✝³ : Bool
x✝² : α
x✝¹ : β x✝²
x✝ : α
⊢ ∀ (b₂ : β x✝), (x✝³ && f x✝² x✝¹ && f x✝ b₂) = (x✝³ && f x✝ b₂ && f x✝² x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ erase a ⟦s⟧ = ⟦AList.erase a s⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ ⟦AList.erase a s⟧.keys = ⟦s⟧.keys.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s✝ : Finmap β
s : AList β
⊢ (erase a ⟦s⟧).keys = ⟦s⟧.keys.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ a' ∈ erase a ⟦s⟧ ↔ a' ≠ a ∧ a' ∈ ⟦s⟧

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
x : Multiset α
⊢ Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a ∉ erase a s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ ¬(b :: c :: l).length ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
⊢ insert a b ⟦s⟧ = ⟦AList.insert a b s⟧

Tactic:
by

Goal state after: