harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Subsingleton.lean
theorem exists_eq_singleton_iff_nonempty_subsingleton :
    (∃ a : α, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton

Proof state:
case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}

Tactic:
exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

Result:
no goals

Proof state:
α : Type u
s : Set α
⊢ (∃ a, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton

Tactic:
refine ⟨?_, fun h => ?_⟩

Result:
case refine_1
α : Type u
s : Set α
⊢ (∃ a, s = {a}) → s.Nonempty ∧ s.Subsingleton

case refine_2
α : Type u
s : Set α
h : s.Nonempty ∧ s.Subsingleton
⊢ ∃ a, s = {a}

Proof state:
case refine_1.intro
α : Type u
a : α
⊢ {a}.Nonempty ∧ {a}.Subsingleton

Tactic:
exact ⟨singleton_nonempty a, subsingleton_singleton⟩

Result:
no goals

Proof state:
case refine_1
α : Type u
s : Set α
⊢ (∃ a, s = {a}) → s.Nonempty ∧ s.Subsingleton

Tactic:
rintro ⟨a, rfl⟩

Result:
case refine_1.intro
α : Type u
a : α
⊢ {a}.Nonempty ∧ {a}.Subsingleton
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem DifferentiableWithinAt.mono (h : DifferentiableWithinAt 𝕜 f t x) (st : s ⊆ t) :
    DifferentiableWithinAt 𝕜 f s x

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
st : s ⊆ t
f' : E →L[𝕜] F
hf' : HasFDerivWithinAt f f' t x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact ⟨f', hf'.mono st⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
h : DifferentiableWithinAt 𝕜 f t x
st : s ⊆ t
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases h with ⟨f', hf'⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
st : s ⊆ t
f' : E →L[𝕜] F
hf' : HasFDerivWithinAt f f' t x
⊢ DifferentiableWithinAt 𝕜 f s x
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma Walk.IsCycle.adj_toSubgraph_iff_of_isCycles [LocallyFinite G] {u} {p : G.Walk u u}
    (hp : p.IsCycle) (hcyc : G.IsCycles) (hv : v ∈ p.toSubgraph.verts) :
    ∀ w, p.toSubgraph.Adj v w ↔ G.Adj v w

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ (p.toSubgraph.neighborSet v).ncard ≠ 0

Tactic:
simp [Set.Nonempty.mono,
hp.ncard_neighborSet_toSubgraph_eq_two (by aesop), Set.nonempty_of_ncard_ne_zero]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ ?m.105361 ∈ p.support

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ Inhabited (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
apply Classical.inhabited_of_nonempty

Result:
case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Proof state:
case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ Nonempty (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Tactic:
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _),
    ← Set.cast_ncard (finite_neighborSet_toSubgraph p), hcyc
      (Set.Nonempty.mono (p.toSubgraph.neighborSet_subset v) <|
        Set.nonempty_of_ncard_ne_zero <| by simp [Set.Nonempty.mono,
        hp.ncard_neighborSet_toSubgraph_eq_two (by aesop), Set.nonempty_of_ncard_ne_zero]),
    hp.ncard_neighborSet_toSubgraph_eq_two (by aesop)]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
⊢ ∀ (w : V), p.toSubgraph.Adj v w ↔ G.Adj v w

Tactic:
refine fun w ↦ Subgraph.adj_iff_of_neighborSet_equiv (?_ : Inhabited _).default (Set.toFinite _)

Result:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ Inhabited (↑(G.neighborSet v) ≃ ↑(p.toSubgraph.neighborSet v))

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : G.LocallyFinite
u : V
p : G.Walk u u
hp : p.IsCycle
hcyc : G.IsCycles
hv : v ∈ p.toSubgraph.verts
w : V
⊢ v ∈ p.support

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/Sheaves/Alexandrov.lean
theorem isSheaf_principalsKanExtension
    {X : TopCat.{v}} [Preorder X] [Topology.IsUpperSet X] (F : X ⥤ C) :
    Presheaf.IsSheaf (principalsKanExtension F)

Proof state:
case val
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op)

