internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Cnf.toPropFun_addClause
Proof state before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
τ : PropAssignment ν
⊢ (∀ (C_1 : Clause L), C_1 ∈ f.data ∨ C_1 = C → τ ⊨ Clause.toPropFun C_1) ↔
    (∀ C ∈ f.data, τ ⊨ Clause.toPropFun C) ∧ τ ⊨ Clause.toPropFun C
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Cnf.toPropFun_and
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
⊢ toPropFun (and f1 f2) = toPropFun f1 ⊓ toPropFun f2
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (and f1 f2) ↔ τ ⊨ toPropFun f1 ⊓ toPropFun f2
Theorem: LeanSAT.Cnf.toPropFun_and
Proof state before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (and f1 f2) ↔ τ ⊨ toPropFun f1 ⊓ toPropFun f2
Tactic:
simp [satisfies_iff, Array.mem_def, and]
Proof state after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ (∀ (C : Clause L), C ∈ f1.data ∨ C ∈ f2.data → τ ⊨ Clause.toPropFun C) ↔
    (∀ C ∈ f1.data, τ ⊨ Clause.toPropFun C) ∧ ∀ C ∈ f2.data, τ ⊨ Clause.toPropFun C
Theorem: LeanSAT.Cnf.toPropFun_and
Proof state before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ (∀ (C : Clause L), C ∈ f1.data ∨ C ∈ f2.data → τ ⊨ Clause.toPropFun C) ↔
    (∀ C ∈ f1.data, τ ⊨ Clause.toPropFun C) ∧ ∀ C ∈ f2.data, τ ⊨ Clause.toPropFun C
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Cnf.toPropFun_not
Proof state before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
c : Clause L
inst✝ : LawfulLitVar L ν
⊢ toPropFun (not c) = (Clause.toPropFun c)ᶜ
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
c : Clause L
inst✝ : LawfulLitVar L ν
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (not c) ↔ τ ⊨ (Clause.toPropFun c)ᶜ
Theorem: LeanSAT.Cnf.toPropFun_not
Proof state before:
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ : DecidableEq ν
c : Clause L
inst✝ : LawfulLitVar L ν
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (not c) ↔ τ ⊨ (Clause.toPropFun c)ᶜ
Tactic:
simp [satisfies_iff, Clause.satisfies_iff, LitVar.satisfies_iff,
  not, Array.mem_def, Bool.eq_not_iff]
Proof state after:
no goals
Theorem: LeanSAT.Cnf.toPropFun_any
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
⊢ toPropFun (any ls) = PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (any ls) ↔ τ ⊨ PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))
Theorem: LeanSAT.Cnf.toPropFun_any
Proof state before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (any ls) ↔ τ ⊨ PropFun.any ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
simp [any, toPropFun, Clause.toPropFun]
Proof state after:
no goals
Theorem: LeanSAT.Cnf.toPropFun_all
Proof state before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
⊢ toPropFun (all ls) = PropFun.all ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
ext τ
Proof state after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (all ls) ↔ τ ⊨ PropFun.all ↑(List.map LitVar.toPropFun (Array.toList ls))
Theorem: LeanSAT.Cnf.toPropFun_all
Proof state before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
ls : Array L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (all ls) ↔ τ ⊨ PropFun.all ↑(List.map LitVar.toPropFun (Array.toList ls))
Tactic:
simp [satisfies_iff, Clause.satisfies_iff, LitVar.satisfies_iff,
  all, Array.mem_def]
