internlm/Lean-Github huggingface dataset:
Theorem: Finset.app_mapEquiv_symm
Proof state before:
case mk.intro.intro
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
y : α
left✝ : y ∈ s
hx : f y ∈ map f s
⊢ f.toFun ↑((mapEquiv s f).symm { val := f y, property := hx }) = ↑{ val := f y, property := hx }
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mapEquiv_of_app
Proof state before:
α' : Type ?u.103548
α : Type ?u.103533
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ s
Tactic:
simp at h
Proof state after:
α' : Type ?u.103548
α : Type ?u.103533
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : x ∈ s
⊢ x ∈ s
Theorem: Finset.mapEquiv_of_app
Proof state before:
α' : Type ?u.103548
α : Type ?u.103533
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : x ∈ s
⊢ x ∈ s
Tactic:
exact h
Proof state after:
no goals
Theorem: Finset.mapEquiv_of_app
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ (mapEquiv s f).symm { val := f x, property := h } = { val := x, property := ⋯ }
Tactic:
simp [mapEquiv]
Proof state after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ filter (fun x_1 => f x_1 = f x) s = {x}
Theorem: Finset.mapEquiv_of_app
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ filter (fun x_1 => f x_1 = f x) s = {x}
Tactic:
rw [eq_singleton_iff_unique_mem]
Proof state after:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ filter (fun x_1 => f x_1 = f x) s ∧ ∀ x_1 ∈ filter (fun x_2 => f x_2 = f x) s, x_1 = x
Theorem: Finset.mapEquiv_of_app
Proof state before:
α' : Type u_1
α : Type u_2
inst✝ : DecidableEq α'
s : Finset α
f : α ↪ α'
x : α
h : f x ∈ map f s
⊢ x ∈ filter (fun x_1 => f x_1 = f x) s ∧ ∀ x_1 ∈ filter (fun x_2 => f x_2 = f x) s, x_1 = x
Tactic:
simpa using h
Proof state after:
no goals
Theorem: Fintype.invFun_eq
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : α
⊢ (invFun f) x = y ↔ ↑x = f y
Tactic:
simp [invFun]
Proof state after:
no goals
Theorem: Fintype.eq_invFun
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : α
⊢ y = (invFun f) x ↔ f y = ↑x
Tactic:
simp [invFun]
Proof state after:
no goals
Theorem: Fintype.invFun_app
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
f' : α → α'
x : α
h : f' x ∈ Finset.map f Finset.univ
⊢ f' = f.toFun → (invFun f) { val := f' x, property := h } = x
Tactic:
rintro rfl
Proof state after:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : α
h : f.toFun x ∈ Finset.map f Finset.univ
⊢ (invFun f) { val := f.toFun x, property := h } = x
Theorem: Fintype.invFun_app
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : α
h : f.toFun x ∈ Finset.map f Finset.univ
⊢ (invFun f) { val := f.toFun x, property := h } = x
Tactic:
simp
Proof state after:
no goals
Theorem: Fintype.app_invFun
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
f' : α → α'
x : { x // x ∈ Finset.map f Finset.univ }
⊢ f' = f.toFun → f' ((invFun f) x) = ↑x
Tactic:
rintro rfl
Proof state after:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
⊢ f.toFun ((invFun f) x) = ↑x
Theorem: Fintype.app_invFun
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
⊢ f.toFun ((invFun f) x) = ↑x
Tactic:
simp [invFun, Finset.app_mapEquiv_symm]
Proof state after:
no goals
Theorem: Fintype.invFun_val_eq
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : α
⊢ (invFun f) x = y ↔ ↑x = f y
Tactic:
simp [invFun]
Proof state after:
no goals
Theorem: Fintype.invFun_eq_invFun
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ (invFun f) x = (invFun f') y ↔ ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
simp [invFun]
Proof state after:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y ↔ ∃ a, ↑x = f a ∧ ↑y = f' a
Theorem: Fintype.invFun_eq_invFun
Proof state before:
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y ↔ ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y → ∃ a, ↑x = f a ∧ ↑y = f' a

case mpr
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ (∃ a, ↑x = f a ∧ ↑y = f' a) → f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
Theorem: Fintype.invFun_eq_invFun
Proof state before:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y → ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ∃ a, ↑x = f a ∧ ↑y = f' a
Theorem: Fintype.invFun_eq_invFun
Proof state before:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ∃ a, ↑x = f a ∧ ↑y = f' a
Tactic:
refine ⟨_, ?_, h.symm⟩
Proof state after:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ↑x = f ↑((Finset.mapEquiv Finset.univ f).symm x)
Theorem: Fintype.invFun_eq_invFun
Proof state before:
case mp
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
h : f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
⊢ ↑x = f ↑((Finset.mapEquiv Finset.univ f).symm x)
Tactic:
simp [Finset.app_mapEquiv_symm]
Proof state after:
no goals
Theorem: Fintype.invFun_eq_invFun
Proof state before:
case mpr
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
⊢ (∃ a, ↑x = f a ∧ ↑y = f' a) → f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
Tactic:
rintro ⟨a,h,h'⟩
Proof state after:
case mpr.intro.intro
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
a : α
h : ↑x = f a
h' : ↑y = f' a
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
Theorem: Fintype.invFun_eq_invFun
Proof state before:
case mpr.intro.intro
α : Type u_1
α' : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α'
f f' : α ↪ α'
x : { x // x ∈ Finset.map f Finset.univ }
y : { x // x ∈ Finset.map f' Finset.univ }
a : α
h : ↑x = f a
h' : ↑y = f' a
⊢ f' ↑((Finset.mapEquiv Finset.univ f).symm x) = ↑y
Tactic:
simp_all
Proof state after:
no goals
Theorem: PNat.val_eq_val
Proof state before:
x y : ℕ+
⊢ ↑x = ↑y ↔ x = y
Tactic:
simp [PNat.val, Subtype.val_inj]
Proof state after:
no goals
Theorem: PNat.natPred_succ
Proof state before:
n : ℕ+
⊢ natPred n + 1 = ↑n
Tactic:
match n with
| ⟨_+1,_⟩ => simp
Proof state after:
no goals
Theorem: PNat.natPred_succ
Proof state before:
n : ℕ+
n✝ : ℕ
property✝ : 0 < n✝ + 1
⊢ natPred { val := n✝ + 1, property := property✝ } + 1 = ↑{ val := n✝ + 1, property := property✝ }
Tactic:
simp
Proof state after:
no goals
Theorem: Array.mem_finRange
Proof state before:
n : ℕ
x : Fin n
⊢ x ∈ finRange n
Tactic:
simp [finRange, mem_def]
Proof state after:
no goals
Theorem: top
Proof state before:
⊢ ⊤
Tactic:
trivial
Proof state after:
no goals
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c ↔ a ≤ bᶜ ⊔ c
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c → a ≤ bᶜ ⊔ c

case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜ ⊔ c → a ⊓ b ≤ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ≤ c → a ≤ bᶜ ⊔ c
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
⊢ a ≤ bᶜ ⊔ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
have : bᶜ ⊔ (a ⊓ b) ≤ bᶜ ⊔ c := sup_le_sup_left h bᶜ
Proof state after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : bᶜ ⊔ a ⊓ b ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : bᶜ ⊔ a ⊓ b ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
replace := le_trans le_sup_inf this
Proof state after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : (bᶜ ⊔ a) ⊓ (bᶜ ⊔ b) ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : (bᶜ ⊔ a) ⊓ (bᶜ ⊔ b) ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
simp only [compl_sup_eq_top, ge_iff_le, le_top, inf_of_le_left, sup_le_iff, le_sup_left,
  true_and] at this
Proof state after:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : a ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mp
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ⊓ b ≤ c
this : a ≤ bᶜ ⊔ c
⊢ a ≤ bᶜ ⊔ c
Tactic:
exact this
Proof state after:
no goals
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜ ⊔ c → a ⊓ b ≤ c
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ bᶜ ⊔ c
⊢ a ⊓ b ≤ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ bᶜ ⊔ c
⊢ a ⊓ b ≤ c
Tactic:
rw [sup_comm] at h
Proof state after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
⊢ a ⊓ b ≤ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
⊢ a ⊓ b ≤ c
Tactic:
have : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b := inf_le_inf_right b h
Proof state after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b
⊢ a ⊓ b ≤ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ (c ⊔ bᶜ) ⊓ b
⊢ a ⊓ b ≤ c
Tactic:
simp [inf_sup_right] at this
Proof state after:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ c
⊢ a ⊓ b ≤ c
Theorem: BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state before:
case mpr
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
h : a ≤ c ⊔ bᶜ
this : a ⊓ b ≤ c
⊢ a ⊓ b ≤ c
Tactic:
exact this
Proof state after:
no goals
Theorem: BooleanAlgebra.inf_compl_le_iff_le_sup
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ bᶜ ≤ c ↔ a ≤ b ⊔ c
Tactic:
conv => rhs; rhs; lhs; rw [← compl_compl b]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ bᶜ ≤ c ↔ a ≤ bᶜᶜ ⊔ c
Theorem: BooleanAlgebra.inf_compl_le_iff_le_sup
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ bᶜ ≤ c ↔ a ≤ bᶜᶜ ⊔ c
Tactic:
exact BooleanAlgebra.inf_le_iff_le_compl_sup
Proof state after:
no goals
Theorem: BooleanAlgebra.le_iff_inf_compl_le_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ ≤ ⊥
Tactic:
conv => lhs; rhs; rw [← compl_compl b]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥
Theorem: BooleanAlgebra.le_iff_inf_compl_le_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥
Tactic:
have : bᶜᶜ = bᶜᶜ ⊔ ⊥ := by exact (sup_bot_eq _).symm
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
this : bᶜᶜ = bᶜᶜ ⊔ ⊥
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥
Theorem: BooleanAlgebra.le_iff_inf_compl_le_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
this : bᶜᶜ = bᶜᶜ ⊔ ⊥
⊢ a ≤ bᶜᶜ ↔ a ⊓ bᶜ ≤ ⊥
Tactic:
rw [this]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
this : bᶜᶜ = bᶜᶜ ⊔ ⊥
⊢ a ≤ bᶜᶜ ⊔ ⊥ ↔ a ⊓ bᶜ ≤ ⊥
Theorem: BooleanAlgebra.le_iff_inf_compl_le_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
this : bᶜᶜ = bᶜᶜ ⊔ ⊥
⊢ a ≤ bᶜᶜ ⊔ ⊥ ↔ a ⊓ bᶜ ≤ ⊥
Tactic:
exact inf_le_iff_le_compl_sup.symm
Proof state after:
no goals
Theorem: BooleanAlgebra.le_iff_inf_compl_le_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ bᶜᶜ = bᶜᶜ ⊔ ⊥
Tactic:
exact (sup_bot_eq _).symm
Proof state after:
no goals
Theorem: BooleanAlgebra.le_iff_inf_compl_eq_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ = ⊥
Tactic:
rw [← le_bot_iff]
Proof state after:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ ≤ ⊥
Theorem: BooleanAlgebra.le_iff_inf_compl_eq_bot
Proof state before:
α : Type u_1
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ≤ b ↔ a ⊓ bᶜ ≤ ⊥
Tactic:
exact le_iff_inf_compl_le_bot
Proof state after:
no goals
Theorem: LeanSAT.Encode.satisfies_cardPred
Proof state before:
ν : Type u_1
lits : Multiset (Literal ν)
P : ℕ → Prop
inst✝ : DecidablePred P
τ : PropAssignment ν
⊢ cardPred lits P τ ↔ P (card lits τ)
Tactic:
unfold cardPred
Proof state after:
ν : Type u_1
lits : Multiset (Literal ν)
P : ℕ → Prop
inst✝ : DecidablePred P
τ : PropAssignment ν
⊢ P (card lits τ) ↔ P (card lits τ)
Theorem: LeanSAT.Encode.satisfies_cardPred
Proof state before:
ν : Type u_1
lits : Multiset (Literal ν)
P : ℕ → Prop
inst✝ : DecidablePred P
τ : PropAssignment ν
⊢ P (card lits τ) ↔ P (card lits τ)
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Encode.ofList_eq_map_get
Proof state before:
α : Type u_1
L : List α
⊢ ↑L = Multiset.map (fun i => List.get L i) Finset.univ.val
Tactic:
conv => lhs; rw [← List.finRange_map_get (l := L)]
Proof state after:
no goals
Theorem: LeanSAT.Encode.Tseitin.NegNormForm.const_toPropFun
Proof state before:
ν : Type u_1
b : Bool
⊢ toPropFun (const b) = if b = true then ⊤ else ⊥
Tactic:
ext τ
Proof state after:
case a
ν : Type u_1
b : Bool
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (const b) ↔ τ ⊨ if b = true then ⊤ else ⊥
Theorem: LeanSAT.Encode.Tseitin.NegNormForm.const_toPropFun
Proof state before:
case a
ν : Type u_1
b : Bool
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (const b) ↔ τ ⊨ if b = true then ⊤ else ⊥
Tactic:
cases b <;> simp [const, toPropFun]
Proof state after:
no goals
Theorem: LeanSAT.Encode.Tseitin.NegNormForm.toPropFun_ofPropForm
Proof state before:
ν : Type u_1
neg : Bool
f : PropForm ν
⊢ toPropFun (ofPropForm neg f) = if neg = true then ⟦PropForm.neg f⟧ else ⟦f⟧
Tactic:
induction f generalizing neg <;>
  aesop (add norm 1 simp ofPropForm)
        (add norm 1 simp toPropFun)
        (add norm 1 simp himp_eq)
        (add norm 1 simp PropFun.biImpl_eq_impls)
Proof state after:
no goals
Theorem: LeanSAT.Encode.Tseitin.NegNormForm.toPropFun_cleanup
Proof state before:
ν : Type u_1
f : NegNormForm ν
⊢ toPropFun (cleanup f) = toPropFun f
Tactic:
apply Eq.symm
Proof state after:
case h
ν : Type u_1
f : NegNormForm ν
⊢ toPropFun f = toPropFun (cleanup f)
Theorem: LeanSAT.Encode.Tseitin.NegNormForm.toPropFun_cleanup
Proof state before:
case h
ν : Type u_1
f : NegNormForm ν
⊢ toPropFun f = toPropFun (cleanup f)
Tactic:
induction f <;>
  aesop (add norm 1 simp ofPropForm)
        (add norm 1 simp toPropFun)
        (add norm 1 simp cleanup)
Proof state after:
no goals
Theorem: List.mem_set
Proof state before:
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h : x✝ ∈ set (head✝ :: bs) 0 x✝¹
⊢ x✝ ∈ head✝ :: bs ∨ x✝ = x✝¹
Tactic:
simp only [set, mem_cons] at h ⊢
Proof state after:
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h : x✝ = x✝¹ ∨ x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h : x✝ = x✝¹ ∨ x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
cases h
Proof state after:
case inl
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inl
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
right
Proof state after:
case inl.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inl.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_set
Proof state before:
case inr
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ (x✝ = head✝ ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
left
Proof state after:
case inr.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ = head✝ ∨ x✝ ∈ bs
Theorem: List.mem_set
Proof state before:
case inr.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ = head✝ ∨ x✝ ∈ bs
Tactic:
right
Proof state after:
case inr.h.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs
Theorem: List.mem_set
Proof state before:
case inr.h.h
α : Type u_1
head✝ : α
bs : List α
x✝¹ x✝ : α
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_set
Proof state before:
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set (b :: bs) (Nat.succ n) x✝¹
⊢ x✝ ∈ b :: bs ∨ x✝ = x✝¹
Tactic:
simp only [set, mem_cons] at h ⊢
Proof state after:
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ = b ∨ x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ = b ∨ x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
cases h
Proof state after:
case inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
. left; left; assumption
Proof state after:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
left
Proof state after:
case inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b ∨ x✝ ∈ bs
Theorem: List.mem_set
Proof state before:
case inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b ∨ x✝ ∈ bs
Tactic:
left
Proof state after:
case inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b
Theorem: List.mem_set
Proof state before:
case inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ = b
⊢ x✝ = b
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_set
Proof state before:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h✝ : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
rename _ => h
Proof state after:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
cases mem_set h
Proof state after:
case inr.inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹

case inr.inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inr.inl
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
left
Proof state after:
case inr.inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ = b ∨ x✝ ∈ bs
Theorem: List.mem_set
Proof state before:
case inr.inl.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ = b ∨ x✝ ∈ bs
Tactic:
right
Proof state after:
case inr.inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs
Theorem: List.mem_set
Proof state before:
case inr.inl.h.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ ∈ bs
⊢ x✝ ∈ bs
Tactic:
assumption
Proof state after:
no goals
Theorem: List.mem_set
Proof state before:
case inr.inr
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ (x✝ = b ∨ x✝ ∈ bs) ∨ x✝ = x✝¹
Tactic:
right
Proof state after:
case inr.inr.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹
Theorem: List.mem_set
Proof state before:
case inr.inr.h
α : Type u_1
b : α
bs : List α
n : Nat
x✝¹ x✝ : α
h : x✝ ∈ set bs n x✝¹
h✝ : x✝ = x✝¹
⊢ x✝ = x✝¹
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.init_zero
Proof state before:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ init 0 f = #[]
Tactic:
simp [init, Id.run, forIn', Std.Range.forIn']
Proof state after:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) 0 0 ⋯ #[] =
    #[]
Theorem: Array.init_zero
Proof state before:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) 0 0 ⋯ #[] =
    #[]
Tactic:
unfold Std.Range.forIn'.loop
Proof state after:
α✝ : Type u_1
f : Fin 0 → α✝
⊢ (if hu : 0 < { start := 0, stop := 0, step := 1 }.stop then
      match 0 with
      | 0 => pure #[]
      | Nat.succ fuel => do
        let __do_lift ← ForInStep.yield (push #[] (f { val := 0, isLt := ⋯ }))
        match __do_lift with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
              (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) fuel (0 + 1) ⋯ b
    else pure #[]) =
    #[]