awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h₁ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊥
h₂ : ((↑a : EReal), ⊥).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 ⊤
h₃ : ((↑a : EReal), ⊥).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
h₄ : ((↑a : EReal), ⊥).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊥).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊥)
have h₅ : ¬a = 0
Tactic: simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h₁ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊥
h₂ : ((↑a : EReal), ⊤).1 ≠ 0 ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 ⊤
h₃ : ((↑a : EReal), ⊤).1 ≠ ⊥ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
h₄ : ((↑a : EReal), ⊤).1 ≠ ⊤ ∨ Ne (α := EReal) ((↑a : EReal), ⊤).2 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) ((↑a : EReal), ⊤)
have h₅ : ¬a = 0
Tactic: simp only [ne_eq, EReal.coe_eq_zero, not_true_eq_false, or_false] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.EReal.Lemmas (hypothesis)
Goal:
a : ℝ
h₁ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊥
h₂ : Ne (α := EReal) (⊤, (↑a : EReal)).1 0 ∨ (⊤, (↑a : EReal)).2 ≠ ⊤
h₃ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊥ ∨ (⊤, (↑a : EReal)).2 ≠ 0
h₄ : Ne (α := EReal) (⊤, (↑a : EReal)).1 ⊤ ∨ (⊤, (↑a : EReal)).2 ≠ 0
⊢ ContinuousAt (Y := EReal) (fun (p : EReal × EReal) ↦ p.1 * p.2) (⊤, (↑a : EReal))
have h₅ : ¬a = 0
Tactic: simp only [ne_eq, not_true_eq_false, EReal.coe_eq_zero, false_or] at h₄
Cleared hypotheses: h₄
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
m n : ℤ
⊢ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = (↑|m - n| : ℝ)
have norm_cast : |m - n| = |m - n|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
have norm_cast : 1 ≤ |m - n|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |m - n|
have rwa : HAdd.hAdd (α := ℤ) 0 1 ≤ |m - n|
Tactic: rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
m n : ℤ
hne : m ≠ n
rwa : HAdd.hAdd (α := ℤ) 0 1 ≤ |m - n|
⊢ 1 ≤ |m - n|
have rwa₁ : 0 < |m - n|
Tactic: rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
m n : ℤ
hne : m ≠ n
rwa : HAdd.hAdd (α := ℤ) 0 1 ≤ |m - n|
rwa₁ : 0 < |m - n|
⊢ 1 ≤ |m - n|
have rwa₂ : m - n ≠ 0
Tactic: rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
have rw : preimage (β := ℝ) Int.cast (ball (↑x : ℝ) r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
Tactic: rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
rw : preimage (β := ℝ) Int.cast (ball (↑x : ℝ) r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
⊢ ball x r = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
have rw₁ : Int.cast ⁻¹' Ioo ((↑x : ℝ) - r) ((↑x : ℝ) + r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
Tactic: rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
rw : preimage (β := ℝ) Int.cast (ball (↑x : ℝ) r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
rw₁ : Int.cast ⁻¹' Ioo ((↑x : ℝ) - r) ((↑x : ℝ) + r) = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
⊢ ball x r = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
have rw₂ : Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉ = Ioo ⌊(↑x : ℝ) - r⌋ ⌈(↑x : ℝ) + r⌉
Tactic: rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
have rw : preimage (β := ℝ) Int.cast (closedBall (↑x : ℝ) r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
Tactic: rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
rw : preimage (β := ℝ) Int.cast (closedBall (↑x : ℝ) r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
have rw₁ : Int.cast ⁻¹' Icc ((↑x : ℝ) - r) ((↑x : ℝ) + r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
Tactic: rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
rw : preimage (β := ℝ) Int.cast (closedBall (↑x : ℝ) r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
rw₁ : Int.cast ⁻¹' Icc ((↑x : ℝ) - r) ((↑x : ℝ) + r) = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
have rw₂ : Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋ = Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋
Tactic: rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
x : ℤ
r : ℝ
⊢ IsCompact (closedBall x r)
have rw : IsCompact (Icc ⌈(↑x : ℝ) - r⌉ ⌊(↑x : ℝ) + r⌋)
Tactic: rw [closedBall_eq_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
⊢ Eq (α := Filter ℤ) cofinite (atBot ⊔ atTop)
have rw : cocompact ℤ = atBot ⊔ atTop
Tactic: rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]
-- Lean 4 proof step from Mathlib.Topology.Instances.Int (goal)
Goal:
rw : cocompact ℤ = atBot ⊔ atTop
⊢ Eq (α := Filter ℤ) cofinite (atBot ⊔ atTop)
have rw₁ : Eq (α := Filter ℤ) (atBot ⊔ atTop) (atBot ⊔ atTop)
Tactic: rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (goal)
Goal:
⊢ Dense (X := ℝ) {x : ℝ | Irrational x}
have refine : ∀ (o : Set ℝ),
  Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) o →
    o.Nonempty → (o ∩ {x : ℝ | Irrational x}).Nonempty
Tactic: refine Real.isTopologicalBasis_Ioo_rat.dense_iff.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (goal)
Goal:
⊢ ∀ (o : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) o →
      o.Nonempty → (o ∩ {x : ℝ | Irrational x}).Nonempty
have simp : ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo (↑x : ℝ) (↑x_1 : ℝ) → o.Nonempty → (o ∩ {x : ℝ | Irrational x}).Nonempty
Tactic: simp only [mem_iUnion, mem_singleton_iff, exists_prop, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (goal)
Goal:
a b : ℚ
hlt : a < b
h : Set.Nonempty (α := ℝ) (Ioo (↑a : ℝ) (↑b : ℝ))
⊢ Set.Nonempty (α := ℝ) (Ioo (↑a : ℝ) (↑b : ℝ) ∩ {x : ℝ | Irrational x})
have rw : Set.Nonempty (α := ℝ) ({x : ℝ | Irrational x} ∩ Ioo (↑a : ℝ) (↑b : ℝ))
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (hypothesis)
Goal:
x : ℝ
hx : Irrational x
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
have A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
Tactic: have A : IsClosed (range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ)) :=
    ((isClosedMap_smul₀ (n⁻¹ : ℝ)).comp Int.isClosedEmbedding_coe_real.isClosedMap).isClosed_range
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (hypothesis)
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
have B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
Tactic: have B : x ∉ range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ) := by
    rintro ⟨m, rfl⟩
    simp at hx
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (goal)
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
have rcases : ∀ (ε : ℝ) (ε0 : ε > 0) (hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ),
  ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
Tactic: rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (goal)
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
have refine : ∀ (δ : ℝ) (hδ : δ ≤ ε) (m : ℤ) (hlt : dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) < δ), False
Tactic: refine (ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (hypothesis)
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) < δ
⊢ False
have hlt₁ : dist (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) x < δ
Tactic: rw [dist_comm] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Topology.Instances.Irrational (goal)
Goal:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (X := ℝ) (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))
B : x ∉ range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ))ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)) x < δ
⊢ False
have refine : (fun (m : ℤ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑m : ℝ)) m = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: refine hε (ball_subset_ball hδ hlt) ⟨m, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ (A x).det
have simp_rw : Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦
  ∑ σ : Equiv.Perm n,
    HSMul.hSMul (α := ℤˣ) (β := R) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
      (∏ i : n, A x ((σ : (a : n) → n) i) i)