Tactic:
apply isLimit

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
⊢ IsSheafOpensLeCover (principalsKanExtension F)

Tactic:
intro ι Us

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ Nonempty (IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
⊢ TopCat.Presheaf.IsSheaf (principalsKanExtension F)

Tactic:
rw [isSheaf_iff_isSheafOpensLeCover]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
⊢ IsSheafOpensLeCover (principalsKanExtension F)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ Nonempty (IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op))

Tactic:
constructor

Result:
case val
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasLimits C
X : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
ι : Type v
Us : ι → Opens ↑X
⊢ IsLimit ((principalsKanExtension F).mapCone (opensLeCoverCocone Us).op)
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem finset_inf_factors {I : Type*} {A B : C} {s : Finset I} {P : I → Subobject B} (f : A ⟶ B) :
    (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

Tactic:
induction s using Finset.induction_on with
| empty => simp [top_factors]
| insert _ ih => simp [ih]

Result:
no goals

Proof state:
case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (s✝.inf P).Factors f ↔ ∀ i ∈ s✝, (P i).Factors f
⊢ ((insert a✝¹ s✝).inf P).Factors f ↔ ∀ i ∈ insert a✝¹ s✝, (P i).Factors f

Tactic:
simp [ih]

Result:
no goals

Proof state:
case empty
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ (∅.inf P).Factors f ↔ ∀ i ∈ ∅, (P i).Factors f

Tactic:
simp [top_factors]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

Tactic:
classical
induction s using Finset.induction_on with
| empty => simp [top_factors]
| insert _ ih => simp [ih]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem nextn : ∀ {s}, Valid s → s.toString.1 = m₁ ++ m₂ →
    ∀ n, s.nextn n ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + utf8Len (m₂.take n)⟩
  | _, h, e => by
    let ⟨l, m, r, h⟩ := h.validFor
    simp only [h.toString] at e; subst e; simp [h.nextn]

Proof state:
m₁ m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁ ++ m₂) r x✝
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }

Tactic:
simp [h.nextn]

Result:
no goals

Proof state:
m₁ m₂ : List Char
x✝ : Substring
h : x✝.Valid
e : x✝.toString.data = m₁ ++ m₂
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }

Tactic:
let ⟨l, m, r, h⟩ := h.validFor

Result:
m₁ m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁ ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }

Proof state:
m₁ m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
e : x✝.toString.data = m₁ ++ m₂
l m r : List Char
h : ValidFor l m r x✝
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }

Tactic:
simp only [h.toString] at e

Result:
m₁ m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ m₂
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }

Proof state:
m₁ m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l m r : List Char
h : ValidFor l m r x✝
e : m = m₁ ++ m₂
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }

Tactic:
subst e

Result:
m₁ m₂ : List Char
x✝ : Substring
h✝ : x✝.Valid
l r : List Char
h : ValidFor l (m₁ ++ m₂) r x✝
⊢ ∀ (n : Nat), x✝.nextn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + utf8Len (List.take n m₂) }
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem isClosed_iff_sup :
    IsClosed s ↔
      ∀ {ι : Type u}, Nonempty ι → ∀ f : ι → Ordinal, (∀ i, f i ∈ s) → ⨆ i, f i ∈ s

Proof state:
s : Set Ordinal.{u}
⊢ IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s

Tactic:
use fun hs ι hι f hf => (mem_closed_iff_sup hs).2 ⟨ι, hι, f, hf, rfl⟩

Result:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → IsClosed s

Proof state:
case mpr
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
x : Ordinal.{u}
hx : x ∈ closure s
⊢ x ∈ s

Tactic:
rcases mem_closure_iff_sup.1 hx with ⟨ι, hι, f, hf, rfl⟩

Result:
case mpr.intro.intro.intro.intro
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : sup f ∈ closure s
⊢ sup f ∈ s

Proof state:
case mpr.intro.intro.intro.intro
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
hx : sup f ∈ closure s
⊢ sup f ∈ s

