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

Goal state before:
pp: case pos
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
this : a ≠ s.fst → ¬f a = ⟨f s.fst, g s.fst s.snd⟩.fst
h✝ : a = s.fst
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))

pp: case neg
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
this : a ≠ s.fst → ¬f a = ⟨f s.fst, g s.fst s.snd⟩.fst
h✝ : ¬a = s.fst
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))

Tactic:
<;>

Goal state after:
case pos
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
this : a ≠ s.fst → ¬f a = ⟨f s.fst, g s.fst s.snd⟩.fst
h✝ : a = s.fst
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))

case neg
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup (f a) (map (Sigma.map f g) tail✝) = Option.map (g a) (dlookup a tail✝)
this : a ≠ s.fst → ¬f a = ⟨f s.fst, g s.fst s.snd⟩.fst
h✝ : ¬a = s.fst
⊢ dlookup (f a) (map (Sigma.map f g) (s :: tail✝)) = Option.map (g a) (dlookup a (s :: tail✝))
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
⊢ (map (Sigma.map id f) []).keys = [].keys

pp: case cons
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : (map (Sigma.map id f) tail✝).keys = tail✝.keys
⊢ (map (Sigma.map id f) (head✝ :: tail✝)).keys = (head✝ :: tail✝).keys

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
⊢ (map (Sigma.map id f) []).keys = [].keys

case cons
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : (map (Sigma.map id f) tail✝).keys = tail✝.keys
⊢ (map (Sigma.map id f) (head✝ :: tail✝)).keys = (head✝ :: tail✝).keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
h✝ : a = s.fst
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
h✝ : ¬a = s.fst
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
h✝ : a = s.fst
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : dlookup a (tail✝ ++ l₂) = (dlookup a tail✝).or (dlookup a l₂)
h✝ : ¬a = s.fst
⊢ dlookup a (s :: tail✝ ++ l₂) = (dlookup a (s :: tail✝)).or (dlookup a l₂)
Module: Mathlib.Data.Finset.DenselyOrdered

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

pp: case e'_2
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x✝ : α
⊢ (∀ y ∈ t, x✝ < y) ↔ x✝ < t.min' ht

Tactic:
<;>

Goal state after:
case e'_1
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x✝ : α
⊢ (∀ x ∈ s, x < x✝) ↔ s.max' hs < x✝

case e'_2
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
H : ∀ x ∈ s, ∀ y ∈ t, x < y
x✝ : α
⊢ (∀ y ∈ t, x✝ < y) ↔ x✝ < t.min' ht
Module: Mathlib.Data.Finset.DenselyOrdered

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

pp: case neg
α : 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
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

Tactic:
<;>

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

case neg
α : 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
⊢ ∃ b, (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y
Module: Mathlib.Data.List.Sigma

Goal state before:
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: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ [].length ≤ 1 → [] = [].head?.toList

pp: case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
⊢ [b].length ≤ 1 → [b] = [b].head?.toList

pp: case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
⊢ (b :: c :: l).length ≤ 1 → b :: c :: l = (b :: c :: l).head?.toList

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ [].length ≤ 1 → [] = [].head?.toList

case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
⊢ [b].length ≤ 1 → [b] = [b].head?.toList

case cons.cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l✝ : List (Sigma β)
h : l✝.NodupKeys
b c : β a
l : List (β a)
⊢ (b :: c :: l).length ≤ 1 → b :: c :: l = (b :: c :: l).head?.toList
Module: Mathlib.Data.List.Sigma

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

pp: case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
h1 : [b].length ≤ 1
⊢ [b] = [b].head?.toList

pp: case cons.cons
α : 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 = (b :: c :: l).head?.toList

Tactic:
<;>

Goal state after:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
h1 : [].length ≤ 1
⊢ [] = [].head?.toList

case cons.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
b : β a
h1 : [b].length ≤ 1
⊢ [b] = [b].head?.toList

case cons.cons
α : 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 = (b :: c :: l).head?.toList
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case h
α : Type u_1
a✝ : List α
⊢ traverse pure ⟦a✝⟧ = pure ⟦a✝⟧

Tactic:
simp [traverse]

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
  simp [Finset.erase, keys, AList.erase, keys_kerase]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
h : a = a₁
⊢ ⟨a₂, b₂⟩ ∈ some ⟨a, b⟩ → a₁ = a₂

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
h : ¬a = a₁
⊢ ⟨a₂, b₂⟩ ∈ none → a₁ = a₂

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
h : a = a₁
⊢ ⟨a₂, b₂⟩ ∈ some ⟨a, b⟩ → a₁ = a₂

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a₁ : α
b₂✝ : β a₁
a₂ : α
b₂ : β a₂
h : ¬a = a₁
⊢ ⟨a₂, b₂⟩ ∈ none → a₁ = a₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : a = x.fst
h₁ : z ∈ some ⟨a, b⟩
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ z = w

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : a = x.fst
h₁ : z ∈ some ⟨a, b⟩
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ z = w

pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : ¬a = x.fst
h₁ : z ∈ none
h✝ : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ z = w

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : ¬a = x.fst
h₁ : z ∈ none
h✝ : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ z = w

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : a = x.fst
h₁ : z ∈ some ⟨a, b⟩
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ z = w

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : a = x.fst
h₁ : z ∈ some ⟨a, b⟩
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ z = w

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : ¬a = x.fst
h₁ : z ∈ none
h✝ : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ z = w

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
z w : Sigma β
h_2 : ¬a = x.fst
h₁ : z ∈ none
h✝ : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ z = w
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ ⟨a, b⟩ = w

pp: case neg.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ ⟨a, b⟩ = w

Tactic:
<;>

Goal state after:
case pos.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ ⟨a, b⟩ = w

case neg.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ ⟨a, b⟩ = w
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
⊢ Pairwise
    (fun a_1 b_1 ↦
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst then some ⟨a, b⟩ else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst then some ⟨a, b⟩ else none) → a_1 = b_1 ∧ c = d)
    l₁

