harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Separation/Basic.lean
theorem isCompact_closure_singleton : IsCompact (closure {x})

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ∈ closure {x}
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Tactic:
rw [← specializes_iff_mem_closure, specializes_comm] at hy

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ⤳ x
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
⊢ IsCompact (closure {x})

Tactic:
refine isCompact_of_finite_subcover fun U hUo hxU ↦ ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
⊢ ∃ t, closure {x} ⊆ ⋃ i ∈ t, U i

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ⤳ x
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Tactic:
simpa using hy.mem_open (hUo i) hi

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
⊢ ∃ t, closure {x} ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨i, hi⟩ : ∃ i, x ∈ U i := mem_iUnion.1 <| hxU <| subset_closure rfl

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
⊢ ∃ t, closure {x} ⊆ ⋃ i ∈ t, U i

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
⊢ ∃ t, closure {x} ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨{i}, fun y hy ↦ ?_⟩

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hxU : closure {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ∈ closure {x}
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem quasiCompact_iff_forall_affine :
    QuasiCompact f ↔
      ∀ U : Y.Opens, IsAffineOpen U → IsCompact (f ⁻¹ᵁ U : Set X)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)) →
    ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)

Tactic:
intro H U hU hU'

Result:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
U : Set ↑↑Y.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
refine ⟨fun H U hU => H U U.isOpen hU.isCompact, ?_⟩

Result:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)) →
    ∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)

Proof state:
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
S : Set ↑Y.affineOpens
hS : S.Finite
hU : IsOpen (⋃ i ∈ S, ↑↑i)
hU' : IsCompact (⋃ i ∈ S, ↑↑i)
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' ⋃ i ∈ S, ↑↑i)

Tactic:
simp only [Set.preimage_iUnion]

Result:
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
S : Set ↑Y.affineOpens
hS : S.Finite
hU : IsOpen (⋃ i ∈ S, ↑↑i)
hU' : IsCompact (⋃ i ∈ S, ↑↑i)
⊢ IsCompact (⋃ i ∈ S, ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑↑i)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)

Tactic:
rw [quasiCompact_iff]

Result:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↑↑Y.toPresheafedSpace), IsOpen U → IsCompact U → IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
U : Set ↑↑Y.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' U)

Tactic:
obtain ⟨S, hS, rfl⟩ := (isCompactOpen_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩

Result:
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
S : Set ↑Y.affineOpens
hS : S.Finite
hU : IsOpen (⋃ i ∈ S, ↑↑i)
hU' : IsCompact (⋃ i ∈ S, ↑↑i)
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' ⋃ i ∈ S, ↑↑i)

Proof state:
case intro.intro
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact ↑(f ⁻¹ᵁ U)
S : Set ↑Y.affineOpens
hS : S.Finite
hU : IsOpen (⋃ i ∈ S, ↑↑i)
hU' : IsCompact (⋃ i ∈ S, ↑↑i)
⊢ IsCompact (⋃ i ∈ S, ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑↑i)

Tactic:
exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem isLindelof_range [LindelofSpace X] {f : X → Y} (hf : Continuous f) :
    IsLindelof (range f)

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous f
⊢ IsLindelof (f '' univ)

Tactic:
exact isLindelof_univ.image hf

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous f
⊢ IsLindelof (range f)

Tactic:
rw [← image_univ]

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous f
⊢ IsLindelof (f '' univ)
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem closure_eq_image_prod (s : Set M) :
    (closure s : Set M) = List.prod '' { l : List M | ∀ x ∈ l, x ∈ s }

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)

Tactic:
exact congrArg _ (funext <| FreeMonoid.lift_apply _)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = List.prod '' {l | ∀ x ∈ l, x ∈ s}

Tactic:
rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]

Result:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)
-- Mathlib/Data/Set/NAry.lean
theorem image2_singleton_left : image2 f {a} t = f a '' t :=
  ext fun x => by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
