harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_empty_of_one_mem {s : Set R} (h : (1 : R) ∈ s) : zeroLocus s = ∅

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal

Tactic:
exact hx h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ False

Tactic:
have eq_top : x.asIdeal = ⊤ := by
  rw [Ideal.eq_top_iff_one]
  exact hx h

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
eq_top : x.asIdeal = ⊤
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False

Tactic:
rw [mem_zeroLocus] at hx

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ x.asIdeal = ⊤

Tactic:
rw [Ideal.eq_top_iff_one]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ 1 ∈ x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ x.asIdeal.IsPrime

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
eq_top : x.asIdeal = ⊤
⊢ False

Tactic:
apply x_prime.ne_top eq_top

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ zeroLocus s = ∅

Tactic:
rw [Set.eq_empty_iff_forall_not_mem]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), x ∉ zeroLocus s

Tactic:
intro x hx

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False

Tactic:
have x_prime : x.asIdeal.IsPrime := by infer_instance

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ False
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Ioc_mul_Ico_subset' [LocallyFiniteOrder α] (a b c d : α) :
    Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d) :=
  Finset.coe_subset.mp <| by simpa using Set.Ioc_mul_Ico_subset' _ _ _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ioc a b * Ico c d) ⊆ ↑(Ioo (a * c) (b * d))

Tactic:
simpa using Set.Ioc_mul_Ico_subset' _ _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.IsOpen.ae_eq_empty_iff_eq (hU : IsOpen U) :
    U =ᵐ[μ] (∅ : Set X) ↔ U = ∅

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen U
⊢ U =ᶠ[ae μ] ∅ ↔ U = ∅

Tactic:
rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_map (f : S →+* T) (n : ℕ) :
    (ascPochhammer S n).map f = ascPochhammer T n

Proof state:
case succ
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
ih : map f (ascPochhammer S n) = ascPochhammer T n
⊢ map f (ascPochhammer S (n + 1)) = ascPochhammer T (n + 1)

Tactic:
simp [ih, ascPochhammer_succ_left, map_comp]

Result:
no goals

Proof state:
case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (ascPochhammer S 0) = ascPochhammer T 0

Tactic:
simp

Result:
no goals

Proof state:
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
⊢ map f (ascPochhammer S n) = ascPochhammer T n

