harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_measurableEquiv_injective (e : α ≃ᵐ β) : Injective (Measure.map e)

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ Injective (map ⇑e)

Tactic:
intro μ₁ μ₂ hμ

Result:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e) μ₁ = map (⇑e) μ₂
⊢ μ₁ = μ₂

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e.symm) (map (⇑e) μ₁) = map (⇑e.symm) (map (⇑e) μ₂)
⊢ μ₁ = μ₂

Tactic:
simpa [map_symm_map e] using hμ

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e) μ₁ = map (⇑e) μ₂
⊢ μ₁ = μ₂

Tactic:
apply_fun Measure.map e.symm at hμ

Result:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μ₁ μ₂ : Measure α
hμ : map (⇑e.symm) (map (⇑e) μ₁) = map (⇑e.symm) (map (⇑e) μ₂)
⊢ μ₁ = μ₂
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_codRestrict [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h p') :
    Submodule.map (codRestrict p f h) p' = comap p.subtype (p'.map f) :=
  Submodule.ext fun ⟨x, hx⟩ => by simp [Subtype.ext_iff_val]

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring R₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
σ₂₁ : R₂ →+* R
inst✝ : RingHomSurjective σ₂₁
p : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ (c : M₂), f c ∈ p
p' : Submodule R₂ M₂
x✝ : ↥p
x : M
hx : x ∈ p
⊢ ⟨x, hx⟩ ∈ map (codRestrict p f h) p' ↔ ⟨x, hx⟩ ∈ comap p.subtype (map f p')

Tactic:
simp [Subtype.ext_iff_val]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1S_mono (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0)
    (h_add : FinMeasAdditive μ T)
    (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f g : α →₁ₛ[μ] G''}
    (hfg : f ≤ g) : setToL1S T f ≤ setToL1S T g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T (g - f)

Tactic:
exact setToL1S_nonneg h_zero h_add hT_nonneg hfg

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(simpleFunc G'' 1 μ)
hfg : f ≤ g
⊢ setToL1S T f ≤ setToL1S T g

Tactic:
rw [← sub_nonneg] at hfg ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T g - setToL1S T f

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T g - setToL1S T f

