harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_zero : (0 : SignedMeasure α).toJordanDecomposition = 0

Proof state:
case a
α : Type u_1
inst✝ : MeasurableSpace α
⊢ (toJordanDecomposition 0).toSignedMeasure = toSignedMeasure 0

Tactic:
simp [toSignedMeasure_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
⊢ toJordanDecomposition 0 = 0

Tactic:
apply toSignedMeasure_injective

Result:
case a
α : Type u_1
inst✝ : MeasurableSpace α
⊢ (toJordanDecomposition 0).toSignedMeasure = toSignedMeasure 0
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem memberSubfamily_inter (a : α) (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ∩ ℬ).memberSubfamily a = 𝒜.memberSubfamily a ∩ ℬ.memberSubfamily a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∩ ℬ) = memberSubfamily a 𝒜 ∩ memberSubfamily a ℬ

Tactic:
unfold memberSubfamily

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ image (fun s => s.erase a) (filter (fun s => a ∈ s) (𝒜 ∩ ℬ)) =
    image (fun s => s.erase a) (filter (fun s => a ∈ s) 𝒜) ∩ image (fun s => s.erase a) (filter (fun s => a ∈ s) ℬ)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ ↑(filter (fun s => a ∈ s) 𝒜) ∪ ↑(filter (fun s => a ∈ s) ℬ) ⊆ {s | a ∈ s}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ image (fun s => s.erase a) (filter (fun s => a ∈ s) (𝒜 ∩ ℬ)) =
    image (fun s => s.erase a) (filter (fun s => a ∈ s) 𝒜) ∩ image (fun s => s.erase a) (filter (fun s => a ∈ s) ℬ)

Tactic:
rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ ↑(filter (fun s => a ∈ s) 𝒜) ∪ ↑(filter (fun s => a ∈ s) ℬ) ⊆ {s | a ∈ s}
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_aroots [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {p : T[X]} {a : S} : a ∈ p.aroots S ↔ p ≠ 0 ∧ aeval a p = 0

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p : T[X]
a : S
⊢ a ∈ p.aroots S ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [mem_aroots', Polynomial.map_ne_zero_iff]

Result:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p : T[X]
a : S
⊢ Function.Injective ⇑(algebraMap T S)

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p : T[X]
a : S
⊢ Function.Injective ⇑(algebraMap T S)

Tactic:
exact FaithfulSMul.algebraMap_injective T S

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem fst_of_isColimit {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) :
    t.fst = ht.desc (BinaryCofan.mk (𝟙 X) 0)

Proof state:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app j

Tactic:
rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.fst = ht.desc (BinaryCofan.mk (𝟙 X) 0)

Tactic:
apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)

Result:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.fst = (BinaryCofan.mk (𝟙 X) 0).ι.app j
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_sub_lt_pi_div_two_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0) :
    angle x (x - y) < π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2

Tactic:
rw [sub_eq_add_neg]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 2

Tactic:
exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_one_right' [GCDMonoid α] (a : α) : Associated (gcd a 1) 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ Associated (gcd a 1) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Hom/Order.lean
theorem coe_iSup {ι : Sort*} [CompleteLattice β] (f : ι → α →o β) :
    ((⨆ i, f i : α →o β) : α → β) = ⨆ i, (f i : α → β)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨆ i, f i) x = (⨆ i, ⇑(f i)) x

Tactic:
simp [iSup_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨆ i, f i) = ⨆ i, ⇑(f i)

Tactic:
funext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨆ i, f i) x = (⨆ i, ⇑(f i)) x
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `f` tends to negative infinity along a nontrivial filter `l`, then
`fun x ↦ f x / r` tends to negative infinity if and only if `0 < r`. -/
lemma tendsto_div_const_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x => f x / r) l atBot ↔ 0 < r

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_pos h]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- Countable unions of σ-compact sets are σ-compact. -/
lemma isSigmaCompact_biUnion {s : Set ι} {S : ι → Set X} (hc : Set.Countable s)
    (hcomp : ∀ (i : ι), i ∈ s → IsSigmaCompact (S i)) :
    IsSigmaCompact (⋃ (i : ι) (_ : i ∈ s), S i)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
have : Countable ↑s := countable_coe_iff.mpr hc

Result:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
rw [biUnion_eq_iUnion]

Result:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ x, S ↑x)

Proof state:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ x, S ↑x)

Tactic:
exact isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem Chain.nil (r : α → α → Prop) : Cycle.Chain r (@nil α)

Proof state:
α : Type u_1
r : α → α → Prop
⊢ Chain r Cycle.nil