Proof state after:
no goals
Theorem: Bool.bnot_eq_bnot
Proof state before:
a b : Bool
⊢ (!a) = !b ↔ a = b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Bool.eq_true_iff_eq_true
Proof state before:
a b : Bool
⊢ (a = true ↔ b = true) ↔ a = b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Bool.eq_false_iff_eq_false
Proof state before:
a b : Bool
⊢ (a = false ↔ b = false) ↔ a = b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Bool.bnot_eq
Proof state before:
a b : Bool
⊢ (!a) = b ↔ ¬a = b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Bool.eq_bnot
Proof state before:
a b : Bool
⊢ a = !b ↔ ¬a = b
Tactic:
cases a <;> cases b <;> decide
Proof state after:
no goals
Theorem: Nat.eq_or_lt_of_lt_succ
Proof state before:
m n : ℕ
⊢ m < n + 1 → m = n ∨ m < n
Tactic:
intro h
Proof state after:
m n : ℕ
h : m < n + 1
⊢ m = n ∨ m < n
Theorem: Nat.eq_or_lt_of_lt_succ
Proof state before:
m n : ℕ
h : m < n + 1
⊢ m = n ∨ m < n
Tactic:
rcases eq_or_lt_of_le (Nat.le_of_lt_succ h) with (rfl | h)
Proof state after:
case inl
m : ℕ
h : m < m + 1
⊢ m = m ∨ m < m

case inr
m n : ℕ
h✝ : m < n + 1
h : m < n
⊢ m = n ∨ m < n
Theorem: Nat.eq_or_lt_of_lt_succ
Proof state before:
case inl
m : ℕ
h : m < m + 1
⊢ m = m ∨ m < m
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: Nat.eq_or_lt_of_lt_succ
Proof state before:
case inr
m n : ℕ
h✝ : m < n + 1
h : m < n
⊢ m = n ∨ m < n
Tactic:
exact Or.inr h
Proof state after:
no goals
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
i : ℤ
⊢ (0 < -i ↔ 0 < i) → i = 0
Tactic:
intro h
Proof state after:
i : ℤ
h : 0 < -i ↔ 0 < i
⊢ i = 0
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
i : ℤ
h : 0 < -i ↔ 0 < i
⊢ i = 0
Tactic:
by_cases hLt : 0 < i
Proof state after:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
⊢ i = 0

case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
⊢ i = 0