t : Set β
a : α
x : γ
⊢ x ∈ image2 f {a} t ↔ x ∈ f a '' t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Idempotent.lean
@[simp] lemma one_compl : (1 : {a : R // IsIdempotentElem a})ᶜ = 0

Proof state:
case a
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑1ᶜ = ↑0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
⊢ 1ᶜ = 0

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑1ᶜ = ↑0
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.smul_of_top_right {f : α → β} {φ : α → 𝕜} (hf : Integrable f μ)
    (hφ : MemLp φ ∞ μ) : Integrable (φ • f) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f μ
hφ : MemLp φ ⊤ μ
⊢ Integrable (φ • f) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : MemLp f 1 μ
hφ : MemLp φ ⊤ μ
⊢ MemLp (φ • f) 1 μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_6
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : BoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : MemLp f 1 μ
hφ : MemLp φ ⊤ μ
⊢ MemLp (φ • f) 1 μ

Tactic:
exact MemLp.smul hf hφ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq_true {p : α → Bool} {xs : Vector α n} :
    xs.all p = true ↔ ∀ (i : Nat) (_ : i < n), p xs[i]

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = true ↔ ∀ (i : Nat) (x : i < n), p xs[i] = true

Tactic:
simp [all_iff_forall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqvAux_of_rel {r : α → α → Bool} {a b : Array α} (hsz : a.size = b.size) {i : Nat} (hi : i ≤ a.size)
    (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
i : Nat
hi : i ≤ a.size
w : ∀ (j : Nat) (hj : j < i), r a[j] b[j] = true
⊢ a.isEqvAux b hsz r i hi = true

Tactic:
induction i with
| zero => simp [Array.isEqvAux]
| succ i ih =>
  simp only [isEqvAux, Bool.and_eq_true]
  exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩

Result:
no goals

Proof state:
case zero
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
hi : 0 ≤ a.size
w : ∀ (j : Nat) (hj : j < 0), r a[j] b[j] = true
⊢ a.isEqvAux b hsz r 0 hi = true

Tactic:
simp [Array.isEqvAux]

Result:
no goals

Proof state:
case succ
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
i : Nat
ih : ∀ (hi : i ≤ a.size), (∀ (j : Nat) (hj : j < i), r a[j] b[j] = true) → a.isEqvAux b hsz r i hi = true
hi : i + 1 ≤ a.size
w : ∀ (j : Nat) (hj : j < i + 1), r a[j] b[j] = true
⊢ a.isEqvAux b hsz r (i + 1) hi = true

Tactic:
simp only [isEqvAux, Bool.and_eq_true]

Result:
case succ
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
i : Nat
ih : ∀ (hi : i ≤ a.size), (∀ (j : Nat) (hj : j < i), r a[j] b[j] = true) → a.isEqvAux b hsz r i hi = true
hi : i + 1 ≤ a.size
w : ∀ (j : Nat) (hj : j < i + 1), r a[j] b[j] = true
⊢ r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true

Proof state:
case succ
α : Type u_1
r : α → α → Bool
a b : Array α
hsz : a.size = b.size
i : Nat
ih : ∀ (hi : i ≤ a.size), (∀ (j : Nat) (hj : j < i), r a[j] b[j] = true) → a.isEqvAux b hsz r i hi = true
hi : i + 1 ≤ a.size
w : ∀ (j : Nat) (hj : j < i + 1), r a[j] b[j] = true
⊢ r a[i] b[i] = true ∧ a.isEqvAux b hsz r i ⋯ = true

Tactic:
exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_replicate (n : ℕ) (a : α) : (replicate n a).prod = a ^ n

Proof state:
α : Type u_3
inst✝ : CommMonoid α
n : ℕ
a : α
⊢ (replicate n a).prod = a ^ n

Tactic:
simp [replicate, List.prod_replicate]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma oneEquiv_ιMulti (f : Fin 1 → M) :
    oneEquiv R M (ιMulti _ _ f) = f 0

Proof state:
R : Type u
inst✝² : CommRing R
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : Fin 1 → M
⊢ (oneEquiv R M) ((ιMulti R 1) f) = f 0

Tactic:
simp [oneEquiv]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd [Nontrivial k] (p : ι → P) (j : ι) (q : P) :
    q ∈ affineSpan k (Set.range p) ↔
      ∃ (s : Finset ι) (w : ι → k), q = s.weightedVSubOfPoint p (p j) w +ᵥ p j

Proof state:
case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
q : P
⊢ (∃ s w, q = (s.weightedVSubOfPoint p (p j)) w +ᵥ p j) → q ∈ affineSpan k (Set.range p)

Tactic:
rintro ⟨s, w, rfl⟩

Result:
case mpr.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
⊢ (s.weightedVSubOfPoint p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)

Proof state:
case mpr.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ (s.weightedVSubOfPoint p (p j)) w +ᵥ p j ∈ affineSpan k (Set.range p)

Tactic:
rw [s.weightedVSubOfPoint_eq_of_weights_eq p j w w' hww, ←
  s.weightedVSubOfPoint_insert w' p j, ←
  (insert j s).affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one w' p h₁ (p j)]

Result:
case mpr.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
j : ι
s : Finset ι
w : ι → k
w' : ι → k := Function.update w j (1 - (s \ {j}).sum w)
h₁ : (insert j s).sum w' = 1
hww : ∀ (i : ι), i ≠ j → w i = w' i
⊢ (Finset.affineCombination k (insert j s) p) w' ∈ affineSpan k (Set.range p)
-- Mathlib/Control/LawfulFix.lean
theorem approx_mono' {i : ℕ} : Fix.approx f i ≤ Fix.approx f (succ i)

Proof state:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) (n✝ + 1) i✝ ≤ approx (⇑f) (n✝ + 1).succ i✝

Tactic:
apply f.monotone

Result:
case succ.a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) n✝ ≤ approx (⇑f) (n✝ + 1)

Proof state:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
⊢ approx (⇑f) (n✝ + 1) ≤ approx (⇑f) (n✝ + 1).succ

Tactic:
intro

Result:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) (n✝ + 1) i✝ ≤ approx (⇑f) (n✝ + 1).succ i✝

Proof state:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ f ⊥

Tactic:
apply @bot_le _ _ _ (f ⊥)

Result:
no goals

Proof state:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) (Nat.succ 0)

Tactic:
dsimp [approx]

Result:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ f ⊥

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (⇑f) i ≤ approx (⇑f) i.succ

Tactic:
induction i with
| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
| succ _ i_ih => intro; apply f.monotone; apply i_ih

Result:
no goals

Proof state:
case succ.a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) n✝ ≤ approx (⇑f) (n✝ + 1)

