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

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
i : α
has : i ∉ s
hfst : image f (insert i s) ⊆ t
hfs : Set.InjOn f ↑(insert i s)
hfat : f i ∈ t
⊢ ↑((g'.trans (Equiv.swap ⟨f i, hfat⟩ (g' i))) i) = f i

pp: case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i

Tactic:
·

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
s : Finset α
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
i : α
has : i ∉ s
hfst : image f (insert i s) ⊆ t
hfs : Set.InjOn f ↑(insert i s)
hfat : f i ∈ t
⊢ ↑((g'.trans (Equiv.swap ⟨f i, hfat⟩ (g' i))) i) = f i
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩

pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a

Tactic:
·

Goal state after:
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a

Tactic:
·

Goal state after:
case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a
Module: Mathlib.Data.Countable.Basic

Goal state before:
pp: α : Type u
β : Type v
π : α → Type w
inst✝¹ : Nonempty α
inst✝ : Uncountable β
inhabited_h : Inhabited α
⊢ Uncountable (α × β)

Tactic:
exact (Prod.mk_right_injective default).uncountable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ ↑i + 1 < n

Tactic:
by lia

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
⊢ ∀ (a b : Sym α 0), a = b

pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b

Tactic:
·

Goal state after:
case zero
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
⊢ ∀ (a b : Sym α 0), a = b
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b

Tactic:
·

Goal state after:
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
⊢ ∀ (a b : Sym α (n✝ + 1)), a = b
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b

pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Tactic:
·

Goal state after:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Tactic:
·

Goal state after:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
i : Fin 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n : ℕ
v : Vector α (n + 1)
i : Fin (n + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
·

Goal state after:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
i : Fin 0
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.succ.refine_1
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)

pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)

Tactic:
·

Goal state after:
case succ.succ.refine_1
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f (f b v.head) v.tail).get 0 =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get (Fin.castSucc 0)) ((v.head ::ᵥ v.tail).get 0)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)

Tactic:
·

Goal state after:
case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m

pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
·

Goal state after:
case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a ↑m else 0) + if a = a then count a ↑m else 0) = count a ↑m
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
·

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ b ∈ univ.erase i, #(s b)

pp: case neg
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
⊢ #({f ∈ piFinset s | f i = a}) = 0

Tactic:
·

Goal state after:
case pos
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ b ∈ univ.erase i, #(s b)
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case neg
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
⊢ #({f ∈ piFinset s | f i = a}) = 0

Tactic:
·

Goal state after:
case neg
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
⊢ #({f ∈ piFinset s | f i = a}) = 0
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ (a_1 : α), a_1 ∉ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a)

pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
·

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ (a_1 : α), a_1 ∉ filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1

Tactic:
·

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ ∀ a_1 ∈ ↑m.snd, a ≠ a_1
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ decode (encode s) = s

pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s

Tactic:
·

Goal state after:
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ decode (encode s) = s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s

Tactic:
·

Goal state after:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s

pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Tactic:
·

Goal state after:
case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s

Tactic:
·

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
⊢ encode (decode (Sum.inr s)) = Sum.inr s
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.pred ⋯)) a

pp: case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i + 1, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.castPred ⋯)) a

Tactic:
·

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.pred ⋯)) a
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
⊢ False

pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s

Tactic:
·

Goal state after:
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
⊢ False
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s

Tactic:
·

Goal state after:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Sum.inr (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = Sum.inr s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case refine_1
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ range (Subtype.val ∘ f) ⊆ s

pp: case refine_2
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Countable

pp: case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite

Tactic:
·

Goal state after:
case refine_1
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ range (Subtype.val ∘ f) ⊆ s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case refine_2
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Countable

pp: case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite

Tactic:
·

Goal state after:
case refine_2
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Countable
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite

Tactic:
·

Goal state after:
case refine_3
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Infinite
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx ↑⟨i, ⋯⟩).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a

pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length

pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Tactic:
·

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ((↑v).eraseIdx ↑⟨i, ⋯⟩).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j.succ, hj⟩.pred ⋯)) a
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mp
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) → ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤

pp: case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
·

Goal state after:
case mp
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) → ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length

pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Tactic:
·

Goal state after:
case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ < (↑v).length
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j

Tactic:
·

Goal state after:
case pos.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ ↑⟨i, ⋯⟩ ≤ j
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
·

Goal state after:
case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, f ↑x ⋯ = ∏ a, f ↑a ⋯

pp: case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯

Tactic:
·

Goal state after:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, f ↑x ⋯ = ∏ a, f ↑a ⋯
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯

Tactic:
·

Goal state after:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x, g ↑x ⋯ = ∏ a, g ↑a ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i + 1, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.castPred ⋯)) a

Tactic:
·

Goal state after:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i + 1, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.castPred ⋯)) a
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr.inl
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : ∅.Countable
hps : ∀ s ∈ ∅, p s
hS : sSup ∅ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

pp: case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
·

Goal state after:
case mpr.inl
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
hSc : ∅.Countable
hps : ∀ s ∈ ∅, p s
hS : sSup ∅ = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a

pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length

pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
·

Goal state after:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).eraseIdx i).insertIdx j a =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      j a
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
·

Goal state after:
case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length

pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
·

Goal state after:
case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ i < (↑v).length
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
·

Goal state after:
case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑i ≤ ↑j

pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ (↑⟨l, hl⟩).length

Tactic:
·

Goal state after:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑i ≤ ↑j
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ (↑⟨l, hl⟩).length

Tactic:
·

Goal state after:
case x
α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ ↑j ≤ (↑⟨l, hl⟩).length