Tactic:
induction n with
| zero => simp
| succ n ih => simp [ih, ascPochhammer_succ_left, map_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false

Proof state:
i : Nat
x : BitVec 0
⊢ x.getLsbD i = false

Tactic:
simp [getLsbD_zero_length]

Result:
no goals

Proof state:
w i : Nat
h : w = 0
x : BitVec w
⊢ x.getLsbD i = false

Tactic:
subst h

Result:
i : Nat
x : BitVec 0
⊢ x.getLsbD i = false
-- Mathlib/Geometry/Manifold/Instances/Real.lean
theorem frontier_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
    frontier { y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i } = { y | a = y i }

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ frontier {y | a ≤ y i} = {y | a = y i}

Tactic:
rw [frontier, closure_halfSpace, interior_halfSpace]

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ {y | a ≤ y i} \ {y | a < y i} = {y | a = y i}

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ {y | a ≤ y i} \ {y | a < y i} = {y | a = y i}

Tactic:
ext y

Result:
case h
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
y : PiLp p fun x => ℝ
⊢ y ∈ {y | a ≤ y i} \ {y | a < y i} ↔ y ∈ {y | a = y i}

Proof state:
case h
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
y : PiLp p fun x => ℝ
⊢ y ∈ {y | a ≤ y i} \ {y | a < y i} ↔ y ∈ {y | a = y i}

Tactic:
simpa only [mem_diff, mem_setOf_eq, not_lt] using antisymm_iff

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem mem_normalizer_fintype {S : Set G} [Finite S] {x : G} (h : ∀ n, n ∈ S → x * n * x⁻¹ ∈ S) :
    x ∈ Subgroup.setNormalizer S

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
⊢ x ∈ setNormalizer S

Tactic:
haveI := Set.fintypeImage S fun n => x * n * x⁻¹

Result:
case intro
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
⊢ x ∈ setNormalizer S

Proof state:
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
⊢ x ∈ setNormalizer S

Tactic:
haveI := Classical.propDecidable

Result:
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ setNormalizer S

Proof state:
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ setNormalizer S

Tactic:
cases nonempty_fintype S

Result:
case intro
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
⊢ x ∈ setNormalizer S

Proof state:
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑((fun n => x * n * x⁻¹) '' S)

Tactic:
rw [Set.card_image_of_injective S conj_injective]

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ n ∈ S, x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
⊢ x ∈ setNormalizer S

Tactic:
exact fun n =>
  ⟨h n, fun h₁ =>
    have heq : (fun n => x * n * x⁻¹) '' S = S :=
      Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
        (by rw [Set.card_image_of_injective S conj_injective])
    have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
    let ⟨y, hy⟩ := this
    conj_injective hy.2 ▸ hy.1⟩

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
/-- special case of `mul_dvd_mul_iff_left` for `ℕ`.
Duplicated here to keep simple imports for this file. -/
protected lemma mul_dvd_mul_iff_left (ha : 0 < a) : a * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d ↦ by rw [Nat.mul_assoc, Nat.mul_right_inj <| ne_of_gt ha]

Proof state:
a b c : ℕ
ha : 0 < a
d : ℕ
⊢ a * c = a * b * d ↔ c = b * d

Tactic:
rw [Nat.mul_assoc, Nat.mul_right_inj <| ne_of_gt ha]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem _root_.ContinuousOn.angle_sign_comp {α : Type*} [TopologicalSpace α] {f : α → Angle}
    {s : Set α} (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ π) :
    ContinuousOn (sign ∘ f) s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
θ : Angle
hθ : θ ∈ f '' s
⊢ ContinuousAt sign θ

Tactic:
obtain ⟨z, hz, rfl⟩ := hθ

Result:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)

Proof state:
case intro.intro
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
z : α
hz : z ∈ s
⊢ ContinuousAt sign (f z)

Tactic:
exact continuousAt_sign (hs _ hz).1 (hs _ hz).2

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
⊢ ContinuousOn (sign ∘ f) s

Tactic:
refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)

Result:
α : Type u_1
inst✝ : TopologicalSpace α
f : α → Angle
s : Set α
hf : ContinuousOn f s
hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑π
θ : Angle
hθ : θ ∈ f '' s
⊢ ContinuousAt sign θ
-- Mathlib/Data/Multiset/UnionInter.lean
lemma union_le (h₁ : s ≤ u) (h₂ : t ≤ u) : s ∪ t ≤ u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t

Tactic:
exact union_le_union_right h₁ t

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u

Tactic:
rw [← eq_union_left h₂]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
-- Mathlib/Data/Nat/EvenOddRec.lean
theorem evenOddRec_even {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) (n : ℕ) :
    (2 * n).evenOddRec h0 h_even h_odd = h_even n (evenOddRec h0 h_even h_odd n)

Proof state:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → false = true)

Tactic:
simp [H]

Result:
no goals

Proof state:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ evenOddRec h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n)

Tactic:
apply binaryRec_eq false n

Result:
P : ℕ → Sort u_1
h0 : P 0
h_even : (i : ℕ) → P i → P (2 * i)
h_odd : (i : ℕ) → P i → P (2 * i + 1)
H : h_even 0 h0 = h0
n : ℕ
⊢ (match false, 0, h0 with
      | false, i, hi => h_even i hi
      | true, i, hi => h_odd i hi) =
      h0 ∨
    (n = 0 → false = true)
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_add_withDensity_rnDeriv_eq [s.HaveLebesgueDecomposition μ] :
    s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s

Proof state:
case h.e'_3.h.e'_6.h.e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart =
    s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)