Tactic:
apply i_ih

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) :
    Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ p * C p.leadingCoeff⁻¹ ≠ 1

Tactic:
contrapose! hpu

Result:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : p * C p.leadingCoeff⁻¹ = 1
⊢ IsUnit p

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : p * C p.leadingCoeff⁻¹ ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
rw [← irreducible_mul_leadingCoeff_inv,
    (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
    natDegree_mul_leadingCoeff_inv _ hp0]

Result:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : p * C p.leadingCoeff⁻¹ ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p * C p.leadingCoeff⁻¹) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
  contrapose! hpu
  exact isUnit_of_mul_eq_one _ _ hpu

Result:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : p * C p.leadingCoeff⁻¹ ≠ 1
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : p * C p.leadingCoeff⁻¹ = 1
⊢ IsUnit p

Tactic:
exact isUnit_of_mul_eq_one _ _ hpu

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
this : p * C p.leadingCoeff⁻¹ ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p * C p.leadingCoeff⁻¹) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
simp only [IsUnit.dvd_mul_right
  (isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem iInf_neBot_of_directed {f : ι → Filter α} [hn : Nonempty α] (hd : Directed (· ≥ ·) f)
    (hb : ∀ i, NeBot (f i)) : NeBot (iInf f)

Proof state:
case inr
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : Nonempty ι
⊢ (iInf f).NeBot

Tactic:
exact iInf_neBot_of_directed' hd hb

Result:
no goals

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
⊢ (iInf f).NeBot

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ (iInf f).NeBot

case inr
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : Nonempty ι
⊢ (iInf f).NeBot

Proof state:
case inl.ne'
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ iInf f ≠ ⊥

Tactic:
simp [iInf_of_empty f, top_ne_bot]

Result:
no goals

Proof state:
case inl
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ (iInf f).NeBot

Tactic:
constructor

Result:
case inl.ne'
α : Type u
ι : Sort x
f : ι → Filter α
hn : Nonempty α
hd : Directed (fun x1 x2 => x1 ≥ x2) f
hb : ∀ (i : ι), (f i).NeBot
h✝ : IsEmpty ι
⊢ iInf f ≠ ⊥
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem edist_indicatorConstLp_eq_enorm {t : Set α} {ht : MeasurableSet t} {hμt : μ t ≠ ∞} :
    edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) =
      ‖indicatorConstLp p (hs.symmDiff ht) (measure_symmDiff_ne_top hμs hμt) c‖ₑ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ edist (MemLp.toLp (s.indicator fun x => c) ⋯) (MemLp.toLp (t.indicator fun x => c) ⋯) =
    ‖MemLp.toLp ((s ∆ t).indicator fun x => c) ⋯‖ₑ

Tactic:
rw [Lp.edist_toLp_toLp, eLpNorm_indicator_sub_indicator, Lp.enorm_toLp]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ edist (indicatorConstLp p hs hμs c) (indicatorConstLp p ht hμt c) = ‖indicatorConstLp p ⋯ ⋯ c‖ₑ

Tactic:
unfold indicatorConstLp

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ edist (MemLp.toLp (s.indicator fun x => c) ⋯) (MemLp.toLp (t.indicator fun x => c) ⋯) =
    ‖MemLp.toLp ((s ∆ t).indicator fun x => c) ⋯‖ₑ
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem dist_self (x : Completion α) : dist x x = 0

Proof state:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ IsClosed {a | dist a a = 0}

Tactic:
refine isClosed_eq ?_ continuous_const

Result:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a => dist a a

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ ∀ (a : α), dist ↑a ↑a = 0

Tactic:
intro a

Result:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist ↑a ↑a = 0

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist ↑a ↑a = 0

Tactic:
rw [Completion.dist_eq, dist_self]

Result:
no goals

Proof state:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ Continuous fun a => dist a a

Tactic:
exact Completion.continuous_dist continuous_id continuous_id

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0

Tactic:
refine induction_on x ?_ ?_

Result:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ IsClosed {a | dist a a = 0}

case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
x : Completion α
⊢ ∀ (a : α), dist ↑a ↑a = 0
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem toProperty_apply (P : AffineTargetMorphismProperty)
    {X Y : Scheme} (f : X ⟶ Y) [i : IsAffine Y] : P.toProperty f ↔ P f

Proof state:
P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ (∃ (h : IsAffine Y), P f) ↔ P f

Tactic:
simp [*]

Result:
no goals

Proof state:
P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ P.toProperty f ↔ P f

Tactic:
delta AffineTargetMorphismProperty.toProperty

Result:
P : AffineTargetMorphismProperty
X Y : Scheme
f : X ⟶ Y
i : IsAffine Y
⊢ (∃ (h : IsAffine Y), P f) ↔ P f
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma indepNum_compl : Gᶜ.indepNum = G.cliqueNum

Proof state:
α : Type u_3
G : SimpleGraph α
⊢ Gᶜ.indepNum = G.cliqueNum

Tactic:
simp [indepNum, cliqueNum]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem IsNormal.cof_le {f} (hf : IsNormal f) (a) : cof a ≤ cof (f a)

Proof state:
case inr.inl.intro
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
b : Ordinal.{u_1}
⊢ 0 < f (succ b)

Tactic:
exact (Ordinal.zero_le (f b)).trans_lt (hf.1 b)

Result:
no goals

Proof state:
case inr.inl.intro
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
b : Ordinal.{u_1}
⊢ (succ b).cof ≤ (f (succ b)).cof

Tactic:
rw [cof_succ, Cardinal.one_le_iff_ne_zero, cof_ne_zero, ← Ordinal.pos_iff_ne_zero]

Result:
case inr.inl.intro
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
b : Ordinal.{u_1}
⊢ 0 < f (succ b)

Proof state:
case inl
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ cof 0 ≤ (f 0).cof

Tactic:
rw [cof_zero]

Result:
case inl
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ 0 ≤ (f 0).cof

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
⊢ a.cof ≤ (f a).cof

Tactic:
rcases zero_or_succ_or_limit a with (rfl | ⟨b, rfl⟩ | ha)

Result:
case inl
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ cof 0 ≤ (f 0).cof

case inr.inl.intro
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
b : Ordinal.{u_1}
⊢ (succ b).cof ≤ (f (succ b)).cof

case inr.inr
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : a.IsLimit
⊢ a.cof ≤ (f a).cof

Proof state:
case inl
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ 0 ≤ (f 0).cof

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case inr.inr
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : a.IsLimit
⊢ a.cof ≤ (f a).cof

Tactic:
rw [hf.cof_eq ha]

Result:
no goals