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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (insertRec H0 IH { entries := l, nodupKeys := ⋯ })) ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
hl : l.NodupKeys
h : ¬c.fst ∈ { entries := l, nodupKeys := hl }
⊢ ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (insertRec H0 IH { entries := l, nodupKeys := ⋯ })) ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
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.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' ↦ s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise (fun a b ↦ a.keys.Disjoint b.keys) L

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun s s' ↦ s.fst ≠ s'.fst) l) ∧
      Pairwise (fun l₁ l₂ ↦ ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst ≠ y.fst) L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise (fun a b ↦ a.keys.Disjoint b.keys) L
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
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
this✝² : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}))
this✝¹ : Nonempty ↑(LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})).toTop
r_inf : T' ⟶ LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π' ≫ snd S' ℕ∪{∞}))
hπ'' : RegularEpi (lightProfiniteToLightCondSet.map π') := regularEpiOfEpi (lightProfiniteToLightCondSet.map π')
this✝ : EffectiveEpi π'
hπ' : RegularEpi (lightProfiniteToLightCondSet.map π') :=
  regularEpiOfPreserves π' lightProfiniteToLightCondSet (pullback.cone π' π') (pullback.isLimit π' π')
hc : Limits.IsColimit ((free R).mapCocone (Limits.Cofork.ofπ (lightProfiniteToLightCondSet.map π') ⋯))
this :
  LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' =
    LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)
⊢ (lightProfiniteToLightCondSet ⋙ free R).map
        (r_inf ≫
          LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
            π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞) ≫ y' ▷ ℕ∪{∞}) ≫
      f =
    (lightProfiniteToLightCondSet ⋙ free R).map
        (r_inf ≫
          LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫
            π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞) ≫ y' ▷ ℕ∪{∞}) ≫
      f

Tactic:
]

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

Goal state before:
pp: case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ (some y✝).isSome = true

Tactic:
]

Goal state after:
case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ (some y✝).isSome = true
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ some y✝ = some y✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
]

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

Goal state before:
pp: case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ s₁.entries.keys
⊢ (some y✝).isSome = true

Tactic:
]

Goal state after:
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
h'' : x✝ ∈ s₁.entries.keys
⊢ (some y✝).isSome = true
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mpr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ some y✝ = some y✝

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

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

Tactic:
]

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 : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ s₁.entries ~ s₂.entries
Module: Mathlib.Data.Finmap

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

Tactic:
]

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ dlookup a l = dlookup a l

pp: case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

pp: case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

Tactic:
]

Goal state after:
case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst

case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst
Module: Mathlib.Data.List.Sigma

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

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (lookupAll a l).length ≤ 1
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (map (Function.const (β a) ?m.47) (lookupAll a l)).Nodup

pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ Type ?u.50

pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ ?m.45

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ (map (Function.const (β a) ?m.47) (lookupAll a l)).Nodup

α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ Type ?u.50

α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
this : (map (Sigma.fst ∘ Sigma.mk a) (lookupAll a l)).Nodup
⊢ ?m.45
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 = (dlookup a l).toList

Tactic:
← head?_lookupAll

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (lookupAll a l).head?.toList
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 = (lookupAll a l).head?.toList

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (lookupAll a l).head?.toList
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:
]

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 α'
⊢ (flip fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y

Tactic:
]

Goal state after:
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
⊢ (flip fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a✝ : List α
⊢ (fun a ↦ h <$> ↑a) <$> Traversable.traverse g a✝ =
    ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝

Tactic:
]

Goal state after:
case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → G β
h : β → γ
a✝ : List α
⊢ (fun a ↦ h <$> ↑a) <$> Traversable.traverse g a✝ =
    ofList <$> (Functor.map (Functor.map h) ∘ Traversable.traverse g) a✝
Module: Mathlib.Data.Finmap

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

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ a ∉ s
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case h
G : Type u_1 → Type u_1
inst✝¹ : Applicative G
inst✝ : CommApplicative G
α β γ : Type u_1
g : α → β
h : β → G γ
a✝ : List α
⊢ ofList <$> Traversable.traverse h (List.map g a✝) = ofList <$> Traversable.traverse h (List.map g a✝)