Tactic:
exact s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasFDerivWithinAt.of_nhdsWithin_eq_bot (h : 𝓝[s\{x}] x = ⊥) :
    HasFDerivWithinAt f f' s x

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
f' : E →L[𝕜] F
x : E
s : Set E
h : 𝓝[s \ {x}] x = ⊥
⊢ (fun x' => f x' - f x - f' (x' - x)) =o[𝕜;⊥] fun x' => x' - x

Tactic:
exact .bot

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
f' : E →L[𝕜] F
x : E
s : Set E
h : 𝓝[s \ {x}] x = ⊥
⊢ HasFDerivWithinAt f f' s x

Tactic:
rw [← hasFDerivWithinAt_diff_singleton x, HasFDerivWithinAt, h,
  hasFDerivAtFilter_iff_isLittleOTVS]

Result:
𝕜 : 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
f' : E →L[𝕜] F
x : E
s : Set E
h : 𝓝[s \ {x}] x = ⊥
⊢ (fun x' => f x' - f x - f' (x' - x)) =o[𝕜;⊥] fun x' => x' - x
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma mem_ball_dynEntourage_comp (T : X → X) (n : ℕ) {U : Set (X × X)} (U_symm : SymmetricRel U)
    (x y : X) (h : (ball x (dynEntourage T U n) ∩ ball y (dynEntourage T U n)).Nonempty) :
    x ∈ ball y (dynEntourage T (U ○ U) n)

Proof state:
case intro.intro
X : Type u_1
T : X → X
n : ℕ
U : Set (X × X)
U_symm : SymmetricRel U
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
rw [mem_ball_symmetry (SymmetricRel.dynEntourage T U_symm n)] at z_Bx

Result:
case intro.intro
X : Type u_1
T : X → X
n : ℕ
U : Set (X × X)
U_symm : SymmetricRel U
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Proof state:
X : Type u_1
T : X → X
n : ℕ
U : Set (X × X)
U_symm : SymmetricRel U
x y : X
h : (ball x (dynEntourage T U n) ∩ ball y (dynEntourage T U n)).Nonempty
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
rcases h with ⟨z, z_Bx, z_By⟩

