harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem tendsto_embedBox_toFilteriUnion_top (l : IntegrationParams) (h : I ≤ J) :
    Tendsto (TaggedPrepartition.embedBox I J h) (l.toFilteriUnion I ⊤)
      (l.toFilteriUnion J (Prepartition.single J I h))

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ Tendsto (⇑(embedBox I J h)) (toFilteriUnion I ⊤) (toFilteriUnion J (Prepartition.single J I h))

Tactic:
simp only [toFilteriUnion, tendsto_iSup]

Result:
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
l : IntegrationParams
h : I ≤ J
⊢ ∀ (i : ℝ≥0),
    Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I i ⊤)
      (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))
-- Mathlib/Data/Multiset/Filter.lean
theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f)
    (x : α) : (s.map f).count (f x) = s.count x

Proof state:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
⊢ ¬∃ a ∈ s, f a = f x

Tactic:
rintro ⟨k, hks, hkx⟩

Result:
case neg.intro.intro
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
k : α
hks : k ∈ s
hkx : f k = f x
⊢ False

Proof state:
case neg.intro.intro
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
k : α
hks : k ∈ s
hkx : f k = f x
⊢ False

Tactic:
rw [hf hkx] at hks

Result:
case neg.intro.intro
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
k : α
hks : x ∈ s
hkx : f k = f x
⊢ False

Proof state:
case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
exact count_map_eq_count f _ hf.injOn _ H

Result:
no goals

Proof state:
case neg.intro.intro
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
k : α
hks : x ∈ s
hkx : f k = f x
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
⊢ count (f x) (map f s) = count x s

Tactic:
by_cases H : x ∈ s

Result:
case pos
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∈ s
⊢ count (f x) (map f s) = count x s

case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
⊢ count (f x) (map f s) = count x s

Proof state:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count_eq_zero_of_not_mem H, count_eq_zero, mem_map]

Result:
case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : x ∉ s
⊢ ¬∃ a ∈ s, f a = f x
-- Mathlib/Order/Interval/Set/SurjOn.lean
theorem surjOn_Icc_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f)
    {a b : α} (hab : a ≤ b) : SurjOn f (Icc a b) (Icc (f a) (f b))

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f b ∈ Icc (f a) (f b)
⊢ f b ∈ f '' Icc a b

Tactic:
exact ⟨b, right_mem_Icc.mpr hab, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
⊢ SurjOn f (Icc a b) (Icc (f a) (f b))

Tactic:
intro p hp

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
⊢ p ∈ f '' Icc a b

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f a ∈ Icc (f a) (f b)
⊢ f a ∈ f '' Icc a b

Tactic:
exact ⟨a, left_mem_Icc.mpr hab, rfl⟩

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Icc a b

Tactic:
exact image_subset f Ioo_subset_Icc_self <|
  surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
⊢ p ∈ f '' Icc a b

Tactic:
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f a ∈ Icc (f a) (f b)
⊢ f a ∈ f '' Icc a b

case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f b ∈ Icc (f a) (f b)
⊢ f b ∈ f '' Icc a b

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Icc a b
-- Mathlib/Data/Nat/Bitwise.lean
lemma bit_mod_two_eq_zero_iff (a x) :
    bit a x % 2 = 0 ↔ !a