Tactic:
by
    refine nd.pairwise_ne.imp ?_
    intro x y h z h₁ w h₂
    split_ifs at h₁ h₂ with h_2 h_1 <;> cases h₁ <;> cases h₂
    exact (h (h_2.symm.trans h_1)).elim

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

pp: case neg
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : ¬x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)

case neg
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
y : Sigma β
ys : List (Sigma β)
tail_ih✝ : sizeOf (kerase x ys) ≤ sizeOf ys
h✝ : ¬x = y.fst
⊢ sizeOf (kerase x (y :: ys)) ≤ sizeOf (y :: ys)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
h : a = s.fst
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
h : ¬a = s.fst
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

Tactic:
<;>

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
h : a = s.fst
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
h : ¬a = s.fst
⊢ (kerase a (s :: tail✝)).kunion (kerase a l) = kerase a ((s :: tail✝).kunion l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case cons.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
tail✝ : List (Sigma β)
l₂ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, s.fst ∈ tail✝.keys → dlookup s.fst (tail✝.kunion l₂) = dlookup s.fst tail✝
⊢ dlookup s.fst ((s :: tail✝).kunion l₂) = dlookup s.fst (s :: tail✝)

pp: case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
⊢ dlookup a ((s :: tail✝).kunion l₂) = dlookup a (s :: tail✝)

Tactic:
<;>

Goal state after:
case cons.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Sigma β
tail✝ : List (Sigma β)
l₂ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, s.fst ∈ tail✝.keys → dlookup s.fst (tail✝.kunion l₂) = dlookup s.fst tail✝
⊢ dlookup s.fst ((s :: tail✝).kunion l₂) = dlookup s.fst (s :: tail✝)

case cons.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ tail✝.keys
⊢ dlookup a ((s :: tail✝).kunion l₂) = dlookup a (s :: tail✝)
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b ∈ none, decide (b ≠ 0) = true) ↔ none.getD 0 ≠ 0

pp: case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
val✝ : M
⊢ (∃ b ∈ some val✝, decide (b ≠ 0) = true) ↔ (some val✝).getD 0 ≠ 0

Tactic:
<;>

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b ∈ none, decide (b ≠ 0) = true) ↔ none.getD 0 ≠ 0

case some
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
val✝ : M
⊢ (∃ b ∈ some val✝, decide (b ≠ 0) = true) ↔ (some val✝).getD 0 ≠ 0
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ none.getD 0 = x ↔ x ∈ none

pp: case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
m : M
⊢ (some m).getD 0 = x ↔ x ∈ some m

Tactic:
<;>

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ none.getD 0 = x ↔ x ∈ none

case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
m : M
⊢ (some m).getD 0 = x ↔ x ∈ some m
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ none.getD 0 = 0 ↔ none = none ∨ 0 ∈ none

pp: case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
⊢ (some m).getD 0 = 0 ↔ some m = none ∨ 0 ∈ some m

Tactic:
<;>

Goal state after:
case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
⊢ none.getD 0 = 0 ↔ none = none ∨ 0 ∈ none

case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
⊢ (some m).getD 0 = 0 ↔ some m = none ∨ 0 ∈ some m
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
h : b = a
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b

pp: case neg
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
h : ¬b = a
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
h : b = a
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b

case neg
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
m : M
b : α
h : ¬b = a
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑1 = 1

pp: case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑(-1) = 1

Tactic:
<;>

Goal state after:
case inl
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑1 = 1

case inr
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ abv ↑(-1) = 1
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑1 = 1

pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑(-1) = 1

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑1 = 1

case inr
R : Type u_1
S : Type u_2
inst✝⁴ : Ring R
inst✝³ : CommRing S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ abv ↑↑(-1) = 1
Module: Mathlib.Data.Int.AbsoluteValue

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (1 • y) = abv y

pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (-1 • y) = abv y

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (1 • y) = abv y

case inr
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
abv : AbsoluteValue R S
y : R
⊢ abv (-1 • y) = abv y
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case hp
m n : ℕ
⊢ ∀ (i n : ℕ), (↑i).bodd = ((n + i).bodd ^^ n.bodd)

pp: case hn
m n : ℕ
⊢ ∀ (i m : ℕ), -[i+1].bodd = (m.bodd ^^ (m + i + 1).bodd)

Tactic:
<;>

Goal state after:
case hp
m n : ℕ
⊢ ∀ (i n : ℕ), (↑i).bodd = ((n + i).bodd ^^ n.bodd)

case hn
m n : ℕ
⊢ ∀ (i m : ℕ), -[i+1].bodd = (m.bodd ^^ (m + i + 1).bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case hp
m n i j : ℕ
⊢ (↑i).bodd = ((j + i).bodd ^^ j.bodd)

pp: case hn
m n i j : ℕ
⊢ -[i+1].bodd = (j.bodd ^^ (j + i + 1).bodd)

Tactic:
<;>

Goal state after:
case hp
m n i j : ℕ
⊢ (↑i).bodd = ((j + i).bodd ^^ j.bodd)

case hn
m n i j : ℕ
⊢ -[i+1].bodd = (j.bodd ^^ (j + i + 1).bodd)