harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Seminorm.lean
theorem ball_smul_closedBall (p : Seminorm 𝕜 E) (r₁ : ℝ) {r₂ : ℝ} (hr₂ : r₂ ≠ 0) :
    Metric.ball (0 : 𝕜) r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ ¬r₂ < 0

Tactic:
exact ((apply_nonneg p b).trans hb).not_lt

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b < r₁ * r₂

Tactic:
intro a ha b hb

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ ‖a‖ * p b < r₁ * r₂

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ p b * ‖a‖ < r₂ * r₁

Tactic:
refine mul_lt_mul' hb ha (norm_nonneg _) (hr₂.lt_or_lt.resolve_left ?_)

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ ¬r₂ < 0

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ ‖a‖ * p b < r₁ * r₂

Tactic:
rw [mul_comm, mul_comm r₁]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
a : 𝕜
ha : ‖a‖ < r₁
b : E
hb : p b ≤ r₂
⊢ p b * ‖a‖ < r₂ * r₁

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)

Tactic:
simp only [smul_subset_iff, mem_ball_zero, mem_closedBall_zero, mem_ball_zero_iff,
  map_smul_eq_mul]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
hr₂ : r₂ ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b < r₁ * r₂
-- Mathlib/Analysis/MeanInequalities.lean
theorem Lp_add_le (hp : 1 ≤ p) :
    (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤
      (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ x ∈ s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) + (∑ x ∈ s, |g x| ^ p) ^ (1 / p)
⊢ (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Tactic:
refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this <;>
  simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add,
    rpow_le_rpow]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  ↑((∑ i ∈ s, ((fun i => ⟨|f i|, ⋯⟩) i + (fun i => ⟨|g i|, ⋯⟩) i) ^ p) ^ (1 / p)) ≤
    ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p) ^ (1 / p) + (∑ i ∈ s, (fun i => ⟨|g i|, ⋯⟩) i ^ p) ^ (1 / p))
⊢ (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Tactic:
push_cast at this

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this : (∑ x ∈ s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) + (∑ x ∈ s, |g x| ^ p) ^ (1 / p)
⊢ (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
⊢ (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)

Tactic:
have :=
  NNReal.coe_le_coe.2
    (NNReal.Lp_add_le s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) hp)

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  ↑((∑ i ∈ s, ((fun i => ⟨|f i|, ⋯⟩) i + (fun i => ⟨|g i|, ⋯⟩) i) ^ p) ^ (1 / p)) ≤
    ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p) ^ (1 / p) + (∑ i ∈ s, (fun i => ⟨|g i|, ⋯⟩) i ^ p) ^ (1 / p))
⊢ (∑ i ∈ s, |f i + g i| ^ p) ^ (1 / p) ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) + (∑ i ∈ s, |g i| ^ p) ^ (1 / p)
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp] lemma enorm_lt_top : ‖x‖ₑ < ∞

Proof state:
E : Type u_8
inst✝ : NNNorm E
x : E
⊢ ‖x‖ₑ < ⊤

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem HasFPowerSeriesOnBall.analyticAt_of_mem (hf : HasFPowerSeriesOnBall f p x r)
    (h : y ∈ EMetric.ball x r) : AnalyticAt 𝕜 f y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ EMetric.ball x r
⊢ AnalyticWithinAt 𝕜 f univ y

Tactic:
exact hf.analyticWithinAt_of_mem (by simpa using h)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ EMetric.ball x r
⊢ y ∈ insert x univ ∩ EMetric.ball x r

Tactic:
simpa using h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : y ∈ EMetric.ball x r
⊢ AnalyticAt 𝕜 f y

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ EMetric.ball x r
⊢ AnalyticAt 𝕜 f y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ EMetric.ball x r
⊢ AnalyticAt 𝕜 f y

Tactic:
rw [← analyticWithinAt_univ]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ EMetric.ball x r
⊢ AnalyticWithinAt 𝕜 f univ y
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Submartingale.stoppedValue_leastGE_eLpNorm_le' [IsFiniteMeasure μ]
    (hf : Submartingale f ℱ μ) (hr : 0 ≤ r) (hf0 : f 0 = 0)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) (i : ℕ) :
    eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤
      ENNReal.toNNReal (2 * μ Set.univ * ENNReal.ofReal (r + R))

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ eLpNorm (stoppedValue f (leastGE f r i)) 1 μ ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal

Tactic:
refine (hf.stoppedValue_leastGE_eLpNorm_le hr hf0 hbdd i).trans ?_

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R) ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
r : ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hr : 0 ≤ r
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
i : ℕ
⊢ 2 * μ Set.univ * ENNReal.ofReal (r + ↑R) ≤ ↑(2 * μ Set.univ * ENNReal.ofReal (r + ↑R)).toNNReal

Tactic:
simp [ENNReal.coe_toNNReal (measure_ne_top μ _), ENNReal.coe_toNNReal]

Result:
no goals
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsPreconnected.eq_univ_of_unbounded {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s)
    (ha : ¬BddAbove s) : s = univ

Proof state:
case intro.intro.intro.intro
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
z : α
zs : z ∈ s
hz : x < z
⊢ x ∈ s

Tactic:
exact hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩

Result:
no goals

Proof state:
case intro.intro
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
⊢ x ∈ s

Tactic:
obtain ⟨z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x

Result:
case intro.intro.intro.intro
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
z : α
zs : z ∈ s
hz : x < z
⊢ x ∈ s

Proof state:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
⊢ x ∈ s

Tactic:
obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, y < x := not_bddBelow_iff.1 hb x

Result:
case intro.intro
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x y : α
ys : y ∈ s
hy : y < x
⊢ x ∈ s

Proof state:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s = univ

Tactic:
refine eq_univ_of_forall fun x => ?_

Result:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
x : α
⊢ x ∈ s
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_length_eq_nilpotencyClass :
    Nat.find (nilpotent_iff_lowerCentralSeries.mp hG) = Group.nilpotencyClass (G := G)

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rintro n h

Result:
case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n = ⊥

Tactic:
rw [← le_bot_iff, ← hn]

Result:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n ≤ H n

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → lowerCentralSeries G n = ⊥

Tactic:
rintro n ⟨H, ⟨hH, hn⟩⟩

Result:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
rw [← least_descending_central_series_length_eq_nilpotencyClass]

Result:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)

Result:
case refine_1
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → lowerCentralSeries G n = ⊥

case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
exact ⟨lowerCentralSeries G, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n ≤ H n

