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

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ (toSubtype' r ⊚ ofSubtype' r) Fin2.fz x = id Fin2.fz x

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝),
    (toSubtype' r ⊚ ofSubtype' r) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ (toSubtype' r ⊚ ofSubtype' r) a✝.fs x = id a✝.fs x

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ (toSubtype' r ⊚ ofSubtype' r) Fin2.fz x = id Fin2.fz x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝),
    (toSubtype' r ⊚ ofSubtype' r) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ (toSubtype' r ⊚ ofSubtype' r) a✝.fs x = id a✝.fs x
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = x✝¹ <$> x✝

pp: case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = mapConst x✝¹ x✝

Tactic:
<;>

Goal state after:
case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = x✝¹ <$> x✝

case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = mapConst x✝¹ x✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ ⟨↑x, ⋯⟩ = x

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝), toSubtype' r a✝ (ofSubtype' r a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ toSubtype' (dropFun r) a✝ (ofSubtype' (dropFun r) a✝ x) = x

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r Fin2.fz
⊢ ⟨↑x, ⋯⟩ = x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : Subtype_ r a✝), toSubtype' r a✝ (ofSubtype' r a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ r a✝.fs
⊢ toSubtype' (dropFun r) a✝ (ofSubtype' (dropFun r) a✝ x) = x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r Fin2.fz (prod.mk Fin2.fz x.1 x.2)) }
⊢ (subtypeVal r ⊚ toSubtype' r) Fin2.fz x = prod.mk Fin2.fz (↑x).1 (↑x).2

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop)
    (x : (fun i ↦ { x // ofRepeat (r i (prod.mk i x.1 x.2)) }) a✝),
    (subtypeVal r ⊚ toSubtype' r) a✝ x = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ (subtypeVal r ⊚ toSubtype' r) a✝.fs x = prod.mk a✝.fs (↑x).1 (↑x).2

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r Fin2.fz (prod.mk Fin2.fz x.1 x.2)) }
⊢ (subtypeVal r ⊚ toSubtype' r) Fin2.fz x = prod.mk Fin2.fz (↑x).1 (↑x).2

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop)
    (x : (fun i ↦ { x // ofRepeat (r i (prod.mk i x.1 x.2)) }) a✝),
    (subtypeVal r ⊚ toSubtype' r) a✝ x = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ (subtypeVal r ⊚ toSubtype' r) a✝.fs x = prod.mk a✝.fs (↑x).1 (↑x).2
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case h_fst
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      fst S ℕ∪{∞}

pp: case h_snd
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      snd S ℕ∪{∞}

Tactic:
<;>

Goal state after:
case h_fst
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ fst S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      fst S ℕ∪{∞}

case h_snd
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) := ⋯
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S := ⋯
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := ⋯
n : ↑ℕ∪{∞}.toTop
⊢ ((S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞})) ≫ π) ≫ snd S ℕ∪{∞} =
    (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
          (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n) ≫
        y' ▷ ℕ∪{∞}) ≫
      snd S ℕ∪{∞}
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ x ∈ (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g) ↔ f ≤ x ∧ x ≤ g

Tactic:
refine (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), x i ∈ (f.rangeIcc g) i) ↔ f ≤ x ∧ x ≤ g
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: case neg.nil
b : Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) []
h2 : ¬Even [].length
⊢ 2 * count b [] =
    if Even [].length then [].length else if (some b == [].head?) = true then [].length + 1 else [].length - 1

pp: case neg.cons
b x : Bool
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ 2 * count b (x :: l) =
    if Even (x :: l).length then (x :: l).length
    else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1

Tactic:
· exact (h2 .zero).elim

Goal state after:
case neg.cons
b x : Bool
l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) (x :: l)
h2 : ¬Even (x :: l).length
⊢ 2 * count b (x :: l) =
    if Even (x :: l).length then (x :: l).length
    else if (some b == (x :: l).head?) = true then (x :: l).length + 1 else (x :: l).length - 1
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ toDFinsupp (replicate 1 a) = DFinsupp.single a 1

Tactic:
toDFinsupp_replicate

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ DFinsupp.single a 1 = DFinsupp.single a 1
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Tactic:
by
  rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_5
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this✝ : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
σ' : ↑ℕ∪{∞}.toTop → ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop → ↑(pullback π (y' ▷ ℕ∪{∞})).toTop :=
  fun n ↦
    ⇑(ConcreteCategory.hom
        (pullback.lift π (y' ▷ ℕ∪{∞}) (S'π n ≫ LightProfinite.fibreIncl n (π ≫ snd S ℕ∪{∞}))
          (lift (𝟙 (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))))
            (CompHausLike.const (LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))) n))
          ⋯))
hσ :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).1 = s
hσ' :
  ∀ (x : ↑ℕ∪{∞}.toTop) (s : ↑(LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π))).toTop),
    ((ConcreteCategory.hom π') (σ' x s)).2 = x