Tactic:
exact h hι f hf

Result:
no goals

Proof state:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → IsClosed s

Tactic:
rw [← closure_subset_iff_isClosed]

Result:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → closure s ⊆ s

Proof state:
case mpr
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) → closure s ⊆ s

Tactic:
intro h x hx

Result:
case mpr
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
x : Ordinal.{u}
hx : x ∈ closure s
⊢ x ∈ s
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem eq_orthogonalProjection_of_eq_subspace {s s' : AffineSubspace ℝ P} [Nonempty s]
    [Nonempty s'] [HasOrthogonalProjection s.direction] [HasOrthogonalProjection s'.direction]
    (h : s = s') (p : P) : (orthogonalProjection s p : P) = (orthogonalProjection s' p : P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s s' : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s
inst✝² : Nonempty ↥s'
inst✝¹ : HasOrthogonalProjection s.direction
inst✝ : HasOrthogonalProjection s'.direction
h : s = s'
p : P
⊢ ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s') p)

Tactic:
subst h

Result:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s
inst✝² : HasOrthogonalProjection s.direction
p : P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s) p)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝³ : Nonempty ↥s
inst✝² : HasOrthogonalProjection s.direction
p : P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ ↑((orthogonalProjection s) p) = ↑((orthogonalProjection s) p)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/BorelCantelli.lean
theorem measure_limsup_cofinite_eq_zero {s : ι → Set α} (hs : ∑' i, μ (s i) ≠ ∞) :
    μ (limsup s cofinite) = 0

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
⊢ μ (limsup s cofinite) = 0

Tactic:
refine bot_unique <| ge_of_tendsto' (ENNReal.tendsto_tsum_compl_atTop_zero hs) fun t ↦ ?_

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ μ (limsup s cofinite) ≤ ∑' (b : { x // x ∉ t }), μ (s ↑b)

Proof state:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ ⨅ i, ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a ⊆ ⋃ x, ⋃ (hx : x ∉ t), s ↑⟨x, hx⟩

Tactic:
exact iInter₂_subset _ t.finite_toSet

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ μ (limsup s cofinite) ≤ μ (⋃ i, s ↑i)

Tactic:
gcongr

Result:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ limsup s cofinite ⊆ ⋃ i, s ↑i

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ μ (limsup s cofinite) ≤ ∑' (b : { x // x ∉ t }), μ (s ↑b)

Tactic:
calc
  μ (limsup s cofinite) ≤ μ (⋃ i : {i // i ∉ t}, s i) := by
    gcongr
    rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]
    exact iInter₂_subset _ t.finite_toSet
  _ ≤ ∑' i : {i // i ∉ t}, μ (s i) := measure_iUnion_le _

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ limsup s cofinite ⊆ ⋃ i, s ↑i

Tactic:
rw [hasBasis_cofinite.limsup_eq_iInf_iSup, iUnion_subtype]

Result:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ⊤
t : Finset ι
⊢ ⨅ i, ⨅ (_ : i.Finite), ⨆ a ∈ iᶜ, s a ⊆ ⋃ x, ⋃ (hx : x ∉ t), s ↑⟨x, hx⟩
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_apply_right (a : α) : toIocDiv hp a (a + p) = 0 :=
  toIocDiv_eq_of_sub_zsmul_mem_Ioc hp <| by simp [hp]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a + p - 0 • p ∈ Set.Ioc a (a + p)

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem PartiallyWellOrderedOn.prod {t : Set β} (hs : PartiallyWellOrderedOn s r)
    (ht : PartiallyWellOrderedOn t r') :
    PartiallyWellOrderedOn (s ×ˢ t) fun x y : α × β => r x.1 y.1 ∧ r' x.2 y.2

Proof state:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g₁ m)) ((Prod.fst ∘ f) (g₁ n))
m n : ℕ
hlt : m < n
hle : r' ((Prod.snd ∘ f ∘ ⇑g₁) m) ((Prod.snd ∘ f ∘ ⇑g₁) n)
⊢ ∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)