Tactic:
exact descending_central_series_ge_lower H hH n

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)}
    (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : Raw.WFImp (Const.alter m a f).1

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ Raw.WFImp (alterₘ m a f).val

Tactic:
exact wfImp_alterₘ h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ Raw.WFImp (alter m a f).val

Tactic:
rw [Const.alter_eq_alterₘ]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ Raw.WFImp (alterₘ m a f).val
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma mod_two_not_eq_zero : ¬n % 2 = 0 ↔ n % 2 = 1

Proof state:
n : ℕ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1

Tactic:
cases mod_two_eq_zero_or_one n <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem constantCoeff_wittZSMul (z : ℤ) (n : ℕ) : constantCoeff (wittZSMul p z n) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ constantCoeff (wittZSMul p z n) = 0

Tactic:
apply constantCoeff_wittStructureInt p _ _ n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ constantCoeff (z • X 0) = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
n : ℕ
⊢ constantCoeff (z • X 0) = 0

Tactic:
simp only [smul_zero, map_zsmul, constantCoeff_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_perm_eraseKey_of_containsₘ_eq_false [BEq α] [Hashable α] [EquivBEq α]
    [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.1) (h' : m.containsₘ a = false) :
    Perm (toListModel m.1.buckets) (eraseKey a (toListModel m.1.buckets))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = false
⊢ containsKey a (toListModel m.val.buckets) = false

Tactic:
rw [← containsₘ_eq_containsKey h, h']

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = false
⊢ toListModel m.val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
rw [eraseKey_of_containsKey_eq_false]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
h' : m.containsₘ a = false
⊢ containsKey a (toListModel m.val.buckets) = false
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
    (h : stop = l.toArray.size) :
    l.toArray.anyM p 0 stop = l.anyM p

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
⊢ anyM p l.toArray = List.anyM p l

Tactic:
rw [← anyM_toList]

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
stop : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
h : stop = l.toArray.size
⊢ anyM p l.toArray 0 stop = List.anyM p l

Tactic:
subst h

Result:
m : Type → Type u_1
α : Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
l : List α
⊢ anyM p l.toArray = List.anyM p l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    (l : Vector α n) (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' l init (fun a m b => pure (.yield (f a m b))) =
      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
f : (a : α) → a ∈ l → β → β
init : β
⊢ (forIn' l init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init l.attach)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → β
⊢ (forIn' { toArray := l, size_toArray := ⋯ } init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init { toArray := l, size_toArray := ⋯ }.attach)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → β
⊢ (forIn' { toArray := l, size_toArray := ⋯ } init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init { toArray := l, size_toArray := ⋯ }.attach)

Tactic:
simp [Array.forIn'_pure_yield_eq_foldl, Array.foldl_map]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem ENat.measurable_iff {α : Type*} [MeasurableSpace α] {f : α → ℕ∞} :
    Measurable f ↔ ∀ n : ℕ, MeasurableSet (f ⁻¹' {↑n})

Proof state:
case coe
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
n : ℕ
⊢ MeasurableSet (f ⁻¹' {↑n})

Tactic:
exact h n

Result:
no goals

Proof state:
case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (⋃ i, f ⁻¹' {some i})ᶜ

Tactic:
exact .compl <| .iUnion h

Result:
no goals

Proof state:
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
⊢ Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})

Tactic:
refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩

Result:
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
n : ℕ∞
⊢ MeasurableSet (f ⁻¹' {n})

Proof state:
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
n : ℕ∞
⊢ MeasurableSet (f ⁻¹' {n})

Tactic:
cases n with
| top =>
  rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
    preimage_iUnion]
  exact .compl <| .iUnion h
| coe n => exact h n

Result:
no goals

Proof state:
case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (f ⁻¹' {⊤})

Tactic:
rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
  preimage_iUnion]

Result:
case top
α : Type u_6
inst✝ : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {↑n})
⊢ MeasurableSet (⋃ i, f ⁻¹' {some i})ᶜ
-- Mathlib/Tactic/Ring/Basic.lean
theorem neg_zero {R} [Ring R] : -(0 : R) = 0

Proof state:
R : Type u_2
inst✝ : Ring R
⊢ -0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_add (m n : ℕ) : fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)

Proof state:
m n : ℕ
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)

Tactic:
induction' n with n ih generalizing m

Result:
case zero
m : ℕ
⊢ fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (0 + 1)

case succ
n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Proof state:
case succ
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Tactic:
simp only [fib_add_two, succ_eq_add_one, ih]

Result:
case succ
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (n + 1) + fib (m + 1) * (fib n + fib (n + 1))

Proof state:
case zero
m : ℕ
⊢ fib (m + 0 + 1) = fib m * fib 0 + fib (m + 1) * fib (0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
case succ
n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Tactic:
rw [add_assoc m 1 n, add_comm 1 n] at ih

Result:
case succ
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Proof state:
case succ
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (n + 1) + fib (m + 1) * (fib n + fib (n + 1))

Tactic:
ring

Result:
no goals

Proof state:
case succ
n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Tactic:
specialize ih (m + 1)

Result:
case succ
n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_lo_2 (u w v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v

Proof state:
u w v k₁ k₂ : Nat
⊢ isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v

Tactic:
simp [isLt]

Result:
u w v k₁ k₂ : Nat
⊢ k₁ < k₂ → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v

Proof state:
u w v k₁ k₂ : Nat
⊢ k₁ < k₂ → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem lift_rank_add_lift_rank_le_rank_prod [Nontrivial R] :
    lift.{v'} (Module.rank R M) + lift.{v} (Module.rank R M') ≤ Module.rank R (M × M')

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')

Tactic:
exact (rank_add_rank_le_rank_prod R _).trans_eq
  (ULift.moduleEquiv.prod ULift.moduleEquiv).rank_eq

Result:
no goals

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ lift.{v', v} (Module.rank R M) + lift.{v, v'} (Module.rank R M') ≤ Module.rank R (M × M')

Tactic:
rw [← rank_ulift, ← rank_ulift]

Result:
R : Type u
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Nontrivial R
⊢ Module.rank R (ULift.{v', v} M) + Module.rank R (ULift.{v, v'} M') ≤ Module.rank R (M × M')