Tactic: simp_rw [Matrix.det_apply]
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
X : Type u_1
n : Type u_5
R : Type u_8
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Fintype n
inst_3 : DecidableEq n
inst_4 : CommRing R
inst_5 : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦
    ∑ σ : Equiv.Perm n,
      HSMul.hSMul (α := ℤˣ) (β := R) (((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) σ : ℤˣ)
        (∏ i : n, A x ((σ : (a : n) → n) i) i)
have refine : ∀ (l : Equiv.Perm n),
  Membership.mem (γ := Finset (Equiv.Perm n)) Finset.univ l →
    Continuous.{u_1, u_8} (Y := R) fun (x : X) ↦ ∏ i : n, A x ((l : (a : n) → n) i) i
Tactic: refine continuous_finsetSum _ fun l _ => Continuous.const_smul ?_ _
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦
    blockDiagonal' (m' := m') (n' := n') (A a) (Sigma.mk (β := fun (i : l) ↦ m' i) i₁ i₂)
      (Sigma.mk (β := fun (i : l) ↦ n' i) j₁ j₂)
have dsimp : Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ if h : i₁ = j₁ then A a i₁ i₂ (cast sorry j₂) else 0
Tactic: dsimp only [blockDiagonal'_apply']
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ if h : i₁ = j₁ then A a i₁ i₂ (cast ⋯ j₂) else 0
have pos : ∀ (h : i₁ = j₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast sorry j₂)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
pos : ∀ (h : i₁ = j₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ if h : i₁ = j₁ then A a i₁ i₂ (cast ⋯ j₂) else 0
have neg : ∀ (h : ¬i₁ = j₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace R
inst_2 : Zero R
inst_3 : DecidableEq l
A : X → (i : l) → Matrix.{u_9, u_10, u_8} (m' i) (n' i) R
hA : Continuous A
x : (i : l) × m' i
x_1 : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : i₁ = j₁
⊢ Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast ⋯ j₂)
have pos : ∀ (j₂ : n' i₁), Continuous.{u_1, u_8} (Y := R) fun (a : X) ↦ A a i₁ i₂ (cast sorry j₂)
Tactic: subst h
Cleared hypotheses: j₁, j₂, h
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
⊢ IsClosed (X := Matrix m m R) {M : Matrix m m R | M.BlockTriangular b}
have simp : IsClosed (X := Matrix m m R) (⋂ (i : m), ⋂ (i_1 : m), ⋂ (_ : b i_1 < b i), {x : Matrix m m R | x i i_1 = 0})
Tactic: simp only [BlockTriangular, Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Instances.Matrix (goal)
Goal:
m : Type u_4
R : Type u_8
inst : TopologicalSpace R
α : Type u_11
b : m → α
inst_1 : LinearOrder α
inst_2 : Zero R
inst_3 : T2Space R
⊢ IsClosed (X := Matrix m m R) (⋂ (i : m), ⋂ (i_1 : m), ⋂ (_ : b i_1 < b i), {x : Matrix m m R | x i i_1 = 0})
have refine : ∀ (i j : m), b j < b i → IsClosed (X := Matrix m m R) {x : Matrix m m R | x i j = 0}
Tactic: refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
x : ℝ≥0
⊢ Filter.map toReal (𝓝[>] x) = 𝓝[>] (↑x : ℝ)
have rw : 𝓝[toReal '' Set.Ioi x] (↑x : ℝ) = 𝓝[>] (↑x : ℝ)
Tactic: rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
x : ℝ≥0
rw : 𝓝[toReal '' Set.Ioi x] (↑x : ℝ) = 𝓝[>] (↑x : ℝ)
⊢ Filter.map toReal (𝓝[>] x) = 𝓝[>] (↑x : ℝ)
have rw₁ : 𝓝[>] (↑x : ℝ) = 𝓝[>] (↑x : ℝ)
Tactic: rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
x : ℝ≥0
⊢ Filter.map toReal (𝓝[≥] x) = 𝓝[≥] (↑x : ℝ)
have rw : 𝓝[toReal '' Set.Ici x] (↑x : ℝ) = 𝓝[≥] (↑x : ℝ)
Tactic: rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ici]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
x : ℝ≥0
rw : 𝓝[toReal '' Set.Ici x] (↑x : ℝ) = 𝓝[≥] (↑x : ℝ)
⊢ Filter.map toReal (𝓝[≥] x) = 𝓝[≥] (↑x : ℝ)
have rw₁ : 𝓝[≥] (↑x : ℝ) = 𝓝[≥] (↑x : ℝ)
Tactic: rw [isEmbedding_coe.map_nhdsWithin_eq, image_coe_Ici]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
⊢ Filter.map Real.toNNReal atTop = atTop
have rw : Filter.map Real.toNNReal (Filter.map toReal atTop) = atTop
Tactic: rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
rw : Filter.map Real.toNNReal (Filter.map toReal atTop) = atTop
⊢ Filter.map Real.toNNReal atTop = atTop
have rw₁ : Eq (α := Filter ℝ≥0) atTop atTop
Tactic: rw [← map_coe_atTop, Function.LeftInverse.filter_map @Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
⊢ comap Real.toNNReal atTop = atTop
have refine : comap Real.toNNReal atTop ≤ atTop
Tactic: refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
⊢ comap Real.toNNReal atTop ≤ atTop
have refine : ∀ (a : ℝ) (ha : 0 < a), Set.Ioi a ∈ comap Real.toNNReal atTop
Tactic: refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
a : ℝ
ha : 0 < a
⊢ Set.Ioi a ∈ comap Real.toNNReal atTop
have h : ∀ (x : ℝ) (hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal), x ∈ Set.Ioi a
Tactic: filter_upwards [preimage_mem_comap (Ioi_mem_atTop a.toNNReal)] with x hx
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
l : Filter α
f : α → ℝ
⊢ Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop
have rw : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l (comap Real.toNNReal atTop)
Tactic: rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
l : Filter α
f : α → ℝ
rw : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l (comap Real.toNNReal atTop)
⊢ Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop
have rw₁ : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto (Real.toNNReal ∘ f) l atTop
Tactic: rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
l : Filter α
f : α → ℝ
rw : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l (comap Real.toNNReal atTop)
rw₁ : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto (Real.toNNReal ∘ f) l atTop
⊢ Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop
have rw₂ : Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop ↔ Tendsto (β := ℝ≥0) (fun (x : α) ↦ (f x).toNNReal) l atTop
Tactic: rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
⊢ Eq (α := Filter ℝ≥0) (⨅ (l : ℝ≥0), ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l)) (⨅ (a : ℝ≥0), ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a))
have simp : Eq (α := Filter ℝ≥0) (⨅ (l : ℝ≥0), ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l)) (⨅ (a : ℝ≥0), ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a))
Tactic: simp only [bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
have inl : L.NeBot → HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
Tactic: rcases L.neBot_or_eq_bot with _ | hL
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
inl : L.NeBot → HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
have inr : ∀ (hL : L.filter = ⊥), HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
Tactic: rcases L.neBot_or_eq_bot with _ | hL
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
h : L.NeBot
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) y.toNNReal L
have inl : ∀ (y : ℝ≥0) (hy : HasSum f (↑y : ℝ) L), HasSum (fun (x : α) ↦ (f x).toNNReal) (↑y : ℝ).toNNReal L
Tactic: lift y to ℝ≥0 using hy.nonneg hf₀
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
h : L.NeBot
y : ℝ≥0
hy : HasSum f (↑y : ℝ) L
⊢ HasSum (fun (x : α) ↦ (f x).toNNReal) (↑y : ℝ).toNNReal L
have inl : ∀ (f : (i : α) → ℝ≥0) (hy : HasSum (fun (i : α) ↦ (↑(f i) : ℝ)) (↑y : ℝ) L),
  HasSum (fun (x : α) ↦ Real.toNNReal ((fun (i : α) ↦ (↑(f i) : ℝ)) x)) (↑y : ℝ).toNNReal L
Tactic: lift f to α → ℝ≥0 using hf₀
Cleared hypotheses: f, hf₀, hy
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L
have inl : L.NeBot → (Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L)
Tactic: rcases L.neBot_or_eq_bot with _ | hL
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
inl : L.NeBot → (Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L)
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L
have inr : ∀ (hL : L.filter = ⊥), Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L
Tactic: rcases L.neBot_or_eq_bot with _ | hL
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L
have inl : Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L → Summable f L
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h : L.NeBot
inl : Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L → Summable f L
⊢ Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L ↔ Summable f L
have inl₁ : Summable f L → Summable (α := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) L
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)
have rw : ∀ (hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)) {i : β → α} (hi : Function.Injective i),
  Summable (α := ℝ) fun (a : β) ↦ (↑((f ∘ i) a) : ℝ)
Tactic: rw [← summable_coe] at hf ⊢
Cleared hypotheses: hf, i, hi
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable (α := ℝ≥0) fun (i : ℕ) ↦ f (i + k)) ↔ Summable f
have rw : (Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f (a + k)) : ℝ)) ↔ Summable (α := ℝ) fun (a : ℕ) ↦ (↑(f a) : ℝ)
Tactic: rw [← summable_coe, ← summable_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun (n : ℕ) ↦ f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
have rw : HasSum (fun (n : ℕ) ↦ (↑(f n) : ℝ)) ((↑a : ℝ) + ∑ i ∈ Finset.range k, (↑(f i) : ℝ)) ↔
  HasSum f (a + ∑ i ∈ Finset.range k, f i)
Tactic: rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun (n : ℕ) ↦ (↑(f n) : ℝ)) ((↑a : ℝ) + ∑ i ∈ Finset.range k, (↑(f i) : ℝ)) ↔
    HasSum f (a + ∑ i ∈ Finset.range k, f i)
have norm_cast : HasSum f (a + ∑ i ∈ Finset.range k, f i) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
Tactic: norm_cast