this : CompactSpace ↑(fibres (⇑(ConcreteCategory.hom π')) σ')
⊢ Epi (cover ({ hom := TopCat.ofHom { toFun := Subtype.val, continuous_toFun := ⋯ } } ≫ π'))

Tactic:
rw [LightProfinite.epi_iff_surjective]
    exact coverToFun_surjective _ _ hσ hσ'

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case inl
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : α
⊢ Sum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

pp: case inr
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : β
⊢ Sum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

Tactic:
<;>

Goal state after:
case inl
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : α
⊢ Sum.inl val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)

case inr
α : Type u
β✝ : α → Type v
β : Type ?u.12
inst✝¹ : FinEnum α
inst✝ : FinEnum β
val✝ : β
⊢ Sum.inr val✝ ∈ List.map Sum.inl (toList α) ++ List.map Sum.inr (toList β)
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case none
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) =
    match none with
    | none => a :: lookmap f l
    | some b => b :: l

pp: case some
α : Type u_1
f : α → Option α
a : α
l : List α
val✝ : α
h : f a = some val✝
⊢ lookmap f (a :: l) =
    match some val✝ with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
<;>

Goal state after:
case none
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) =
    match none with
    | none => a :: lookmap f l
    | some b => b :: l

case some
α : Type u_1
f : α → Option α
a : α
l : List α
val✝ : α
h : f a = some val✝
⊢ lookmap f (a :: l) =
    match some val✝ with
    | none => a :: lookmap f l
    | some b => b :: l
Module: Mathlib.Data.List.Lookmap

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

pp: case swap.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
<;>

Goal state after:
case swap.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
h₁ : f a = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

case swap.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
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 β)
h : (c :: l).NodupKeys
⊢ C { entries := c :: l, nodupKeys := h }

Tactic:
rw [mk_cons_eq_insert]

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 β)
h : (c :: l).NodupKeys
⊢ C (insert c.fst c.snd { entries := l, nodupKeys := ⋯ })
Module: Mathlib.Data.List.AList

Goal state before:
pp: case H0
α : Type u
β : α → Type v
inst✝ : DecidableEq α
⊢ True

pp: case IH
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a✝² : α
b✝ : β a✝²
l✝ : AList β
a✝¹ : ¬a✝² ∈ l✝
a✝ : True
⊢ True

Tactic:
<;>

Goal state after:
case H0
α : Type u
β : α → Type v
inst✝ : DecidableEq α
⊢ True

case IH
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a✝² : α
b✝ : β a✝²
l✝ : AList β
a✝¹ : ¬a✝² ∈ l✝
a✝ : True
⊢ True
Module: Mathlib.Data.List.AList

Goal state before:
pp: case e'_1.e'_3
α : 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)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l

pp: case e'_2.e'_3
α : 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)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
e_1✝ :
  C (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    C { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ }
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l

Tactic:
<;>

Goal state after:
case e'_1.e'_3
α : 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)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l

case e'_2.e'_3
α : 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)
l : List (Sigma β)
hl : l.NodupKeys
fst✝ : α
snd✝ : β fst✝
h : ¬⟨fst✝, snd✝⟩.fst ∈ { entries := l, nodupKeys := hl }
this :
  insertRec H0 IH { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ } ≍
    IH ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl } h
      (insertRec H0 IH { entries := l, nodupKeys := hl })
e_1✝ :
  C (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }) =
    C { entries := ⟨fst✝, snd✝⟩ :: l, nodupKeys := ⋯ }
⊢ (insert ⟨fst✝, snd✝⟩.fst ⟨fst✝, snd✝⟩.snd { entries := l, nodupKeys := hl }).entries = ⟨fst✝, snd✝⟩ :: l
Module: Mathlib.Data.List.AList

Goal state before:
pp: case left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s

pp: case right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s

Tactic:
<;>

Goal state after:
case left
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s

case right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s
Module: Mathlib.Data.List.AList

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

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

Tactic:
<;>

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

case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝ →
    dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
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:
nodupKeys_iff_pairwise,

Goal state after:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise (fun s s' ↦ s.fst ≠ s'.fst) L.flatten ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise Disjoint (map keys L)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
h✝ : a = s.fst
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
h✝ : ¬a = s.fst
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
h✝ : a = s.fst
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : (dlookup a tail✝).isSome = true ↔ a ∈ tail✝.keys
h✝ : ¬a = s.fst
⊢ (dlookup a (s :: tail✝)).isSome = true ↔ a ∈ (s :: tail✝).keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
h✝ : a = s.fst
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
h✝ : ¬a = s.fst
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
h✝ : a = s.fst
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : b ∈ dlookup a tail✝ → ⟨a, b⟩ ∈ tail✝
h✝ : ¬a = s.fst
⊢ b ∈ dlookup a (s :: tail✝) → ⟨a, b⟩ ∈ s :: tail✝
Module: Mathlib.Data.List.Sigma

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

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : ¬s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : Option.map (Sigma.mk a) (dlookup a tail✝) = find? (fun s ↦ decide (a = s.fst)) tail✝
h✝ : ¬s.fst = a
⊢ Option.map (Sigma.mk a) (dlookup a (s :: tail✝)) = find? (fun s ↦ decide (a = s.fst)) (s :: tail✝)