Tactic:
rw [← setToL1S_sub h_zero h_add]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝³ : NormedLatticeAddCommGroup G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : NormedLatticeAddCommGroup G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f g : ↥(simpleFunc G'' 1 μ)
hfg : 0 ≤ g - f
⊢ 0 ≤ setToL1S T (g - f)
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
lemma forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C] [HasForget.{w} C]
    [Category.{v'} D] [HasForget.{w} D] [HasForget₂ C D] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget₂ C D).obj X) :
    ((forget₂ C D).map (f ≫ g) x) =
      (forget₂ C D).map g ((forget₂ C D).map f x)

Proof state:
C : Type u
D : Type u'
inst✝⁴ : Category.{v, u} C
inst✝³ : HasForget C
inst✝² : Category.{v', u'} D
inst✝¹ : HasForget D
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : (forget D).obj ((forget₂ C D).obj X)
⊢ ((forget₂ C D).map (f ≫ g)) x = ((forget₂ C D).map g) (((forget₂ C D).map f) x)

Tactic:
rw [Functor.map_comp, comp_apply]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_one (k : ℕ) : multichoose 1 k = 1

Proof state:
case zero

⊢ multichoose 1 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
k : ℕ
IH : multichoose 1 k = 1
⊢ multichoose 1 (k + 1) = 1

Tactic:
simp [multichoose_succ_succ 0 k, IH]

Result:
no goals

Proof state:
k : ℕ
⊢ multichoose 1 k = 1

Tactic:
induction' k with k IH

Result:
case zero

⊢ multichoose 1 0 = 1

case succ
k : ℕ
IH : multichoose 1 k = 1
⊢ multichoose 1 (k + 1) = 1
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.clm_comp (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) :
    HasDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
⊢ HasDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') univ x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') univ x

Tactic:
exact hc.clm_comp hd

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
@[simp] lemma subset_compl_singleton : s ⊆ {a}ᶜ ↔ a ∉ s

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ s ⊆ {a}ᶜ ↔ a ∉ s

Tactic:
rw [subset_compl_comm, singleton_subset_iff, mem_compl]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem image_const_add_Ioc : (fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c)

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c : M
⊢ (fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ioc]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_iSup (f : ι → G.Subgraph) :
    (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem finrank_add_finrank_orthogonal (b₁ : B.IsRefl) (W : Submodule K V) :
    finrank K W + finrank K (B.orthogonal W) =
      finrank K V + finrank K (W ⊓ B.orthogonal ⊤ : Subspace K V)

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
rw [← toLin_restrict_ker_eq_inf_orthogonal _ _ b₁, ←
  toLin_restrict_range_dualCoannihilator_eq_orthogonal _ _, finrank_map_subtype_eq]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥W + finrank K ↥(range (domRestrict B W)).dualCoannihilator =
    finrank K V + finrank K ↥(ker (domRestrict B W))

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥W + finrank K ↥(range (domRestrict B W)).dualCoannihilator =
    finrank K V + finrank K ↥(ker (domRestrict B W))

Tactic:
conv_rhs =>
  rw [← @Subspace.finrank_add_finrank_dualCoannihilator_eq K V _ _ _ _
      (LinearMap.range (B.domRestrict W)),
    add_comm, ← add_assoc, add_comm (finrank K (LinearMap.ker (B.domRestrict W))),
    LinearMap.finrank_range_add_finrank_ker]

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem perm_insertIdx_iff_of_le {l₁ l₂ : List α} {m n : ℕ} (hm : m ≤ l₁.length)
    (hn : n ≤ l₂.length) (a : α) : insertIdx m a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
m n : ℕ
hm : m ≤ l₁.length
hn : n ≤ l₂.length
a : α
⊢ insertIdx m a l₁ ~ insertIdx n a l₂ ↔ l₁ ~ l₂

Tactic:
rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_image₂_image₂_comm {γ δ : Type*} {u : Finset γ} {v : Finset δ} [DecidableEq ζ]
    [DecidableEq ζ'] [DecidableEq ν] {f : ε → ζ → ν} {g : α → β → ε} {h : γ → δ → ζ}
    {f' : ε' → ζ' → ν} {g' : α → γ → ε'} {h' : β → δ → ζ'}
    (h_comm : ∀ a b c d, f (g a b) (h c d) = f' (g' a c) (h' b d)) :
    image₂ f (image₂ g s t) (image₂ h u v) = image₂ f' (image₂ g' s u) (image₂ h' t v) :=
  coe_injective <| by
    push_cast
    exact image2_image2_image2_comm h_comm

Proof state:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst✝⁴ : DecidableEq ε
inst✝³ : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g ↑s ↑t) (image2 h ↑u ↑v) = image2 f' (image2 g' ↑s ↑u) (image2 h' ↑t ↑v)

Tactic:
exact image2_image2_image2_comm h_comm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst✝⁴ : DecidableEq ε
inst✝³ : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ ↑(image₂ f (image₂ g s t) (image₂ h u v)) = ↑(image₂ f' (image₂ g' s u) (image₂ h' t v))

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
ε : Type u_9
ε' : Type u_10
ζ : Type u_11
ζ' : Type u_12
ν : Type u_13
inst✝⁴ : DecidableEq ε
inst✝³ : DecidableEq ε'
s : Finset α
t : Finset β
γ : Type u_14
δ : Type u_15
u : Finset γ
v : Finset δ
inst✝² : DecidableEq ζ
inst✝¹ : DecidableEq ζ'
inst✝ : DecidableEq ν
f : ε → ζ → ν
g : α → β → ε
h : γ → δ → ζ
f' : ε' → ζ' → ν
g' : α → γ → ε'
h' : β → δ → ζ'
h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)
⊢ image2 f (image2 g ↑s ↑t) (image2 h ↑u ↑v) = image2 f' (image2 g' ↑s ↑u) (image2 h' ↑t ↑v)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_norm_go (ctx : Context) (p : Poly) (r : Poly) : (norm.go p r).denote ctx = p.denote ctx + r.denote ctx

Proof state:
ctx : Context
p r : Poly
⊢ denote ctx (norm.go p r) = denote ctx p + denote ctx r

Tactic:
match p with
| [] => simp
| (k, v):: p => simp [denote_norm_go]

Result:
no goals

Proof state:
ctx : Context
p✝ r : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx (norm.go ((k, v) :: p) r) = denote ctx ((k, v) :: p) + denote ctx r

Tactic:
simp [denote_norm_go]

Result:
no goals

Proof state:
ctx : Context
p r : Poly
⊢ denote ctx (norm.go [] r) = denote ctx [] + denote ctx r

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Ioc {a b : ℝ} : volume (Ioc a b) = ofReal (b - a)

Proof state:
a b : ℝ
⊢ volume (Ioc a b) = ofReal (b - a)

Tactic:
simp [volume_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) :
    ((⟦aig, ⟨start, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?)
      →
    (⟦aig, ⟨start, h1⟩, assign1⟧ = sat?)

Proof state:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
⊢ (⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ &&
        State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val) =
      sat? →
    ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = sat?

Tactic:
have := go_as_denote' aig start h1 assign1

Result:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
this :
  ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true
⊢ (⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ &&
        State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val) =
      sat? →
    ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = sat?

Proof state:
sat? : Bool
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
this :
  ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = true →
    State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val = true
⊢ (⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ &&
        State.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val) =
      sat? →
    ⟦assign1, { aig := aig, ref := { gate := start, hgate := h1 } }⟧ = sat?

Tactic:
by_cases CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf <;> simp_all

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma predAbove_last_castSucc {i : Fin (n + 1)} : predAbove (last n) (i.castSucc) = i

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ (last n).predAbove i.castSucc = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.skeletonLT_subset_complex [RelCWComplex C D] {n : ℕ∞} : skeletonLT C n ⊆ C

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ skeletonLT C n ⊆ skeletonLT C ⊤

Tactic:
exact skeletonLT_mono (OrderTop.le_top n)

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ skeletonLT C n ⊆ C

Tactic:
simp_rw [← skeletonLT_top (C := C) (D := D)]

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ skeletonLT C n ⊆ skeletonLT C ⊤
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
lemma addOppositeEquiv_support (x : HahnSeries Γ (Rᵃᵒᵖ)) :
    (addOppositeEquiv x).unop.support = x.support

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
x✝ : Γ
⊢ x✝ ∈ (AddOpposite.unop (addOppositeEquiv x)).support ↔ x✝ ∈ x.support

Tactic:
simp [addOppositeEquiv_apply]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
⊢ (AddOpposite.unop (addOppositeEquiv x)).support = x.support

Tactic:
ext

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ Rᵃᵒᵖ
x✝ : Γ
⊢ x✝ ∈ (AddOpposite.unop (addOppositeEquiv x)).support ↔ x✝ ∈ x.support
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.isEquivalent_nat_ceil :
    (fun (x : R) ↦ ↑⌈x⌉₊) ~[atTop] (fun x ↦ x)

Proof state:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ (fun x => ↑⌈x⌉₊) ~[atTop] fun x => x

Tactic:
refine isEquivalent_of_tendsto_one ?_ tendsto_nat_ceil_div_atTop

Result:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ ∀ᶠ (x : R) in atTop, x = 0 → ↑⌈x⌉₊ = 0

Proof state:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ ∀ᶠ (x : R) in atTop, x = 0 → ↑⌈x⌉₊ = 0

Tactic:
filter_upwards with x hx using by rw [hx, Nat.ceil_zero, Nat.cast_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
x : R
hx : x = 0
⊢ ↑⌈x⌉₊ = 0

Tactic:
rw [hx, Nat.ceil_zero, Nat.cast_eq_zero]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
theorem levelOne_nonpos_wt_const (hk : k ≤ 0) (f : F) :
    ⇑f = Function.const _ (cuspFunction 1 f 0)

Proof state:
case h
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
z : ℍ
⊢ f z = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0) z

Tactic:
have hQ : 𝕢 1 z ∈ (Metric.ball 0 1) := by
  simpa only [Metric.mem_ball, dist_zero_right, neg_mul, mul_zero, div_one, Real.exp_zero]
    using (norm_qParam_lt_iff zero_lt_one 0 z.1).mpr z.2

Result:
case h
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
z : ℍ
hQ : 𝕢 1 ↑z ∈ Metric.ball 0 1
⊢ f z = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0) z

Proof state:
case h
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
z : ℍ
hQ : 𝕢 1 ↑z ∈ Metric.ball 0 1
⊢ f z = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0) z

Tactic:
simpa only [← eq_cuspFunction 1 f z, Nat.cast_one, Function.const_apply] using
  (cuspFunction_eqOn_const_of_nonpos_wt hk f) hQ

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
z : ℍ
⊢ 𝕢 1 ↑z ∈ Metric.ball 0 1

Tactic:
simpa only [Metric.mem_ball, dist_zero_right, neg_mul, mul_zero, div_one, Real.exp_zero]
  using (norm_qParam_lt_iff zero_lt_one 0 z.1).mpr z.2

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
⊢ ⇑f = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0)

Tactic:
ext z

Result:
case h
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F Γ(1) k
hk : k ≤ 0
f : F
z : ℍ
⊢ f z = Function.const ℍ (SlashInvariantFormClass.cuspFunction 1 f 0) z
-- Mathlib/Algebra/GeomSum.lean
lemma pow_one_sub_dvd_pow_mul_sub_one [Ring α] (x : α) (m n : ℕ) :
    ((x ^ m) - 1 : α) ∣ (x ^ (m * n) - 1)

Proof state:
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1

Tactic:
exact sub_one_dvd_pow_sub_one (x := x ^ m) (n := n)

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1

Tactic:
rw [npow_mul]

Result:
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1
-- Mathlib/Order/CompleteSublattice.lean
protected lemma codisjoint_iff {a b : L} :
    Codisjoint a b ↔ Codisjoint (a : α) (b : α)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Codisjoint a b ↔ Codisjoint ↑a ↑b

Tactic:
rw [codisjoint_iff, codisjoint_iff, ← Sublattice.coe_sup, ← coe_top (L := L),
  Subtype.coe_injective.eq_iff]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepFun_iff {β : ι → Type*}
    (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x) (μ : Measure Ω) :
    iIndepFun m f μ ↔ ∀ (s : Finset ι) {f' : ι → Set Ω}
      (_H : ∀ i, i ∈ s → MeasurableSet[(m i).comap (f i)] (f' i)),
      μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)

Proof state:
Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
β : ι → Type u_6
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
⊢ iIndepFun m f μ ↔
    ∀ (s : Finset ι) {f' : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)

Tactic:
simp only [iIndepFun_iff_iIndep, iIndep_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem map_comp_ιMulti {n : ℕ} (f : M →ₗ[R] N) :
    (map f).toLinearMap.compAlternatingMap (ιMulti R n (M := M)) =
    (ιMulti R n (M := N)).compLinearMap f

Proof state:
case H
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ ((map f).toLinearMap.compAlternatingMap (ιMulti R n)) m = ((ιMulti R n).compLinearMap f) m

Tactic:
exact map_apply_ιMulti _ _

Result:
no goals

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
⊢ (map f).toLinearMap.compAlternatingMap (ιMulti R n) = (ιMulti R n).compLinearMap f

Tactic:
ext m

Result:
case H
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] N
m : Fin n → M
⊢ ((map f).toLinearMap.compAlternatingMap (ιMulti R n)) m = ((ιMulti R n).compLinearMap f) m
-- Mathlib/Data/Set/NAry.lean
theorem image2_empty_right : image2 f s ∅ = ∅ :=
  ext <| by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ image2 f s ∅ ↔ x ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@[simp] lemma compProd_zero_right (μ : Measure α) : μ ⊗ₘ (0 : Kernel α β) = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
⊢ μ ⊗ₘ 0 = 0

Tactic:
simp [compProd]

Result:
no goals