Result:
case intro.intro
X : Type u_1
T : X → X
n : ℕ
U : Set (X × X)
U_symm : SymmetricRel U
x y z : X
z_Bx : z ∈ ball x (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Proof state:
case intro.intro
X : Type u_1
T : X → X
n : ℕ
U : Set (X × X)
U_symm : SymmetricRel U
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
exact dynEntourage_comp_subset T U U n (mem_ball_comp z_By z_Bx)

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma groupCohomologyπ_comp_isoH1_hom  :
    groupCohomologyπ A 1 ≫ (isoH1 A).hom = (isoOneCocycles A).hom ≫ H1π A

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ groupCohomologyπ A 1 ≫ (isoH1 A).hom = (isoOneCocycles A).hom ≫ H1π A

Tactic:
simp [isoH1, isoOneCocycles]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem cauchyFilter_eq {α : Type*} [UniformSpace α] [CompleteSpace α] [T0Space α]
    {f g : CauchyFilter α} :
    haveI := f.2.1.nonempty; lim f.1 = lim g.1 ↔ Inseparable f g

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : T0Space α
f g : CauchyFilter α
⊢ lim ↑f = lim ↑g ↔ Inseparable f g

Tactic:
rw [← inseparable_iff_eq, inseparable_lim_iff]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem countable_cover_nhds_of_sigmaCompact {f : X → Set X} (hf : ∀ x, f x ∈ 𝓝 x) :
    ∃ s : Set X, s.Countable ∧ ⋃ x ∈ s, f x = univ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
  ⟨s, -, hsc, hsU⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
s : Set X
hsc : s.Countable
hsU : univ ⊆ ⋃ x ∈ s, f x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
s : Set X
hsc : s.Countable
hsU : univ ⊆ ⋃ x ∈ s, f x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
exact ⟨s, hsc, univ_subset_iff.1 hsU⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
simp only [← nhdsWithin_univ] at hf

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem split_eq_scale_split' : ∀ {o o' m} [NF o], split' o = (o', m) → split o = (scale 1 o', m)
  | 0, o', m, _, p => by injection p; substs o' m; rfl
  | oadd e n a, o', m, h, p => by
    by_cases e0 : e = 0 <;> simp only [split', e0, ↓reduceIte, Prod.mk.injEq, split] at p ⊢
    · rcases p with ⟨rfl, rfl⟩
      exact ⟨rfl, rfl⟩
    · revert p
      rcases h' : split' a with ⟨a', m'⟩
      haveI := h.fst
      haveI := h.snd
      simp only [split_eq_scale_split' h', and_imp]
      have : 1 + (e - 1) = e

Proof state:
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
this : ¬e.repr = repr 0
⊢ 1 + (e.repr - 1) = e.repr

Tactic:
exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem countP_attach (l : Vector α n) (p : α → Bool) :
    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP (fun a => p a.val) { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
p : α → Bool
⊢ countP (fun a => p a.val) l.attach = countP p l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ countP (fun a => p a.val) { toArray := toArray✝, size_toArray := size_toArray✝ }.attach =
    countP p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Data/Complex/Basic.lean
theorem I_mul_im (z : ℂ) : (I * z).im = z.re

Proof state:
z : ℂ
⊢ (I * z).im = z.re

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem zero_cpow_eq_nhds {b : ℂ} (hb : b ≠ 0) : (fun x : ℂ => (0 : ℂ) ^ x) =ᶠ[𝓝 b] 0

Proof state:
b : ℂ
hb : b ≠ 0
⊢ (fun x => 0 ^ x) =ᶠ[𝓝 b] 0

Tactic:
suffices ∀ᶠ x : ℂ in 𝓝 b, x ≠ 0 from
  this.mono fun x hx ↦ by
    dsimp only
    rw [zero_cpow hx, Pi.zero_apply]

Result:
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0

Proof state:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ (fun x => 0 ^ x) x = 0 x

Tactic:
dsimp only

Result:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = 0 x

Proof state:
b : ℂ
hb : b ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0
x : ℂ
hx : x ≠ 0
⊢ 0 ^ x = 0 x

Tactic:
rw [zero_cpow hx, Pi.zero_apply]

Result:
no goals

Proof state:
b : ℂ
hb : b ≠ 0
⊢ ∀ᶠ (x : ℂ) in 𝓝 b, x ≠ 0

Tactic:
exact IsOpen.eventually_mem isOpen_ne hb

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem add_eq_eval₃ [Semiring R] [AddCommMonoid M] [Module R M] {a₁ : R × M} (a₂ : R × M)
    {l₁ l₂ l : NF R M} (h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval) :
    (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + (l₁.eval + (a₂.1 • a₂.2 + l₂.eval)) = a₁.1 • a₁.2 + (l₁.eval + (l₂.eval + a₂.1 • a₂.2))

Tactic:
congr! 2

Result:
case h.e'_6.h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₂.1 • a₂.2 + l₂.eval = l₂.eval + a₂.1 • a₂.2

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₁.1 • a₁.2 + l₁.eval + l₂.eval + a₂.1 • a₂.2

Tactic:
simp only [add_assoc]

Result:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + (l₁.eval + (a₂.1 • a₂.2 + l₂.eval)) = a₁.1 • a₁.2 + (l₁.eval + (l₂.eval + a₂.1 • a₂.2))

Proof state:
case h.e'_6.h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₂.1 • a₂.2 + l₂.eval = l₂.eval + a₂.1 • a₂.2

Tactic:
rw [add_comm]

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]

Result:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₂.1 • a₂.2 + (a₁.1 • a₁.2 + l₁.eval + l₂.eval)

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₂.1 • a₂.2 + (a₁.1 • a₁.2 + l₁.eval + l₂.eval)

Tactic:
nth_rw 4 [add_comm]

Result:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval
⊢ a₁.1 • a₁.2 + l₁.eval + (a₂.1 • a₂.2 + l₂.eval) = a₁.1 • a₁.2 + l₁.eval + l₂.eval + a₂.1 • a₂.2