case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Tactic:
. have := h.mpr hLt; linarith
Proof state after:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Tactic:
. have : ¬ 0 < -i := fun h₂ => hLt (h.mp h₂); linarith
Proof state after:
no goals
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
⊢ i = 0
Tactic:
have := h.mpr hLt
Proof state after:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
this : 0 < -i
⊢ i = 0
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
case pos
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : 0 < i
this : 0 < -i
⊢ i = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
⊢ i = 0
Tactic:
have : ¬ 0 < -i := fun h₂ => hLt (h.mp h₂)
Proof state after:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
this : ¬0 < -i
⊢ i = 0
Theorem: Int.eq_zero_of_lt_neg_iff_lt
Proof state before:
case neg
i : ℤ
h : 0 < -i ↔ 0 < i
hLt : ¬0 < i
this : ¬0 < -i
⊢ i = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Quotient.elim_mk
Proof state before:
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ elim ⟦a⟧ f h = f a ⋯
Tactic:
simp [elim]
Proof state after:
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ Trunc.lift (fun x => f ↑x ⋯) ⋯ (toTrunc ⟦a⟧) = f a ⋯
Theorem: Quotient.elim_mk
Proof state before:
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ Trunc.lift (fun x => f ↑x ⋯) ⋯ (toTrunc ⟦a⟧) = f a ⋯
Tactic:
apply Trunc.lift_mk
Proof state after:
no goals
Theorem: Multiset.elim_mk
Proof state before:
α : Type u_1
β : Type u_2
L : List α
f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb
⊢ elim ⟦L⟧ f h = f L ⋯
Tactic:
simp [elim]
Proof state after:
α : Type u_1
β : Type u_2
L : List α
f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb
⊢ Quotient.elim ⟦L⟧ f h = f L ⋯
Theorem: Multiset.elim_mk
Proof state before:
α : Type u_1
β : Type u_2
L : List α
f : (L' : List α) → ⟦L'⟧ = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ⟦a⟧ = ⟦L⟧) (hb : ⟦b⟧ = ⟦L⟧), f a ha = f b hb
⊢ Quotient.elim ⟦L⟧ f h = f L ⋯
Tactic:
apply Trunc.lift_mk
Proof state after:
no goals
Theorem: Multiset.elim_eq_forall
Proof state before:
α : Type u_1
β : Type u_2
s : Multiset α
f : (L : List α) → ↑L = s → β
h : ∀ (a b : List α) (ha : ↑a = s) (hb : ↑b = s), f a ha = f b hb
motive : Prop
hmotive : ∀ {L : List α} {hL : ↑L = s}, elim s f h = f L hL → motive
⊢ motive
Tactic:
induction s using Quotient.inductionOn with | _ L =>
exact hmotive rfl
Proof state after:
no goals
Theorem: Multiset.elim_eq_forall
Proof state before:
case h
α : Type u_1
β : Type u_2
motive : Prop
L : List α
f : (L_1 : List α) → ↑L_1 = ⟦L⟧ → β
h : ∀ (a b : List α) (ha : ↑a = ⟦L⟧) (hb : ↑b = ⟦L⟧), f a ha = f b hb
hmotive : ∀ {L_1 : List α} {hL : ↑L_1 = ⟦L⟧}, elim ⟦L⟧ f h = f L_1 hL → motive
⊢ motive
Tactic:
exact hmotive rfl
Proof state after:
no goals
Theorem: Fin.succFin_of_ne
Proof state before:
n : ℕ
i : Fin n
⊢ ↑i + 1 ≠ n → ↑i + 1 < n
Tactic:
intro hi
Proof state after:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
⊢ ↑i + 1 < n
Theorem: Fin.succFin_of_ne
Proof state before:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
⊢ ↑i + 1 < n
Tactic:
have := i.isLt
Proof state after:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
⊢ ↑i + 1 < n
Theorem: Fin.succFin_of_ne
Proof state before:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
⊢ ↑i + 1 < n
Tactic:
rcases eq_or_lt_of_le (Nat.succ_le_of_lt this) with (h | h)
Proof state after:
case inl
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i = n
⊢ ↑i + 1 < n

case inr
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i < n
⊢ ↑i + 1 < n
Theorem: Fin.succFin_of_ne
Proof state before:
case inl
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i = n
⊢ ↑i + 1 < n
Tactic:
exact absurd h hi
Proof state after:
no goals
Theorem: Fin.succFin_of_ne
Proof state before:
case inr
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i < n
⊢ ↑i + 1 < n
Tactic:
exact h
Proof state after:
no goals
Theorem: Finset.elim_eq_forall
Proof state before:
α : Type u_1
β : Type u_2
s : Finset α
f : (L : List α) → ↑L = s.val → β
h : ∀ (a b : List α) (ha : ↑a = s.val) (hb : ↑b = s.val), f a ha = f b hb
motive : Prop
hmotive : ∀ {L : List α} {hL : ↑L = s.val}, elim s f h = f L hL → motive
⊢ motive
Tactic:
rcases s with ⟨s,h⟩
Proof state after:
case mk
α : Type u_1
β : Type u_2
motive : Prop
s : Multiset α
h✝ : Multiset.Nodup s
f : (L : List α) → ↑L = { val := s, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := s, nodup := h✝ }.val) (hb : ↑b = { val := s, nodup := h✝ }.val), f a ha = f b hb
hmotive : ∀ {L : List α} {hL : ↑L = { val := s, nodup := h✝ }.val}, elim { val := s, nodup := h✝ } f h = f L hL → motive
⊢ motive
Theorem: Finset.elim_eq_forall
Proof state before:
case mk
α : Type u_1
β : Type u_2
motive : Prop
s : Multiset α
h✝ : Multiset.Nodup s
f : (L : List α) → ↑L = { val := s, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := s, nodup := h✝ }.val) (hb : ↑b = { val := s, nodup := h✝ }.val), f a ha = f b hb
hmotive : ∀ {L : List α} {hL : ↑L = { val := s, nodup := h✝ }.val}, elim { val := s, nodup := h✝ } f h = f L hL → motive
⊢ motive
Tactic:
induction s using Quotient.inductionOn with | _ L =>
exact hmotive rfl
Proof state after:
no goals
Theorem: Finset.elim_eq_forall
Proof state before:
case mk.h
α : Type u_1
β : Type u_2
motive : Prop
L : List α
h✝ : Multiset.Nodup ⟦L⟧
f : (L_1 : List α) → ↑L_1 = { val := ⟦L⟧, nodup := h✝ }.val → β
h :
  ∀ (a b : List α) (ha : ↑a = { val := ⟦L⟧, nodup := h✝ }.val) (hb : ↑b = { val := ⟦L⟧, nodup := h✝ }.val),
    f a ha = f b hb