Tactic:
exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩

Result:
no goals

Proof state:
case intro
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g₁ m)) ((Prod.fst ∘ f) (g₁ n))
⊢ ∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)

Tactic:
obtain ⟨m, n, hlt, hle⟩ := ht (Prod.snd ∘ f ∘ g₁) fun n => (hf _).2

Result:
case intro.intro.intro.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g₁ m)) ((Prod.fst ∘ f) (g₁ n))
m n : ℕ
hlt : m < n
hle : r' ((Prod.snd ∘ f ∘ ⇑g₁) m) ((Prod.snd ∘ f ∘ ⇑g₁) n)
⊢ ∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun x y => r x.1 y.1 ∧ r' x.2 y.2

Tactic:
intro f hf

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
⊢ ∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)

Tactic:
obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq (Prod.fst ∘ f) fun n => (hf n).1

Result:
case intro
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g₁ m)) ((Prod.fst ∘ f) (g₁ n))
⊢ ∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_neg_iff {x y : PGame} : y ⧏ -x ↔ x ⧏ -y

Proof state:
x y : PGame
⊢ y ⧏ -x ↔ x ⧏ -y

Tactic:
rw [← neg_neg x, neg_lf_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem IsRadical.of_dvd [CancelCommMonoidWithZero R] {x y : R} (hy : IsRadical y) (h0 : y ≠ 0)
    (hxy : x ∣ y) : IsRadical x := (isRadical_iff_pow_one_lt 2 one_lt_two).2 <| by
  obtain ⟨z, rfl⟩ := hxy
  refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)
  rw [mul_pow, sq z]; exact mul_dvd_mul dvd (dvd_mul_left z z)

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1

Tactic:
refine fun w dvd ↦ ((mul_dvd_mul_iff_right <| right_ne_zero_of_mul h0).mp <| hy 2 _ ?_)

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ (w * z) ^ 2

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ w ^ 2 * (z * z)

Tactic:
exact mul_dvd_mul dvd (dvd_mul_left z z)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ (w * z) ^ 2

Tactic:
rw [mul_pow, sq z]

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
w : R
dvd : x ∣ w ^ 2
⊢ x * z ∣ w ^ 2 * (z * z)

Proof state:
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x y : R
hy : IsRadical y
h0 : y ≠ 0
hxy : x ∣ y
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1

Tactic:
obtain ⟨z, rfl⟩ := hxy

Result:
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
x z : R
hy : IsRadical (x * z)
h0 : x * z ≠ 0
⊢ ∀ (x_1 : R), x ∣ x_1 ^ 2 → x ∣ x_1
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one (i : ι × κ) (r : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) =
      Finsupp.single i.1 r ⊗ₜ Finsupp.single i.2 1

Proof state:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

Tactic:
nth_rw 1 [← mul_one r]

Result:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r * 1)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

Proof state:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst✝ : CommSemiring R
i : ι × κ
r : R
⊢ (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r * 1)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

Tactic:
exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Quotient.lean
theorem dense_image_mk {s : Set G} :
    Dense (mk '' s : Set (G ⧸ N)) ↔ Dense (s * (N : Set G))

Proof state:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousMul G
N : Subgroup G
s : Set G
⊢ Dense (mk '' s) ↔ Dense (s * ↑N)

Tactic:
rw [← dense_preimage_mk, preimage_image_mk_eq_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem cardinalMk_le_finrank [Module.Finite R M]
    {ι : Type w} {b : ι → M} (h : LinearIndependent R b) : #ι ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ lift.{max v w, w} #ι ≤ lift.{max v w, w} ↑(finrank R M)

Tactic:
simpa only [← finrank_eq_rank, lift_natCast, lift_le_nat_iff] using h.cardinal_lift_le_rank

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ #ι ≤ ↑(finrank R M)

Tactic:
rw [← lift_le.{max v w}]

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
⊢ lift.{max v w, w} #ι ≤ lift.{max v w, w} ↑(finrank R M)