Tactic:
trivial

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem comp_linearEquiv_eq_zero_iff (g : MultilinearMap R M₁' M₂) (f : ∀ i, M₁ i ≃ₗ[R] M₁' i) :
    (g.compLinearMap fun i => (f i : M₁ i →ₗ[R] M₁' i)) = 0 ↔ g = 0

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
M₁' : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
f' : (i : ι) → M₁ i →ₗ[R] M₁' i := fun i => ↑(f i)
⊢ g.compLinearMap f' = 0 ↔ g = 0

Tactic:
rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
M₁' : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
⊢ (g.compLinearMap fun i => ↑(f i)) = 0 ↔ g = 0

Tactic:
set f' := fun i => (f i : M₁ i →ₗ[R] M₁' i)

Result:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
M₁' : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
f' : (i : ι) → M₁ i →ₗ[R] M₁' i := fun i => ↑(f i)
⊢ g.compLinearMap f' = 0 ↔ g = 0
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem map_Q {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive]
    (X : SimplicialObject C) (q n : ℕ) :
    G.map ((Q q : K[X] ⟶ _).f n) = (Q q : K[((whiskering C D).obj G).obj X] ⟶ _).f n

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = 𝟙 (((whiskering C D).obj G).obj X _⦋n⦌)

Tactic:
apply G.map_id

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map ((Q q).f n) = (Q q).f n

Tactic:
rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f,
  P_add_Q_f]

Result:
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = 𝟙 (((whiskering C D).obj G).obj X _⦋n⦌)
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem singletonSubgraph_eq_induce {v : V} :
    G.singletonSubgraph v = (⊤ : G.Subgraph).induce {v}

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ G.singletonSubgraph v = ⊤.induce {v}

Tactic:
ext <;> simp +contextual [-Set.bot_eq_empty, Prop.bot_eq_false]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive] lemma subset_div_left (ht : 1 ∈ t) : s ⊆ s / t

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹

Tactic:
exact subset_mul_left _ <| by simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ s ⊆ s * t⁻¹
-- Mathlib/RingTheory/Localization/Defs.lean
theorem eq_iff_exists {x y} : algebraMap R S x = algebraMap R S y ↔ ∃ c : M, ↑c * x = ↑c * y :=
  Iff.intro IsLocalization.exists_of_eq fun ⟨c, h⟩ ↦ by
    apply_fun algebraMap R S at h
    rw [map_mul, map_mul] at h
    exact (IsLocalization.map_units S c).mul_right_inj.mp h

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥M
h : (algebraMap R S) (↑c * x) = (algebraMap R S) (↑c * y)
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
rw [map_mul, map_mul] at h

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥M
h : (algebraMap R S) ↑c * (algebraMap R S) x = (algebraMap R S) ↑c * (algebraMap R S) y
⊢ (algebraMap R S) x = (algebraMap R S) y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥M
h : ↑c * x = ↑c * y
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
apply_fun algebraMap R S at h

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥M
h : (algebraMap R S) (↑c * x) = (algebraMap R S) (↑c * y)
⊢ (algebraMap R S) x = (algebraMap R S) y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x y : R
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥M
h : (algebraMap R S) ↑c * (algebraMap R S) x = (algebraMap R S) ↑c * (algebraMap R S) y
⊢ (algebraMap R S) x = (algebraMap R S) y

Tactic:
exact (IsLocalization.map_units S c).mul_right_inj.mp h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma of_surjective (f : X → Y) (hf : Function.Surjective f) :
    HasCardinalLT Y κ

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Proof state:
X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ HasCardinalLT Y κ

Tactic:
dsimp [HasCardinalLT] at h ⊢

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
exact lt_of_le_of_lt (Cardinal.mk_le_of_surjective
  (Function.Surjective.comp ULift.up_surjective (Function.Surjective.comp hf
    ULift.down_surjective))) h

Result:
no goals

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ
-- Mathlib/Order/Filter/CardinalInter.lean
theorem eventually_cardinal_forall {p : α → ι → Prop} (hic : #ι < c) :
    (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ ⋂ i, {x | p x i} ∈ l ↔ ∀ (i : ι), {x | p x i} ∈ l

Tactic:
exact cardinal_iInter_mem hic

Result:
no goals

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simp only [Filter.Eventually, setOf_forall]

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
p : α → ι → Prop
hic : #ι < c
⊢ ⋂ i, {x | p x i} ∈ l ↔ ∀ (i : ι), {x | p x i} ∈ l
-- Mathlib/Order/Ideal.lean
theorem sequenceOfCofinals.encode_mem (i : ι) :
    sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

Proof state:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i

Tactic:
apply Cofinal.above_mem

Result:
no goals

Proof state:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i

Tactic:
rw [Encodable.encodek]

Result:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match some i with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i

Proof state:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

Tactic:
dsimp only [sequenceOfCofinals, Nat.add]

Result:
P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ (match Encodable.decode (Encodable.encode i) with
    | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
    | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i))) ∈
    𝒟 i
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.of_mem_Icc [IsFiniteMeasure μ] (a b : ℝ) {X : α → ℝ}
    (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) :
    HasFiniteIntegral X μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ ‖a‖ ⊔ ‖b‖