hmotive :
  ∀ {L_1 : List α} {hL : ↑L_1 = { val := ⟦L⟧, nodup := h✝ }.val},
    elim { val := ⟦L⟧, nodup := h✝ } f h = f L_1 hL → motive
⊢ motive
Tactic:
exact hmotive rfl
Proof state after:
no goals
Theorem: Fintype.elim_elems_eq_forall
Proof state before:
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ C
Tactic:
apply Multiset.elim_eq_forall (motive := C)
Proof state after:
V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ ∀ {L : List ?m.10905} {hL : ↑L = ?m.10907}, Multiset.elim ?m.10907 ?m.10908 ?m.10909 = ?m.10908 L hL → C

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Type ?u.10903

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Type ?u.10904

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ Multiset ?m.10905

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ (L : List ?m.10905) → ↑L = ?m.10907 → ?m.10906

V : Type u_1
β : Type u_2
inst✝ : Fintype V
f : (L : List V) → (∀ (v : V), v ∈ L) → List.Nodup L → β
h :
  ∀ (L1 : List V) (h1 : ∀ (v : V), v ∈ L1) (h11 : List.Nodup L1) (L2 : List V) (h2 : ∀ (v : V), v ∈ L2)
    (h22 : List.Nodup L2), f L1 h1 h11 = f L2 h2 h22