Tactic:
]

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
⊢ (dlookup a l).toList.Nodup

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (dlookup a l).toList.Nodup
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∈ s₁
⊢ lookup a s₁ = lookup a s₁

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ none = none

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦∅⟧ ∪ ⟦s₁⟧ = ⟦s₁⟧
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ : Finmap β
s₁ : AList β
⊢ ⟦s₁⟧ ∪ ⟦∅⟧ = ⟦s₁⟧
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : α
b : β x
h : lookup x s = some b
⊢ some b = some b

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ ¬x = a

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ ¬x = a
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
⊢ x ∉ singleton a b

Tactic:
rwa [mem_singleton]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
h' : ¬x = a
this : x ∉ singleton a b
⊢ lookup x s = lookup x s

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ x.Disjoint y ∧ x.Disjoint z ↔ x.Disjoint y ∧ x.Disjoint z

Tactic:
]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x s₂
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂

Tactic:
]

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x s₂
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x s₂
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂

Tactic:
]

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x s₁ = lookup x s₂
hs₁ : x ∉ s₁
hs₂ : x ∈ s₂
⊢ lookup x s₁ = lookup x s₂
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∉ s₁
hs₂ : x ∉ s₂
⊢ none = none

Tactic:
]

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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (if t = ∅ then ∅ else s) = (image (const β✝) s).sup fun f ↦ image f t

Tactic:
]

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (if t = ∅ then ∅ else s) = (image (const β✝) s).sup fun f ↦ image f t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ a ∈ s ↔ ∃ i ∈ image (const β✝) s, a ∈ image i t

Tactic:
]

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ a ∈ s ↔ ∃ i ∈ image (const β✝) s, a ∈ image i t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
f : β✝ → α✝
hf : ∃ a ∈ s, const β✝ a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ s

Tactic:
]

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
f : β✝ → α✝
hf : ∃ a ∈ s, const β✝ a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ s
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
]

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (if s = ∅ then ∅ else t) = (image (const α✝ id) s).sup fun f ↦ image f t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
t : Finset β✝
⊢ ∅ = ∅

Tactic:
]

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ a ∈ t ↔ ∃ i ∈ image (const α✝ id) s, a ∈ image i t

Tactic:
]

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ a ∈ t ↔ ∃ i ∈ image (const α✝ id) s, a ∈ image i t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
ha : a ∈ t
⊢ a ∈ t

Tactic:
]

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
ha : a ∈ t
⊢ a ∈ t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
f : β✝ → β✝
hf : ∃ a ∈ s, const α✝ id a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ t

Tactic:
]

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
f : β✝ → β✝
hf : ∃ a ∈ s, const α✝ id a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ t
Module: Mathlib.Data.List.Sigma

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

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s ↦ decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x ↦ a == x.fst) l)
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((t i ×ˢ s.pi t).sup fun i_1 ↦ f i i_1.1 ⊓ s.attach.inf fun i_2 ↦ f (↑i_2) (i_1.2 ↑i_2 ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert ⟨i, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)

Tactic:
]

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((t i ×ˢ s.pi t).sup fun i_1 ↦ f i i_1.1 ⊓ s.attach.inf fun i_2 ↦ f (↑i_2) (i_1.2 ↑i_2 ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert ⟨i, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (s.biUnion fun a ↦ image (fun b ↦ (a, b)) t) = s.biUnion fun a ↦ image (fun b ↦ (a, b)) t

Tactic:
]

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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ (t.biUnion fun b ↦ image (fun a ↦ (a, b)) s) = t.biUnion fun b ↦ image (fun a ↦ (a, b)) s

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> pure s.val = pure s

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> pure s.val = pure s
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert.refine_1
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j = i ∨ j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j

Tactic:
]

Goal state after:
case insert.refine_1
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
h :
  ∀ (b : (a : ι) → a ∈ insert i s → κ a),
    (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
      f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
a : κ i
g : (a : ι) → a ∈ s → κ a
ha : a ∈ t i
hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a
aux : ∀ (j : ↥s), ↑j ≠ i
j : ι
hj✝ : j ∈ insert i s
hj : j = i ∨ j ∈ s
⊢ (if hji : j = i then cast ⋯ a else g j ⋯) ∈ t j
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ [].NodupKeys

Tactic:
]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l : List (Sigma β)
l' : List (Sigma β)
hl : [] = l'
⊢ [].NodupKeys