Tactic:
filter_upwards [h.mono fun ω h ↦ h.1, h.mono fun ω h ↦ h.2] with ω using abs_le_max_abs_abs

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ HasFiniteIntegral X μ

Tactic:
apply (hasFiniteIntegral_const (max ‖a‖ ‖b‖)).mono'

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
a b : ℝ
X : α → ℝ
h : ∀ᵐ (ω : α) ∂μ, X ω ∈ Icc a b
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖X a_1‖ ≤ ‖a‖ ⊔ ‖b‖
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem nhdsWithin_compl_infty_eq : 𝓝[≠] (∞ : OnePoint X) = map (↑) (coclosedCompact X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝[≠] ∞ = map some (coclosedCompact X)

Tactic:
refine (nhdsWithin_basis_open ∞ _).ext (hasBasis_coclosedCompact.map _) ?_ ?_

Result:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set (OnePoint X)), ∞ ∈ i ∧ IsOpen i → ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X), IsClosed i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ

Proof state:
case refine_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' sᶜ

Tactic:
refine ⟨_, ⟨mem_compl infty_not_mem_image_coe, isOpen_compl_image_coe.2 ⟨h₁, h₂⟩⟩, ?_⟩

Result:
case refine_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set (OnePoint X)), ∞ ∈ i ∧ IsOpen i → ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ i ∩ {∞}ᶜ

Tactic:
rintro s ⟨hs, hso⟩

Result:
case refine_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ

Proof state:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
⊢ ∀ (i' : Set X), IsClosed i' ∧ IsCompact i' → ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' i'ᶜ

Tactic:
rintro s ⟨h₁, h₂⟩

Result:
case refine_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ ∃ i, (∞ ∈ i ∧ IsOpen i) ∧ i ∩ {∞}ᶜ ⊆ some '' sᶜ

Proof state:
case refine_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ

Tactic:
simp [Subset.rfl]

Result:
no goals

Proof state:
case refine_2.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h₁ : IsClosed s
h₂ : IsCompact s
⊢ (some '' s)ᶜ ∩ {∞}ᶜ ⊆ some '' sᶜ

Tactic:
simp [compl_image_coe, ← diff_eq, subset_preimage_image]

Result:
no goals

Proof state:
case refine_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ ∃ i', (IsClosed i' ∧ IsCompact i') ∧ some '' i'ᶜ ⊆ s ∩ {∞}ᶜ

Tactic:
refine ⟨_, (isOpen_iff_of_mem hs).mp hso, ?_⟩

Result:
case refine_1.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
hs : ∞ ∈ s
hso : IsOpen s
⊢ some '' (some ⁻¹' s)ᶜᶜ ⊆ s ∩ {∞}ᶜ
-- Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
lemma isLocallySurjective_π_app_zero_of_isLocallySurjective_map  :
    Sheaf.IsLocallySurjective (c.π.app ⟨0⟩)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((c.π.app (op 0)).val.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op 0)).val.map (op φ))) y

Tactic:
have hh : EffectiveEpi (limit.π (preimageDiagram hF X y) ⟨0⟩) :=
  h _ fun n ↦ by simpa [preimageDiagram] using (preimageStruct hF X y).effectiveEpi n

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).val.obj (op X))
hh : EffectiveEpi (limit.π (CategoryTheory.coherentTopology.preimageDiagram hF X y) (op 0))
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ),
      ∃ x,
        (ConcreteCategory.hom ((c.π.app (op 0)).val.app (op X'))) x =
          (ConcreteCategory.hom ((F.obj (op 0)).val.map (op φ))) y
-- Mathlib/Topology/GDelta/Basic.lean
theorem mem_residual_iff {s : Set X} :
    s ∈ residual X ↔
      ∃ S : Set (Set X), (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s :=
  mem_countableGenerate_iff.trans <| by simp_rw [subset_def, mem_setOf, forall_and, and_assoc]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S ⊆ {t | IsOpen t ∧ Dense t}, S.Countable ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ t ∈ S, IsOpen t) ∧ (∀ t ∈ S, Dense t) ∧ S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
simp_rw [subset_def, mem_setOf, forall_and, and_assoc]

Result:
no goals