harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Irreducible.lean
theorem isIrreducible_iff_sUnion_isClosed :
    IsIrreducible s ↔
      ∀ t : Finset (Set X), (∀ z ∈ t, IsClosed z) → (s ⊆ ⋃₀ ↑t) → ∃ z ∈ t, s ⊆ z

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, IsClosed z) →
      s ⊆ ⋃₀ ↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t) →
        ∃ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, s ⊆ z

Tactic:
simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
  sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
  exists_exists_and_eq_and]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ a ∈ t, s ⊆ aᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ a ∈ t, s ⊆ aᶜ

Tactic:
refine forall_congr' fun _ => Iff.trans ?_ not_imp_not

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
x✝ : ∀ u ∈ t, IsOpen u
⊢ (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔ (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ a ∈ ↑t, aᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

Tactic:
refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, IsClosed z) →
      s ⊆ ⋃₀ ↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t) →
        ∃ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, s ⊆ z

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔ ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

Tactic:
simp only [isIrreducible_iff_sInter]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty) ↔
    ∀ (t : Finset (Set X)), (∀ z ∈ t, IsClosed z) → s ⊆ ⋃₀ ↑t → ∃ z ∈ t, s ⊆ z

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
x✝ : ∀ u ∈ t, IsOpen u
⊢ (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔ (¬∃ a ∈ t, s ⊆ aᶜ) → ¬s ⊆ ⋃ a ∈ ↑t, aᶜ

Tactic:
simp only [not_exists, not_and, ← compl_iInter₂, ← sInter_eq_biInter,
  subset_compl_iff_disjoint_right, not_disjoint_iff_nonempty_inter]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
    polarBilin (Q.baseChange A) = BilinForm.baseChange A (polarBilin Q)

Proof state:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ polarBilin (QuadraticForm.baseChange A Q) = BilinForm.baseChange A (polarBilin Q)

Tactic:
rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul,
  ← LinearMap.map_smul, smul_tmul', ← two_nsmul_associated R, coe_associatedHom, associated_sq,
  smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem diam_boxIcc (ν : ι → ℤ) :
    Metric.diam (Box.Icc (box n ν)) ≤ 1 / n

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ 0 ≤ 1 / ↑n

Tactic:
positivity

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ EMetric.diam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (1 / ↑n)

Tactic:
simp_rw [Real.ediam_Icc, box.upper_sub_lower, le_rfl]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ Metric.diam (Set.univ.pi fun i => Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ 1 / ↑n

Tactic:
refine ENNReal.toReal_le_of_le_ofReal (by positivity) <| EMetric.diam_pi_le_of_le (fun i ↦ ?_)

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ EMetric.diam (Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ ENNReal.ofReal (1 / ↑n)

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ Metric.diam (Box.Icc (box n ν)) ≤ 1 / ↑n

Tactic:
rw [BoxIntegral.Box.Icc_eq_pi]

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
⊢ Metric.diam (Set.univ.pi fun i => Set.Icc ((box n ν).lower i) ((box n ν).upper i)) ≤ 1 / ↑n
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem hasMFDerivAt_fst (x : M × M') :
    HasMFDerivAt (I.prod I') I Prod.fst x
      (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x : M × M'
y : E × E'
hy : y ∈ ((extChartAt I x.1).prod (extChartAt I' x.2)).target
⊢ (↑(extChartAt I x.1) ∘ Prod.fst ∘ ↑(extChartAt (I.prod I') x).symm) y = y.1

Tactic:
exact (extChartAt I x.1).right_inv hy.1

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x : M × M'
⊢ HasMFDerivAt (I.prod I') I Prod.fst x (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Tactic:
refine ⟨continuous_fst.continuousAt, ?_⟩

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x : M × M'
⊢ HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I x Prod.fst)
    (ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I'))
    (↑(extChartAt (I.prod I') x) x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_seqRight [Monad m] (x : StateT σ m α) (y : StateT σ m β) (s : σ) : (x *> y).run s = (x.run s >>= fun p => y.run p.2)

Proof state:
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝ : Monad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (do
          let _ ← x
          y).run
      s =
    do
    let p ← x.run s
    y.run p.snd

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝ : Monad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (x *> y).run s = do
    let p ← x.run s
    y.run p.snd

Tactic:
show (x >>= fun _ => y).run s = _

Result:
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝ : Monad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ (do
          let _ ← x
          y).run
      s =
    do
    let p ← x.run s
    y.run p.snd
-- Mathlib/Order/DirectedInverseSystem.lean
theorem isNatEquiv_piEquivSucc [InverseSystem f] (H : ∀ x, (e x).1 = f (le_succ i) x)
    (nat : IsNatEquiv f equiv) : IsNatEquiv f (piEquivSucc equiv e hi) := fun j k hj hk h x ↦ by
  have lt_succ {j} := (lt_succ_iff_of_not_isMax (b := j) hi).mpr
  obtain rfl | hj := le_succ_iff_eq_or_le.mp hj
  · obtain rfl | hk := le_succ_iff_eq_or_le.mp hk
    · simp [InverseSystem.map_self]
    · funext l
      rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
        ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]
      simp [piSplitLE_lt (l.2.trans_le hk)]
  · rw [piEquivSucc, piSplitLE_lt (h.trans_lt <| lt_succ hj), nat hj, piSplitLE_lt (lt_succ hj)]

Proof state:
case inl.inr.h
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ (piEquivSucc equiv e hi ⟨k, hk✝⟩) (f h x) l = piLTProj h ((piEquivSucc equiv e hi ⟨i⁺, hj⟩) x) l

Tactic:
rw [piEquivSucc, piSplitLE_lt (lt_succ hk),
  ← InverseSystem.map_map (f := f) hk (le_succ i), ← H, piLTProj, nat le_rfl]

Result:
case inl.inr.h
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝² : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝¹ : SuccOrder ι
equiv : (j : ↑(Iic i)) → F ↑j ≃ piLT X ↑j
e : F i⁺ ≃ F i × X i
hi : ¬IsMax i
inst✝ : InverseSystem f
H : ∀ (x : F i⁺), (e x).1 = f ⋯ x
nat : IsNatEquiv f equiv
k : ι
hk✝ : k ∈ Iic i⁺
lt_succ : ∀ {j : ι}, j ≤ i → j < i⁺
hj : i⁺ ∈ Iic i⁺
h : k ≤ i⁺
x : F i⁺
hk : k ≤ i
l : ↑(Iio ↑⟨k, hk✝⟩)
⊢ piLTProj hk ((equiv ⟨i, ⋯⟩) (e x).1) l =
    (piSplitLE
        (fun j => equiv ⟨↑j, ⋯⟩,
          e.trans (((equiv ⟨i, ⋯⟩).prodCongr (Equiv.refl (X i))).trans (piSplitLE.trans (Equiv.piCongrSet ⋯))))
        ⟨i⁺, hj⟩)
      x ⟨↑l, ⋯⟩
-- Mathlib/SetTheory/Lists.lean
theorem sizeof_pos {b} (l : Lists' α b) : 0 < SizeOf.sizeOf l

Proof state:
α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l

Tactic:
cases l <;> simp only [Lists'.atom.sizeOf_spec, Lists'.nil.sizeOf_spec, Lists'.cons'.sizeOf_spec,
  true_or, add_pos_iff, zero_lt_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Hull.lean
theorem AffineMap.image_convexHull (f : E →ᵃ[𝕜] F) (s : Set E) :
    f '' convexHull 𝕜 s = convexHull 𝕜 (f '' s)

Proof state:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)

Tactic:
refine convexHull_min ?_ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)

Result:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)

Proof state:
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) (⇑f '' s) ⊆ ⇑f '' (convexHull 𝕜) s

Tactic:
exact convexHull_min (Set.image_subset _ (subset_convexHull 𝕜 s))
  ((convex_convexHull 𝕜 s).affine_image f)

Result:
no goals

Proof state:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' (convexHull 𝕜) s ⊆ (convexHull 𝕜) (⇑f '' s)

Tactic:
rw [Set.image_subset_iff]

Result:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)

Proof state:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' s ⊆ (convexHull 𝕜) (⇑f '' s)

Tactic:
exact subset_convexHull 𝕜 (f '' s)

Result:
no goals

Proof state:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ s ⊆ ⇑f ⁻¹' (convexHull 𝕜) (⇑f '' s)

Tactic:
rw [← Set.image_subset_iff]

Result:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' s ⊆ (convexHull 𝕜) (⇑f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)

Tactic:
apply Set.Subset.antisymm

Result:
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' (convexHull 𝕜) s ⊆ (convexHull 𝕜) (⇑f '' s)

case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ (convexHull 𝕜) (⇑f '' s) ⊆ ⇑f '' (convexHull 𝕜) s
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem ne_zero_of_ne_zero_of_monic (hp : p ≠ 0) (hq : Monic q) : q ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
hq : q.Monic
⊢ q ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hq : Monic 0
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : 0 ≠ 0
hq : 0 = 1
⊢ False

Tactic:
exact hp rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hq : Monic 0
⊢ False

Tactic:
rw [Monic.def, leadingCoeff_zero] at hq

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hq : 0 = 1
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
hq : 0 = 1
⊢ False

Tactic:
rw [← mul_one p, ← C_1, ← hq, C_0, mul_zero] at hp

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : 0 ≠ 0
hq : 0 = 1
⊢ False
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem Ico_disjoint_Ico : Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Proof state:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ a₂ ⊓ b₂ ≤ a₁ ⊔ b₁

Tactic:
simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measure_eq_div_smul (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) :
    μ' = (μ' s / ν' s) • ν'

Proof state:
case h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
t : Set G
⊢ μ' t = ((μ' s / ν' s) • ν') t

Tactic:
rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
  measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel h2s h3s]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
⊢ μ' = (μ' s / ν' s) • ν'

Tactic:
ext1 t -

Result:
case h
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
t : Set G
⊢ μ' t = ((μ' s / ν' s) • ν') t
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem HD_bound_aux2 [Nonempty X] (f : Cb X Y) (C : ℝ) :
    BddAbove (range fun y : Y => ⨅ x, f (inl x, inr y) + C)

Proof state:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
y : Y
⊢ ⨅ x, f (inl x, inr y) + C ≤ Cf + C

Tactic:
calc
  ⨅ x, f (inl x, inr y) + C ≤ f (inl default, inr y) + C := ciInf_le (HD_below_aux2 C) default
  _ ≤ Cf + C := add_le_add ((fun x => hCf (mem_range_self x)) _) le_rfl

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : GromovHausdorff.Cb X Y
C : ℝ
⊢ BddAbove (range fun y => ⨅ x, f (inl x, inr y) + C)

Tactic:
obtain ⟨Cf, hCf⟩ := f.isBounded_range.bddAbove

Result:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun y => ⨅ x, f (inl x, inr y) + C)

Proof state:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun y => ⨅ x, f (inl x, inr y) + C)

Tactic:
refine ⟨Cf + C, forall_mem_range.2 fun y => ?_⟩

Result:
case intro
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty X
f : GromovHausdorff.Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
y : Y
⊢ ⨅ x, f (inl x, inr y) + C ≤ Cf + C
-- Mathlib/Data/ENNReal/Order.lean
theorem top_mul' : ∞ * a = if a = 0 then 0 else ∞

Proof state:
a : ℝ≥0∞
⊢ ⊤ * a = if a = 0 then 0 else ⊤

Tactic:
convert WithTop.top_mul' a

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem nhdsSet_Icc (h : a ≤ b) : 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Proof state:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rcases h.eq_or_lt with rfl | hlt

Result:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)

case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Proof state:
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_univ : derivWithin f univ = deriv f

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x✝ : 𝕜
⊢ (fderivWithin 𝕜 f univ x✝) 1 = (fderiv 𝕜 f x✝) 1

Tactic:
rw [fderivWithin_univ]

Result:
no goals

Proof state:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x✝ : 𝕜
⊢ derivWithin f univ x✝ = deriv f x✝

Tactic:
unfold derivWithin deriv

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x✝ : 𝕜
⊢ (fderivWithin 𝕜 f univ x✝) 1 = (fderiv 𝕜 f x✝) 1

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ derivWithin f univ = deriv f

Tactic:
ext

Result:
case h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x✝ : 𝕜
⊢ derivWithin f univ x✝ = deriv f x✝
-- Mathlib/Order/CompletePartialOrder.lean
/-- Scott-continuity takes on a simpler form in complete partial orders. -/
lemma CompletePartialOrder.scottContinuous {f : α → β} :
    ScottContinuous f ↔
    ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → IsLUB (f '' d) (f (sSup d))

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f a)

Tactic:
rw [hda.unique hd.isLUB_sSup]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f (sSup d))

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f (sSup d))

Tactic:
exact h hne hd

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
⊢ ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))

Tactic:
refine ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f a)
-- Mathlib/Data/Seq/Parallel.lean
theorem mem_parallel {S : WSeq (Computation α)} {a} (H : ∀ s ∈ S, s ~> a) {c} (cs : c ∈ S)
    (ac : a ∈ c) : a ∈ parallel S

Proof state:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ a ∈ parallel S

Tactic:
haveI := terminates_of_mem ac

Result:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : c.Terminates
⊢ a ∈ parallel S

Proof state:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : c.Terminates
⊢ a ∈ parallel S

Tactic:
haveI := terminates_parallel cs

Result:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this✝ : c.Terminates
this : (parallel S).Terminates
⊢ a ∈ parallel S

Proof state:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ (s : Computation α), s ∈ S → s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this✝ : c.Terminates
this : (parallel S).Terminates
⊢ a ∈ parallel S

Tactic:
exact mem_of_promises _ (parallel_promises H)

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem eq_ofPred_closed (c : ClosureOperator α) :
    c = ofPred c c.IsClosed c.le_closure c.isClosed_closure fun _ _ ↦ closure_min

Proof state:
case a
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x✝ : α
⊢ c x✝ = (ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯) x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ c = ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x✝ : α
⊢ c x✝ = (ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯) x✝