C : Prop
h' : ∀ (L : List V) (h1 : ∀ (v : V), v ∈ L) (h2 : List.Nodup L), elim_elems f h = f L h1 h2 → C
⊢ ∀ (a b : List ?m.10905) (ha : ↑a = ?m.10907) (hb : ↑b = ?m.10907), ?m.10908 a ha = ?m.10908 b hb
Theorem: Finset.biUnion_union
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
⊢ Finset.biUnion (s1 ∪ s2) f = Finset.biUnion s1 f ∪ Finset.biUnion s2 f
Tactic:
ext b
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ b ∈ Finset.biUnion (s1 ∪ s2) f ↔ b ∈ Finset.biUnion s1 f ∪ Finset.biUnion s2 f
Theorem: Finset.biUnion_union
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ b ∈ Finset.biUnion (s1 ∪ s2) f ↔ b ∈ Finset.biUnion s1 f ∪ Finset.biUnion s2 f
Tactic:
simp only [mem_biUnion, mem_union]
Proof state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) ↔ (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a
Theorem: Finset.biUnion_union
Proof state before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) ↔ (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a
Tactic:
constructor
Proof state after:
case a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) → (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a

case a.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ ((∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a) → ∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a
Theorem: Finset.biUnion_union
Proof state before:
case a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) → (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a
Tactic:
rintro ⟨a,b|b⟩
Proof state after:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a

case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a
Theorem: Finset.biUnion_union
Proof state before:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a
Tactic:
refine Or.inl ⟨a,?_⟩
Proof state after:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ a ∈ s1 ∧ b✝ ∈ f a
Theorem: Finset.biUnion_union
Proof state before:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ a ∈ s1 ∧ b✝ ∈ f a
Tactic:
simp only [and_self, *]
Proof state after:
no goals
Theorem: Finset.biUnion_union
Proof state before:
case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a
Tactic:
refine Or.inr ⟨a,?_⟩
Proof state after:
case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ a ∈ s2 ∧ b✝ ∈ f a
Theorem: Finset.biUnion_union
Proof state before:
case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ a ∈ s2 ∧ b✝ ∈ f a
Tactic:
simp only [and_self, *]
Proof state after:
no goals
Theorem: Finset.biUnion_union
Proof state before:
case a.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ ((∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a) → ∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a
Tactic:
rintro (⟨a,b,c⟩|⟨a,b,c⟩)
  <;> refine ⟨a, ?_⟩
Proof state after:
case a.mpr.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s1
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a

case a.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s2
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a
Theorem: Finset.biUnion_union
Proof state before:
case a.mpr.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s1
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a
Tactic:
simp only [and_self, true_or, *]
Proof state after:
no goals
Theorem: Finset.biUnion_union
Proof state before:
case a.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s2
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a
Tactic:
simp only [and_self, or_true, *]
Proof state after:
no goals
Theorem: Finset.getUnique_eq
Proof state before:
α : Type u_1
xs : Finset α
h : ∃ x, xs = {x}
v : α
⊢ getUnique xs h = v ↔ xs = {v}
Tactic:
rcases h with ⟨x,rfl⟩
Proof state after:
case intro
α : Type u_1
v x : α
⊢ getUnique {x} ⋯ = v ↔ {x} = {v}
Theorem: Finset.getUnique_eq
Proof state before:
case intro
α : Type u_1
v x : α
⊢ getUnique {x} ⋯ = v ↔ {x} = {v}
Tactic:
simp [getUnique]
Proof state after:
case intro
α : Type u_1
v x : α
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v
Theorem: Finset.getUnique_eq
Proof state before:
case intro
α : Type u_1
v x : α
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v
Tactic:
apply elim_eq_forall
Proof state after:
case intro.hmotive
α : Type u_1
v x : α
⊢ ∀ {L : List ?intro.α} {hL : ↑L = ?intro.s.val},
    elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL →
      (elim {x}
            (fun L _hL =>
              match L, _hL with
              | [], _hL => ⋯.elim
              | x_1 :: tail, _hL => x_1)
            ⋯ =
          v ↔
        x = v)

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb
Theorem: Finset.getUnique_eq
Proof state before:
case intro.hmotive
α : Type u_1
v x : α
⊢ ∀ {L : List ?intro.α} {hL : ↑L = ?intro.s.val},
    elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL →
      (elim {x}
            (fun L _hL =>
              match L, _hL with
              | [], _hL => ⋯.elim
              | x_1 :: tail, _hL => x_1)
            ⋯ =
          v ↔
        x = v)

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb
Tactic:
intro L hL heq
Proof state after:
case intro.hmotive
α : Type u_1
v x : α
L : List ?intro.α
hL : ↑L = ?intro.s.val
heq : elim ?intro.s ?intro.f ?intro.h = ?intro.f L hL
⊢ elim {x}
        (fun L _hL =>
          match L, _hL with
          | [], _hL => ⋯.elim
          | x_1 :: tail, _hL => x_1)
        ⋯ =
      v ↔
    x = v

case intro.α
α : Type u_1
v x : α
⊢ Type ?u.15504

case intro.β
α : Type u_1
v x : α
⊢ Type ?u.15505

case intro.s
α : Type u_1
v x : α
⊢ Finset ?intro.α

case intro.f
α : Type u_1
v x : α
⊢ (L : List ?intro.α) → ↑L = ?intro.s.val → ?intro.β

case intro.h
α : Type u_1
v x : α
⊢ ∀ (a b : List ?intro.α) (ha : ↑a = ?intro.s.val) (hb : ↑b = ?intro.s.val), ?intro.f a ha = ?intro.f b hb