internlm/Lean-Github huggingface dataset:
Theorem: List.remove_subset
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.182431 → Type ?u.182433
α : Type u_1
β : Type ?u.182439
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l : List α
⊢ remove a l ⊆ l
Tactic:
simp[subset_def, mem_remove_iff]
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.182431 → Type ?u.182433
α : Type u_1
β : Type ?u.182439
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {a_1 : α}, a_1 ∈ l → ¬a_1 = a → a_1 ∈ l
Theorem: List.remove_subset
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.182431 → Type ?u.182433
α : Type u_1
β : Type ?u.182439
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {a_1 : α}, a_1 ∈ l → ¬a_1 = a → a_1 ∈ l
Tactic:
intros
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.182431 → Type ?u.182433
α : Type u_1
β : Type ?u.182439
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l : List α
a✝² : α
a✝¹ : a✝² ∈ l
a✝ : ¬a✝² = a
⊢ a✝² ∈ l
Theorem: List.remove_subset
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.182431 → Type ?u.182433
α : Type u_1
β : Type ?u.182439
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l : List α
a✝² : α
a✝¹ : a✝² ∈ l
a✝ : ¬a✝² = a
⊢ a✝² ∈ l
Tactic:
simp[*]
Proof state after:
no goals
Theorem: List.remove_subset_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ remove a l₁ ⊆ remove a l₂
Tactic:
simp[subset_def, mem_remove_iff]
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ ∀ {a_1 : α}, a_1 ∈ l₁ → ¬a_1 = a → a_1 ∈ l₂ ∧ ¬a_1 = a
Theorem: List.remove_subset_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ ∀ {a_1 : α}, a_1 ∈ l₁ → ¬a_1 = a → a_1 ∈ l₂ ∧ ¬a_1 = a
Tactic:
intros
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂ ∧ ¬a✝² = a
Theorem: List.remove_subset_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂ ∧ ¬a✝² = a
Tactic:
simp[*]
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂
Theorem: List.remove_subset_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₂
Tactic:
exact h (by assumption)
Proof state after:
no goals
Theorem: List.remove_subset_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.186492 → Type ?u.186494
α : Type u_1
β : Type ?u.186500
inst✝¹ : Monad m
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
h : l₁ ⊆ l₂
a✝² : α
a✝¹ : a✝² ∈ l₁
a✝ : ¬a✝² = a
⊢ a✝² ∈ l₁
Tactic:
assumption
Proof state after:
no goals
Theorem: List.remove_cons_subset_cons_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
⊢ remove b (a :: l) ⊆ a :: remove b l
Tactic:
intro x
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x ∈ remove b (a :: l) → x ∈ a :: remove b l
Theorem: List.remove_cons_subset_cons_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x ∈ remove b (a :: l) → x ∈ a :: remove b l
Tactic:
simp[List.mem_remove_iff]
Proof state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x = a ∨ x ∈ l → ¬x = b → x = a ∨ x ∈ l ∧ ¬x = b
Theorem: List.remove_cons_subset_cons_remove
Proof state before:
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.191054 → Type ?u.191056
α : Type u_1
β : Type ?u.191062
inst✝¹ : Monad m
inst✝ : DecidableEq α
a b : α
l : List α
x : α
⊢ x = a ∨ x ∈ l → ¬x = b → x = a ∨ x ∈ l ∧ ¬x = b
Tactic:
rintro (rfl | hx) nex <;> simp[*]
Proof state after:
no goals
Theorem: List.remove_map_substet_map_remove
Proof state before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a : α
⊢ remove (f a) (map f l) ⊆ map f (remove a l)
Tactic:
simp[List.subset_def, List.mem_remove_iff]
Proof state after:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a : α
⊢ ∀ a_1 ∈ l, ¬f a_1 = f a → ∃ a_4, (a_4 ∈ l ∧ ¬a_4 = a) ∧ f a_4 = f a_1
Theorem: List.remove_map_substet_map_remove
Proof state before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a : α
⊢ ∀ a_1 ∈ l, ¬f a_1 = f a → ∃ a_4, (a_4 ∈ l ∧ ¬a_4 = a) ∧ f a_4 = f a_1
Tactic:
intro b hb neb
Proof state after:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a b : α
hb : b ∈ l
neb : ¬f b = f a
⊢ ∃ a_1, (a_1 ∈ l ∧ ¬a_1 = a) ∧ f a_1 = f b
Theorem: List.remove_map_substet_map_remove
Proof state before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a b : α
hb : b ∈ l
neb : ¬f b = f a
⊢ ∃ a_1, (a_1 ∈ l ∧ ¬a_1 = a) ∧ f a_1 = f b
Tactic:
exact ⟨b, ⟨hb, by rintro rfl; exact neb rfl⟩, rfl⟩
Proof state after:
no goals
Theorem: List.remove_map_substet_map_remove
Proof state before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
a b : α
hb : b ∈ l
neb : ¬f b = f a
⊢ ¬b = a
Tactic:
rintro rfl
Proof state after:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
b : α
hb : b ∈ l
neb : ¬f b = f b
⊢ False
Theorem: List.remove_map_substet_map_remove
Proof state before:
α✝ : Type u
inst✝⁵ : DecidableEq α✝
β✝ : Type v
inst✝⁴ : DecidableEq β✝
m : Type ?u.193416 → Type ?u.193418
α : Type u_1
β : Type u_2
inst✝³ : Monad m
inst✝² inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
l : List α
b : α
hb : b ∈ l
neb : ¬f b = f b
⊢ False
Tactic:
exact neb rfl
Proof state after:
no goals
Theorem: Vector.get_one
Proof state before:
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.tail.head
Tactic:
rw[←Vector.get_zero, Vector.get_tail_succ]
Proof state after:
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.get (Fin.succ 0)
Theorem: Vector.get_one
Proof state before:
α✝ : Type u_1
α : Type u_2
n : ℕ
v : Vector α (n + 2)
⊢ v.get 1 = v.get (Fin.succ 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: Vector.ofFn_vecCons
Proof state before:
α : Type u_1
n : ℕ
a : α
v : Fin n → α
⊢ ofFn (a :> v) = a ::ᵥ ofFn v
Tactic:
ext i
Proof state after:
case x
α : Type u_1
n : ℕ
a : α
v : Fin n → α
i : Fin n.succ
⊢ (ofFn (a :> v)).get i = (a ::ᵥ ofFn v).get i
Theorem: Vector.ofFn_vecCons
Proof state before:
case x
α : Type u_1
n : ℕ
a : α
v : Fin n → α
i : Fin n.succ
⊢ (ofFn (a :> v)).get i = (a ::ᵥ ofFn v).get i
Tactic:
cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: Finset.mem_rangeOfFinite_iff
Proof state before:
α : Type u
β : Type v
γ : Type w
ι : Sort v
inst✝ : Finite ι
f : ι → α
a : α
⊢ a ∈ rangeOfFinite f ↔ ∃ i, f i = a
Tactic:
simp[rangeOfFinite]
Proof state after:
no goals
Theorem: Finset.mem_imageOfFinset_iff
Proof state before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ b ∈ s.imageOfFinset f ↔ ∃ a, ∃ (ha : a ∈ s), f a ha = b
Tactic:
simp[imageOfFinset, mem_rangeOfFinite_iff]
Proof state after:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) ↔ ∃ a, ∃ (ha : a ∈ s), f a ha = b
Theorem: Finset.mem_imageOfFinset_iff
Proof state before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) ↔ ∃ a, ∃ (ha : a ∈ s), f a ha = b
Tactic:
constructor
Proof state after:
case mp
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) → ∃ a, ∃ (ha : a ∈ s), f a ha = b

case mpr
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a, ∃ (ha : a ∈ s), f a ha = b) → ∃ a ∈ s, ∃ (i : a ∈ s), f a i = b
Theorem: Finset.mem_imageOfFinset_iff
Proof state before:
case mp
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a ∈ s, ∃ (i : a ∈ s), f a i = b) → ∃ a, ∃ (ha : a ∈ s), f a ha = b
Tactic:
rintro ⟨a, _, ha, rfl⟩
Proof state after:
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
left✝ ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha
Theorem: Finset.mem_imageOfFinset_iff
Proof state before:
case mp.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
left✝ ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha
Tactic:
exact ⟨a, ha, rfl⟩
Proof state after:
no goals
Theorem: Finset.mem_imageOfFinset_iff
Proof state before:
case mpr
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
b : β
⊢ (∃ a, ∃ (ha : a ∈ s), f a ha = b) → ∃ a ∈ s, ∃ (i : a ∈ s), f a i = b
Tactic:
rintro ⟨a, ha, rfl⟩
Proof state after:
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1 ∈ s, ∃ (i : a_1 ∈ s), f a_1 i = f a ha
Theorem: Finset.mem_imageOfFinset_iff
Proof state before:
case mpr.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1 ∈ s, ∃ (i : a_1 ∈ s), f a_1 i = f a ha
Tactic:
exact ⟨a, ha, ha, rfl⟩
Proof state after:
no goals
Theorem: Finset.mem_imageOfFinset
Proof state before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ f a ha ∈ s.imageOfFinset f
Tactic:
simp[mem_imageOfFinset_iff]
Proof state after:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha
Theorem: Finset.mem_imageOfFinset
Proof state before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq β
s : Finset α
f : (a : α) → a ∈ s → β
a : α
ha : a ∈ s
⊢ ∃ a_1, ∃ (ha_1 : a_1 ∈ s), f a_1 ha_1 = f a ha
Tactic:
exact ⟨a, ha, rfl⟩
Proof state after:
no goals
Theorem: Finset.erase_union
Proof state before:
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ (s ∪ t).erase a = s.erase a ∪ t.erase a
Tactic:
ext
Proof state after:
case a
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
s t : Finset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).erase a ↔ a✝ ∈ s.erase a ∪ t.erase a
Theorem: Finset.erase_union
Proof state before:
case a
α : Type u
β : Type v
γ : Type w
inst✝ : DecidableEq α
a : α
s t : Finset α
a✝ : α
⊢ a✝ ∈ (s ∪ t).erase a ↔ a✝ ∈ s.erase a ∪ t.erase a
Tactic:
simp[and_or_left]
Proof state after:
no goals
Theorem: Finset.equiv_univ
Proof state before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype α'
inst✝ : DecidableEq α'
e : α ≃ α'
⊢ image (⇑e) univ = univ
Tactic:
ext x
Proof state after:
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype α'
inst✝ : DecidableEq α'
e : α ≃ α'
x : α'
⊢ x ∈ image (⇑e) univ ↔ x ∈ univ
Theorem: Finset.equiv_univ
Proof state before:
case a
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype α'
inst✝ : DecidableEq α'
e : α ≃ α'
x : α'
⊢ x ∈ image (⇑e) univ ↔ x ∈ univ
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.sup_univ_equiv
Proof state before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
α' : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
inst✝² : Fintype α'
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
e : α' ≃ α
⊢ (univ.sup fun i => f (e i)) = univ.sup f
Tactic:
simpa[Function.comp] using Eq.symm <| Finset.sup_image univ e f
Proof state after:
no goals
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
l : List σ
f : σ → α
⊢ (univ.sup fun i => f (l.get i)) = (List.map f l).sup
Tactic:
induction' l with s l ih <;> simp
Proof state after:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Tactic:
{ have : (Finset.univ : Finset (Fin $ l.length + 1)) = insert 0 ((Finset.univ : Finset (Fin l.length)).image Fin.succ) := by ext; simp
  rw[this, Finset.sup_insert, Finset.sup_image]; simp[Function.comp, ih] }
Proof state after:
no goals
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Tactic:
have : (Finset.univ : Finset (Fin $ l.length + 1)) = insert 0 ((Finset.univ : Finset (Fin l.length)).image Fin.succ) := by ext; simp
Proof state after:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ (univ.sup fun i => f ((s :: l).get i)) = f s ⊔ (List.map f l).sup
Tactic:
rw[this, Finset.sup_insert, Finset.sup_image]
Proof state after:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ f ((s :: l).get 0) ⊔ univ.sup ((fun i => f ((s :: l).get i)) ∘ Fin.succ) = f s ⊔ (List.map f l).sup
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
case cons
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
this : univ = insert 0 (image Fin.succ univ)
⊢ f ((s :: l).get 0) ⊔ univ.sup ((fun i => f ((s :: l).get i)) ∘ Fin.succ) = f s ⊔ (List.map f l).sup
Tactic:
simp[Function.comp, ih]
Proof state after:
no goals
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
⊢ univ = insert 0 (image Fin.succ univ)
Tactic:
ext
Proof state after:
case a
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
a✝ : Fin (l.length + 1)
⊢ a✝ ∈ univ ↔ a✝ ∈ insert 0 (image Fin.succ univ)
Theorem: Finset.sup_univ_list_eq_sup_map
Proof state before:
case a
α✝ : Type u
β : Type v
γ : Type w
σ : Type u_1
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : σ → α
s : σ
l : List σ
ih : (univ.sup fun i => f (l.get i)) = (List.map f l).sup
a✝ : Fin (l.length + 1)
⊢ a✝ ∈ univ ↔ a✝ ∈ insert 0 (image Fin.succ univ)
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.sup_univ_cast
Proof state before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : Fin n → α
n' : ℕ
h : n' = n
⊢ (univ.sup fun i => f (Fin.cast h i)) = univ.sup f
Tactic:
rcases h with rfl
Proof state after:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n' : ℕ
f : Fin n' → α
⊢ (univ.sup fun i => f (Fin.cast ⋯ i)) = univ.sup f
Theorem: Finset.sup_univ_cast
Proof state before:
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n' : ℕ
f : Fin n' → α
⊢ (univ.sup fun i => f (Fin.cast ⋯ i)) = univ.sup f
Tactic:
simp
Proof state after:
no goals
Theorem: Denumerable.lt_of_mem_list
Proof state before:
⊢ ∀ i ∈ ofNat (List ℕ) 0, i < 0
Tactic:
simp
Proof state after:
no goals
Theorem: Denumerable.lt_of_mem_list
Proof state before:
n : ℕ
this : n.unpair.2 < n + 1
⊢ ∀ i ∈ ofNat (List ℕ) (n + 1), i < n + 1
Tactic:
simp
Proof state after:
n : ℕ
this : n.unpair.2 < n + 1
⊢ n.unpair.1 < n + 1 ∧ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1
Theorem: Denumerable.lt_of_mem_list
Proof state before:
n : ℕ
this : n.unpair.2 < n + 1
⊢ n.unpair.1 < n + 1 ∧ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1
Tactic:
exact ⟨Nat.lt_succ_of_le (Nat.unpair_left_le n),
  by { intro i hi
       have : i < n.unpair.2 := lt_of_mem_list n.unpair.2 i hi
       exact lt_trans this (Nat.lt_succ_of_le $ Nat.unpair_right_le n) }⟩
Proof state after:
no goals
Theorem: Denumerable.lt_of_mem_list
Proof state before:
n : ℕ
this : n.unpair.2 < n + 1
⊢ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1
Tactic:
intro i hi
Proof state after:
n : ℕ
this : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
⊢ i < n + 1
Theorem: Denumerable.lt_of_mem_list
Proof state before:
n : ℕ
this : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
⊢ i < n + 1
Tactic:
have : i < n.unpair.2 := lt_of_mem_list n.unpair.2 i hi
Proof state after:
n : ℕ
this✝ : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
this : i < n.unpair.2
⊢ i < n + 1
Theorem: Denumerable.lt_of_mem_list
Proof state before:
n : ℕ
this✝ : n.unpair.2 < n + 1
i : ℕ
hi : i ∈ ofNat (List ℕ) n.unpair.2
this : i < n.unpair.2
⊢ i < n + 1
Tactic:
exact lt_trans this (Nat.lt_succ_of_le $ Nat.unpair_right_le n)
Proof state after:
no goals
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
x✝¹ : Vector α 0
x✝ : Fin 0 →. α
⊢ x✝¹ ∈ Vector.mOfFn x✝ ↔ ∀ (i : Fin 0), x✝¹.get i ∈ x✝ i
Tactic:
simp[Vector.mOfFn, Vector.eq_nil]
Proof state after:
no goals
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ w ∈ Vector.mOfFn v ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i
Tactic:
simp[Vector.mOfFn, @mem_vector_mOfFn _ n]
Proof state after:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i
Tactic:
exact ⟨by rintro ⟨a, ha, v, hv, rfl⟩ i; cases i using Fin.cases <;> simp[ha, hv],
  by intro h; exact ⟨w.head, by simpa using h 0, w.tail, fun i => by simpa using h i.succ, by simp⟩⟩
Proof state after:
no goals
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) → ∀ (i : Fin (n + 1)), w.get i ∈ v i
Tactic:
rintro ⟨a, ha, v, hv, rfl⟩ i
Proof state after:
case intro.intro.intro.intro
α : Type u_1
n : ℕ
v✝ : Fin (n + 1) →. α
a : α
ha : a ∈ v✝ 0
v : Vector α n
hv : ∀ (i : Fin n), v.get i ∈ v✝ i.succ
i : Fin (n + 1)
⊢ (a ::ᵥ v).get i ∈ v✝ i
Theorem: Part.mem_vector_mOfFn
Proof state before:
case intro.intro.intro.intro
α : Type u_1
n : ℕ
v✝ : Fin (n + 1) →. α
a : α
ha : a ∈ v✝ 0
v : Vector α n
hv : ∀ (i : Fin n), v.get i ∈ v✝ i.succ
i : Fin (n + 1)
⊢ (a ::ᵥ v).get i ∈ v✝ i
Tactic:
cases i using Fin.cases <;> simp[ha, hv]
Proof state after:
no goals
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∀ (i : Fin (n + 1)), w.get i ∈ v i) → ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1
Tactic:
intro h
Proof state after:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1
Tactic:
exact ⟨w.head, by simpa using h 0, w.tail, fun i => by simpa using h i.succ, by simp⟩
Proof state after:
no goals
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ w.head ∈ v 0
Tactic:
simpa using h 0
Proof state after:
no goals
Theorem: Part.mem_vector_mOfFn
Proof state before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
i : Fin n
⊢ w.tail.get i ∈ v i.succ
Tactic:
simpa using h i.succ
Proof state after:
no goals