Proof state:
a : Bool
x : ℕ
⊢ bit a x % 2 = 0 ↔ (!a) = true

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem edist_def (f g : α →₁[μ] β) : edist f g = ∫⁻ a, edist (f a) (g a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (if 1 = ⊤ then eLpNormEssSup (↑↑f - ↑↑g) μ else ∫⁻ (a : α), ‖↑↑f a - ↑↑g a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ

Tactic:
simp [edist_eq_enorm_sub]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ edist f g = ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ

Tactic:
simp only [Lp.edist_def, eLpNorm, one_ne_zero, eLpNorm'_eq_lintegral_enorm, Pi.sub_apply,
  one_toReal, ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (if 1 = ⊤ then eLpNormEssSup (↑↑f - ↑↑g) μ else ∫⁻ (a : α), ‖↑↑f a - ↑↑g a‖ₑ ∂μ) =
    ∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem leadingCoeff_cubic (ha : a ≠ 0) :
    leadingCoeff (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = a

Proof state:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).leadingCoeff = a

Tactic:
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2), add_comm,
  leadingCoeff_add_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
  leadingCoeff_C_mul_X_pow]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto
    (hF : UniformCauchySeqOnFilter F p p')
    (hF' : ∀ᶠ x : α in p', Tendsto (fun n => F n x) p (𝓝 (f x))) :
    TendstoUniformlyOnFilter F f p p'

Proof state:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t

Tactic:
have := hx.and (hm' ht)

Result:
case inr.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n => F n x.2) p (𝓝 (f x.2))
this✝ :
  ∀ᶠ (x : (α × ι) × ι) in (p' ×ˢ p) ×ˢ p,
    (F ((Equiv.prodAssoc α ι ι) x).swap.1.1 ((Equiv.prodAssoc α ι ι) x).swap.2,
          F ((Equiv.prodAssoc α ι ι) x).swap.1.2 ((Equiv.prodAssoc α ι ι) x).swap.2) ∈
        t ∧
      Tendsto (fun n => F n ((Equiv.prodAssoc α ι ι) x).swap.2) p (𝓝 (f ((Equiv.prodAssoc α ι ι) x).swap.2))
x : α
n : ι
hx : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t
hm' : Tendsto (fun x_1 => (f x, F x_1 x)) p (𝓤 β)
this : ∀ᶠ (x_1 : ι) in p, (F n x, F x_1 x) ∈ t ∧ (fun x_2 => (f x, F x_2 x)) x_1 ∈ t
⊢ ∃ z, (f x, z) ∈ t ∧ (z, F n x) ∈ t

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f p p'

Tactic:
rcases p.eq_or_neBot with rfl | _

Result:
case inl
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p' : Filter α
hF : UniformCauchySeqOnFilter F ⊥ p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) ⊥ (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f ⊥ p'

case inr
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n => F n x) p (𝓝 (f x))
h✝ : p.NeBot
⊢ TendstoUniformlyOnFilter F f p p'
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_stream_nth_rat_eq (v_eq_q : v = (↑q : K)) (n : ℕ) :
    ((IntFractPair.stream q n).map (mapFr (↑)) : Option <| IntFractPair K) =
      IntFractPair.stream v n

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
IH : some { b := b, fr := ↑fr } = IntFractPair.stream (↑q) n
⊢ (↑fr)⁻¹ = ↑fr⁻¹

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma connected_iff_exists_forall_reachable : G.Connected ↔ ∃ v, ∀ w, G.Reachable v w

Proof state:
case mpr
V : Type u
G : SimpleGraph V
⊢ (∃ v, ∀ (w : V), G.Reachable v w) → G.Preconnected ∧ Nonempty V

Tactic:
rintro ⟨v, h⟩

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
v : V
h : ∀ (w : V), G.Reachable v w
⊢ G.Preconnected ∧ Nonempty V

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
v : V
h : ∀ (w : V), G.Reachable v w
⊢ G.Preconnected ∧ Nonempty V

Tactic:
exact ⟨fun u w => (h u).symm.trans (h w), ⟨v⟩⟩

Result:
no goals

Proof state:
case mp.intro.intro
V : Type u
G : SimpleGraph V
hp : G.Preconnected
v : V
⊢ ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
exact ⟨v, fun w => hp v w⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.Connected ↔ ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
rw [connected_iff]

Result:
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ v, ∀ (w : V), G.Reachable v w

Proof state:
case mp
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V → ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
rintro ⟨hp, ⟨v⟩⟩

Result:
case mp.intro.intro
V : Type u
G : SimpleGraph V
hp : G.Preconnected
v : V
⊢ ∃ v, ∀ (w : V), G.Reachable v w

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V ↔ ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
⊢ G.Preconnected ∧ Nonempty V → ∃ v, ∀ (w : V), G.Reachable v w

case mpr
V : Type u
G : SimpleGraph V
⊢ (∃ v, ∀ (w : V), G.Reachable v w) → G.Preconnected ∧ Nonempty V
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0)
    (h : ∀ a, p a ↔ q a ∧ QuasispectrumRestricts a f) :
    NonUnitalContinuousFunctionalCalculus R p where
  predicate_zero := h0
  compactSpace_quasispectrum a

Proof state:
case h.mpr.intro
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁴ : Semifield R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Field S
inst✝¹⁸ : StarRing S
inst✝¹⁷ : MetricSpace S
inst✝¹⁶ : IsTopologicalRing S
inst✝¹⁵ : ContinuousStar S
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module S A
inst✝¹¹ : IsScalarTower S A A
inst✝¹⁰ : SMulCommClass S A A
inst✝⁹ : Algebra R S
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
y : ↑(σₙ R a)
⊢ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
      ⟨(algebraMap R S) ↑y, ⋯⟩ =
    (algebraMap R S) (g y)

Tactic:
simp only [nonUnitalStarAlgHom_postcomp_apply, NonUnitalStarAlgHom.coe_coe,
  Function.comp_apply, comp_apply, coe_mk, ContinuousMap.coe_mk, StarAlgHom.ofId_apply]

Result:
case h.mpr.intro
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁴ : Semifield R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Field S
inst✝¹⁸ : StarRing S
inst✝¹⁷ : MetricSpace S
inst✝¹⁶ : IsTopologicalRing S
inst✝¹⁵ : ContinuousStar S
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module S A
inst✝¹¹ : IsScalarTower S A A
inst✝¹⁰ : SMulCommClass S A A
inst✝⁹ : Algebra R S
inst✝⁸ : Module R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
y : ↑(σₙ R a)
⊢ (algebraMap R S) (g (Subtype.map ⇑f ⋯ ⟨(algebraMap R S) ↑y, ⋯⟩)) = (algebraMap R S) (g y)
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_of_s_rat_eq (v_eq_q : v = (↑q : K)) :
    ((of q).s.map (Pair.map ((↑))) : Stream'.Seq <| Pair K) = (of v).s

Proof state:
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
a✝ : Pair K
⊢ a✝ ∈ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n ↔ a✝ ∈ (of v).s.get? n

Tactic:
rw [← coe_of_s_get?_rat_eq v_eq_q]

Result:
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
a✝ : Pair K
⊢ a✝ ∈ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n ↔ a✝ ∈ Option.map (Pair.map Rat.cast) ((of q).s.get? n)

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s

Tactic:
ext n

Result:
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
a✝ : Pair K
⊢ a✝ ∈ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n ↔ a✝ ∈ (of v).s.get? n

Proof state:
case h.a
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
a✝ : Pair K
⊢ a✝ ∈ (Stream'.Seq.map (Pair.map Rat.cast) (of q).s).get? n ↔ a✝ ∈ Option.map (Pair.map Rat.cast) ((of q).s.get? n)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn_map [Monad m] [LawfulMonad m]
    (l : Array α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
    forIn (l.map g) init f = forIn l init fun a y => f (g a) y

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → γ → m (ForInStep γ)
toList✝ : List α
⊢ forIn (map g { toList := toList✝ }) init f = forIn { toList := toList✝ } init fun a y => f (g a) y

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
g : α → β
f : β → γ → m (ForInStep γ)
⊢ forIn (map g l) init f = forIn l init fun a y => f (g a) y

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
f : β → γ → m (ForInStep γ)
toList✝ : List α
⊢ forIn (map g { toList := toList✝ }) init f = forIn { toList := toList✝ } init fun a y => f (g a) y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_modify_self (h : m.1.WF) [Inhabited α] {k fallback : α} {f : β k → β k} :
    (m.modify k f).getKeyD k fallback = if m.contains k then k else fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
inst✝ : Inhabited α
k fallback : α
f : β k → β k
⊢ (m.modify k f).getKeyD k fallback = if m.contains k = true then k else fallback

Tactic:
simp_to_model [modify] using List.getKeyD_modifyKey_self

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_le_of_omega0_le_left {a : Ordinal} (ha : ω ≤ a) (b : Ordinal) :
    (a ^ b).card ≤ max a.card b.card

Proof state:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ Cardinal.lift.{u_1, u_1} b.card * ⨆ a_1, (a ^ ↑a_1).card ≤ a.card ⊔ b.card

Tactic:
rw [Cardinal.lift_id, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]

Result:
case refine_3
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ (⨆ a_1, (a ^ ↑a_1).card) ⊔ b.card ≤ a.card ⊔ b.card

case refine_3.h'
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ b.card ≠ 0

case refine_3.h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ℵ₀ ≤ ⨆ a_1, (a ^ ↑a_1).card

Proof state:
case h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
⊢ ∀ (i : ↑(Iio b)), (a ^ ↑i).card ≤ a.card ⊔ b.card

Tactic:
intro c

Result:
case h
a : Ordinal.{u_1}
ha : ω ≤ a
b✝ b : Ordinal.{u_1}
hb : b.IsLimit
IH : ∀ o' < b, (a ^ o').card ≤ a.card ⊔ o'.card
c : ↑(Iio b)
⊢ (a ^ ↑c).card ≤ a.card ⊔ b.card
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasurableSet.exists_isOpen_symmDiff_lt [InnerRegularCompactLTTop μ]
    [IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α]
    {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ U, IsOpen U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Tactic:
rcases hs.exists_isCompact_isClosed_diff_lt hμs this with ⟨K, hKs, hKco, hKcl, hμK⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed K
hμK : μ (s \ K) < ε / 2
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed K
hμK : μ (s \ K) < ε / 2
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Tactic:
rcases hKco.exists_isOpen_lt_add (μ := μ) this with ⟨U, hKU, hUo, hμU⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen U
hμU : μ U < μ K + ε / 2
⊢ ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (U ∆ s) < ε

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen U
hμU : μ U < μ K + ε / 2
⊢ μ K ≤ μ s

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen U
hμU : μ U < μ K + ε / 2
⊢ μ K ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top hμs (by gcongr)

Result:
no goals