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

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take m ⋯ fun i ↦ addCases u v i) = take m h u

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
x : α
⊢ x ∈ toList α

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : FinEnum α
⊢ (toList α).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Type ?u.19
β : Type ?u.20
f : α → β
inst✝¹ : DecidableEq α
inst✝ : FinEnum β
h : Injective f
⊢ ∀ (x : α), x ∈ List.filterMap (partialInv f) (toList β)

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
x : PUnit.{?u.8 + 1}
⊢ x ∈ [PUnit.unit]

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β✝ : α → Type v
β : Type ?u.23
inst✝¹ : FinEnum α
inst✝ : FinEnum β
x : α × β
⊢ x ∈ toList α ×ˢ toList β

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ ∀ (x : Fin n), x ∈ List.finRange n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take (n + m) ⋯ fun i ↦ addCases u v i) = fun i ↦ addCases u (take m h v) i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
m : ℕ
h : m ≤ n
v : Fin n → α
⊢ (List.ofFn (take m h v)).length = (List.take m (List.ofFn v)).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum.Option

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) → ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n✝ : ℕ
α : Type u_2
m : ℕ
h : m ≤ n✝
v : Fin n✝ → α
n : ℕ
h1 : n < (List.ofFn (take m h v)).length
h2 : n < (List.take m (List.ofFn v)).length
⊢ (List.ofFn (take m h v)).get ⟨n, h1⟩ = (List.take m (List.ofFn v)).get ⟨n, h2⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.ofFn (take m h l.get)).length = (List.take m l).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
n : ℕ
h1 : n < (List.ofFn (take m h l.get)).length
h2 : n < (List.take m l).length
⊢ (List.ofFn (take m h l.get)).get ⟨n, h1⟩ = (List.take m l).get ⟨n, h2⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.take m l).get = take m h l.get ∘ Fin.cast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α✝ : Fin n → Sort u_1
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).length = m

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : Finset α), x ∈ enum (toList α)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).get = take m h v ∘ Fin.cast ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Type v
inst✝¹ : (a : α) → FinEnum (β a)
inst✝ : Decidable α
h : α
x✝ : (a : α) ×' β a
a : α
Ba : β a
⊢ ⟨a, Ba⟩ ∈ List.map (PSigma.mk h) (toList (β h))

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u
β✝ : α✝ → Type v
α : Prop
β : α → Prop
inst✝¹ : Decidable α
inst✝ : (a : α) → Decidable (β a)
h : ∃ (a : α), β a
⊢ ∀ (x : (a : α) ×' β a), x ∈ [⟨⋯, ⋯⟩]

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
xs : List α
⊢ ∀ (x : { x // x ∈ xs }), x ∈ xs.attach

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : IsEmpty α
e : FinEnum α
⊢ e = { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : Unique α
e : FinEnum α
⊢ e = { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun a b ↦ decidableEq_of_subsingleton a b }

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

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
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 π')
⊢ EffectiveEpi π'

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ LeftInverse BitVec.ofFin BitVec.toFin

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
n : ℕ
⊢ RightInverse BitVec.ofFin BitVec.toFin

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u_1
inst✝¹ : FinEnum α
β : α → Type u_2
inst✝ : (a : α) → FinEnum (β a)
f : (a : α) → β a
⊢ f ∈ enum β

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α✝ : Type u_1
inst✝³ : FinEnum α✝
β : α✝ → Type u_2
inst✝² : (a : α✝) → FinEnum (β a)
p : Prop
inst✝¹ : Decidable p
α : p → Type
inst✝ : (hp : p) → FinEnum (α hp)
hp : ¬p
⊢ ∀ (x : (hp : p) → α hp), x ∈ [fun hp' ↦ ⋯.elim]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Vector

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ Finite (Vector α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Vector

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ Finite (Sym α n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Perm α) = (Nat.card α)!

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
hα : Nat.card α ≤ 2
⊢ IsCyclic (Perm α)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ IsMulCommutative (Perm α) ↔ Nat.card α ≤ 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → Option α
l : List α
acc : Array α
⊢ go f l acc = acc.toListAppend (lookmap f l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) = a :: lookmap f l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → Option α
a b : α
l : List α
h : f a = some b
⊢ lookmap f (a :: l) = b :: l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f g : α → Option α
a : α
l : List α
H : ∀ (a_1 : α), a_1 ∈ a :: l → f a_1 = g a_1
⊢ lookmap f (a :: l) = lookmap g (a :: l)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option α
g : α → β
h : ∀ (a b : α), b ∈ f a → g a = g b
a : α
l : List α
⊢ map g (lookmap f (a :: l)) = map g (a :: l)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
f : α → Option α
l : List α
⊢ (lookmap f l).length = l.length

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
l₁ : List (Sigma β)
h₁ : l₁.NodupKeys
l₂ : List (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.List.AList

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
⊢ s₁.keys ⊆ s₂.keys

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert a b s).entries = ⟨a, b⟩ :: s.entries

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  ext : 1; simp only [AList.entries_insert, List.kerase_cons_eq]

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

Tactic:
by

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

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

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

Tactic:
by

Goal state after:
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)
⊢ insertRec H0 IH ∅ = H0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 }
this :
  insertRec H0 IH { entries := c :: l, nodupKeys := ⋯ } ≍
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
⊢ insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) =
    IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })

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
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 π') ⋯))
⊢ (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π') ≫ snd S' ℕ∪{∞} =
    (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞} ≫ lift (𝟙 S') (CompHausLike.const S' ∞)) ≫
      snd S' ℕ∪{∞}

Tactic:
by

Goal state after:
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 : AList β
h : ¬c.fst ∈ l
⊢ insertRec H0 IH (insert c.fst c.snd l) = IH c.fst c.snd l h (insertRec H0 IH l)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : AList β
⊢ (s ∪ ∅).entries = s.entries

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ s₄ : AList β
p₁₂ : s₁.entries ~ s₂.entries
p₃₄ : s₃.entries ~ s₄.entries
⊢ (s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries

Tactic:
by

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : AList β
⊢ insert a b (s₁ ∪ s₂) = insert a b s₁ ∪ s₂

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after: