internlm/Lean-Github huggingface dataset:
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ f (v 0) ∧ f (conj (vecTail v)) ↔ ∀ (i : Fin (n + 1)), f (v i)
Tactic:
simp[ih]
Proof state after:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) ↔ ∀ (i : Fin (n + 1)), f (v i)
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) ↔ ∀ (i : Fin (n + 1)), f (v i)
Tactic:
constructor
Proof state after:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) → ∀ (i : Fin (n + 1)), f (v i)

case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (∀ (i : Fin (n + 1)), f (v i)) → f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) → ∀ (i : Fin (n + 1)), f (v i)
Tactic:
intro ⟨hz, hs⟩ i
Proof state after:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i : Fin (n + 1)
⊢ f (v i)
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i : Fin (n + 1)
⊢ f (v i)
Tactic:
cases i using Fin.cases
Proof state after:
case succ.mp.zero
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
⊢ f (v 0)

case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mp.zero
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
⊢ f (v 0)

case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Tactic:
{ exact hz }
Proof state after:
case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Tactic:
{ exact hs _ }
Proof state after:
no goals
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mp.zero
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
⊢ f (v 0)
Tactic:
exact hz
Proof state after:
no goals
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Tactic:
exact hs _
Proof state after:
no goals
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (∀ (i : Fin (n + 1)), f (v i)) → f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)
Tactic:
intro h
Proof state after:
case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
h : ∀ (i : Fin (n + 1)), f (v i)
⊢ f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)
Theorem: Matrix.conj_hom_prop
Proof state before:
case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
h : ∀ (i : Fin (n + 1)), f (v i)
⊢ f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)
Tactic:
exact ⟨h 0, fun i => h _⟩
Proof state after:
no goals
Theorem: Matrix.hom_conj
Proof state before:
β : Type u_3
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
n : ℕ
inst✝¹ : FunLike F α β
inst✝ : LogicalConnective.HomClass F α β
f : F
v : Fin n → α
⊢ f (conj v) = conj (⇑f ∘ v)
Tactic:
induction' n with n ih <;> simp[*, conj]
Proof state after:
no goals
Theorem: List.map_conj
Proof state before:
α : Type u_1
inst✝² : LogicalConnective α
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
l : List α
⊢ f l.conj ↔ ∀ a ∈ l, f a
Tactic:
induction l <;> simp[*]
Proof state after:
no goals
Theorem: List.map_conj_append
Proof state before:
α : Type u_1
inst✝² : LogicalConnective α
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
l₁ l₂ : List α
⊢ f (l₁ ++ l₂).conj ↔ f (l₁.conj ⋏ l₂.conj)
Tactic:
induction l₁ <;> induction l₂ <;> aesop
Proof state after:
no goals
Theorem: List.map_disj
Proof state before:
α : Type u_1
inst✝² : LogicalConnective α
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
l : List α
⊢ f l.disj ↔ ∃ a ∈ l, f a
Tactic:
induction l <;> simp[*]
Proof state after:
no goals
Theorem: List.map_disj_append
Proof state before:
α : Type u_1
inst✝² : LogicalConnective α
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
l₁ l₂ : List α
⊢ f (l₁ ++ l₂).disj ↔ f (l₁.disj ⋎ l₂.disj)
Tactic:
induction l₁ <;> induction l₂ <;> aesop
Proof state after:
no goals
Theorem: List.conj'_cons_nonempty
Proof state before:
F : Type u
inst✝ : LogicalConnective F
p q a : F
as : List F
h : as ≠ []
⊢ (a :: as).conj' = a ⋏ as.conj'
Tactic:
cases as with
| nil => contradiction;
| cons q rs => simp [List.conj']
Proof state after:
no goals
Theorem: List.conj'_cons_nonempty
Proof state before:
case nil
F : Type u
inst✝ : LogicalConnective F
p q a : F
h : [] ≠ []
⊢ [a].conj' = a ⋏ [].conj'
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.conj'_cons_nonempty
Proof state before:
case cons
F : Type u
inst✝ : LogicalConnective F
p q✝ a q : F
rs : List F
h : q :: rs ≠ []
⊢ (a :: q :: rs).conj' = a ⋏ (q :: rs).conj'
Tactic:
simp [List.conj']
Proof state after:
no goals
Theorem: List.disj'_cons_nonempty
Proof state before:
F : Type u
inst✝ : LogicalConnective F
p q a : F
as : List F
h : as ≠ []
⊢ (a :: as).disj' = a ⋎ as.disj'
Tactic:
cases as with
| nil => contradiction;
| cons q rs => simp [List.disj']
Proof state after:
no goals
Theorem: List.disj'_cons_nonempty
Proof state before:
case nil
F : Type u
inst✝ : LogicalConnective F
p q a : F
h : [] ≠ []
⊢ [a].disj' = a ⋎ [].disj'
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.disj'_cons_nonempty
Proof state before:
case cons
F : Type u
inst✝ : LogicalConnective F
p q✝ a q : F
rs : List F
h : q :: rs ≠ []
⊢ (a :: q :: rs).disj' = a ⋎ (q :: rs).disj'
Tactic:
simp [List.disj']
Proof state after:
no goals
Theorem: List.induction_with_singleton
Proof state before:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
⊢ ∀ (as : List F), motive as
Tactic:
intro as
Proof state after:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
as : List F
⊢ motive as
Theorem: List.induction_with_singleton
Proof state before:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
as : List F
⊢ motive as
Tactic:
induction as with
| nil => exact hnil;
| cons a as ih => cases as with
  | nil => exact hsingle a;
  | cons b bs => exact hcons a (b :: bs) (by simp) ih;
Proof state after:
no goals
Theorem: List.induction_with_singleton
Proof state before:
case nil
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
⊢ motive []
Tactic:
exact hnil
Proof state after:
no goals
Theorem: List.induction_with_singleton
Proof state before:
case cons
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a : F
as : List F
ih : motive as
⊢ motive (a :: as)
Tactic:
cases as with
| nil => exact hsingle a;
| cons b bs => exact hcons a (b :: bs) (by simp) ih;
Proof state after:
no goals
Theorem: List.induction_with_singleton
Proof state before:
case cons.nil
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a : F
ih : motive []
⊢ motive [a]
Tactic:
exact hsingle a
Proof state after:
no goals
Theorem: List.induction_with_singleton
Proof state before:
case cons.cons
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a b : F
bs : List F
ih : motive (b :: bs)
⊢ motive (a :: b :: bs)
Tactic:
exact hcons a (b :: bs) (by simp) ih
Proof state after:
no goals
Theorem: List.induction_with_singleton
Proof state before:
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
a b : F
bs : List F
ih : motive (b :: bs)
⊢ b :: bs ≠ []
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.map_conj
Proof state before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s : Finset α
⊢ f (⋀s) ↔ ∀ a ∈ s, f a
Tactic:
simpa using List.map_conj f s.toList
Proof state after:
no goals
Theorem: Finset.map_conj_union
Proof state before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ f (⋀(s₁ ∪ s₂)) ↔ f (⋀s₁ ⋏ ⋀s₂)
Tactic:
simp [map_conj]
Proof state after:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a) ↔ (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a
Theorem: Finset.map_conj_union
Proof state before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a) ↔ (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a
Tactic:
constructor
Proof state after:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a) → (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a

case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a) → ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
Theorem: Finset.map_conj_union
Proof state before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a) → (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a

case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a) → ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
Tactic:
. intro h;
  constructor;
  . intro a ha;
    exact h a (Or.inl ha);
  . intro a ha;
    exact h a (Or.inr ha);
Proof state after:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a) → ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
Theorem: Finset.map_conj_union
Proof state before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a) → ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
Tactic:
. intro ⟨h₁, h₂⟩ a ha;
  cases ha <;> simp_all;
Proof state after:
no goals
Theorem: Finset.map_conj_union
Proof state before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a) → (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a
Tactic:
intro h
Proof state after:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a
Theorem: Finset.map_conj_union
Proof state before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a
Tactic:
constructor
Proof state after:
case mp.left
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₁, f a

case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Theorem: Finset.map_conj_union
Proof state before:
case mp.left
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₁, f a

case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Tactic:
. intro a ha;
  exact h a (Or.inl ha);
Proof state after:
case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Theorem: Finset.map_conj_union
Proof state before:
case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Tactic:
. intro a ha;
  exact h a (Or.inr ha);
Proof state after:
no goals
Theorem: Finset.map_conj_union
Proof state before:
case mp.left
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₁, f a
Tactic:
intro a ha
Proof state after:
case mp.left
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₁
⊢ f a
Theorem: Finset.map_conj_union
Proof state before:
case mp.left
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₁
⊢ f a
Tactic:
exact h a (Or.inl ha)
Proof state after:
no goals
Theorem: Finset.map_conj_union
Proof state before:
case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Tactic:
intro a ha
Proof state after:
case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₂
⊢ f a
Theorem: Finset.map_conj_union
Proof state before:
case mp.right
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₂
⊢ f a
Tactic:
exact h a (Or.inr ha)
Proof state after:
no goals
Theorem: Finset.map_conj_union
Proof state before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a) → ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
Tactic:
intro ⟨h₁, h₂⟩ a ha
Proof state after:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h₁ : ∀ a ∈ s₁, f a
h₂ : ∀ a ∈ s₂, f a
a : α
ha : a ∈ s₁ ∨ a ∈ s₂
⊢ f a
Theorem: Finset.map_conj_union
Proof state before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
h₁ : ∀ a ∈ s₁, f a
h₂ : ∀ a ∈ s₂, f a
a : α
ha : a ∈ s₁ ∨ a ∈ s₂
⊢ f a
Tactic:
cases ha <;> simp_all
Proof state after:
no goals
Theorem: Finset.map_disj
Proof state before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s : Finset α
⊢ f (⋁s) ↔ ∃ a ∈ s, f a
Tactic:
simpa using List.map_disj f s.toList
Proof state after:
no goals
Theorem: Finset.map_disj_union
Proof state before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ f (⋁(s₁ ∪ s₂)) ↔ f (⋁s₁ ⋎ ⋁s₂)
Tactic:
simp [map_disj]
Proof state after:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) ↔ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Theorem: Finset.map_disj_union
Proof state before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) ↔ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
constructor
Proof state after:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Theorem: Finset.map_disj_union
Proof state before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. rintro ⟨a, h₁ | h₂, hb⟩;
  . left; use a;
  . right; use a;
Proof state after:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a