harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem tendsto_Lp_iff_tendsto_eLpNorm {ι} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → Lp E p μ)
    (f_lim : α → E) (f_lim_ℒp : MemLp f_lim p μ) :
    fi.Tendsto f (𝓝 (f_lim_ℒp.toLp f_lim)) ↔
      fi.Tendsto (fun n => eLpNorm (⇑(f n) - f_lim) p μ) (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ (fun n => eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) = fun n => eLpNorm (↑↑(f n) - f_lim) p μ

Tactic:
exact funext fun n => eLpNorm_congr_ae (EventuallyEq.rfl.sub (MemLp.coeFn_toLp f_lim_ℒp))

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
h_eq : (fun n => eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) = fun n => eLpNorm (↑↑(f n) - f_lim) p μ
⊢ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

Tactic:
rw [h_eq]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

Tactic:
suffices h_eq :
    (fun n => eLpNorm (⇑(f n) - ⇑(MemLp.toLp f_lim f_lim_ℒp)) p μ) =
      (fun n => eLpNorm (⇑(f n) - f_lim) p μ) by
  rw [h_eq]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ (fun n => eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) = fun n => eLpNorm (↑↑(f n) - f_lim) p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto f fi (𝓝 (MemLp.toLp f_lim f_lim_ℒp)) ↔ Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)

Tactic:
rw [tendsto_Lp_iff_tendsto_eLpNorm']

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
ι : Type u_7
fi : Filter ι
inst✝ : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
f_lim : α → E
f_lim_ℒp : MemLp f_lim p μ
⊢ Tendsto (fun n => eLpNorm (↑↑(f n) - ↑↑(MemLp.toLp f_lim f_lim_ℒp)) p μ) fi (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n) - f_lim) p μ) fi (𝓝 0)
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem support_subset_source : support f ⊆ (chartAt H c).source

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ (extChartAt I c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut ⊆ (extChartAt I c).source

Tactic:
exact inter_subset_left

Result:
no goals

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ support ↑f ⊆ (chartAt H c).source

Tactic:
rw [f.support_eq_inter_preimage, ← extChartAt_source I]

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ (extChartAt I c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut ⊆ (extChartAt I c).source
-- Mathlib/Analysis/Normed/Field/Basic.lean
@[simp] lemma enorm_pow (a : α) (n : ℕ) : ‖a ^ n‖ₑ = ‖a‖ₑ ^ n

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
a : α
n : ℕ
⊢ ‖a ^ n‖ₑ = ‖a‖ₑ ^ n

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive] lemma pow_mem_pow (ha : a ∈ s) : a ^ n ∈ s ^ n

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
    (b :: l).findIdx p = bif p b then 0 else (l.findIdx p) + 1

Proof state:
case nil
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
⊢ findIdx.go p [] (n + 1) = findIdx.go p [] n + 1

Tactic:
unfold findIdx.go

Result:
case nil
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
⊢ n + 1 = n + 1

Proof state:
α : Type u_1
p : α → Bool
b : α
l : List α
⊢ findIdx p (b :: l) = bif p b then 0 else findIdx p l + 1

Tactic:
cases H : p b with
| true => simp [H, findIdx, findIdx.go]
| false => simp [H, findIdx, findIdx.go, findIdx_go_succ]

Result:
no goals

Proof state:
case nil
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
⊢ n + 1 = n + 1

Tactic:
exact Nat.succ_eq_add_one n

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
b : α
l : List α
H : p b = false
⊢ findIdx p (b :: l) = bif false then 0 else findIdx p l + 1

Tactic:
simp [H, findIdx, findIdx.go, findIdx_go_succ]

Result:
no goals

Proof state:
case cons
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
head : α
tail : List α
⊢ findIdx.go p (head :: tail) (n + 1) = findIdx.go p (head :: tail) n + 1

Tactic:
unfold findIdx.go

Result:
case cons
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
head : α
tail : List α
⊢ (bif p head then n + 1 else findIdx.go p tail (n + 1 + 1)) = (bif p head then n else findIdx.go p tail (n + 1)) + 1

Proof state:
α : Type u_1
p✝ : α → Bool
b : α
l✝ : List α
p : α → Bool
l : List α
n : Nat
⊢ findIdx.go p l (n + 1) = findIdx.go p l n + 1

Tactic:
cases l with
| nil => unfold findIdx.go; exact Nat.succ_eq_add_one n
| cons head tail =>
  unfold findIdx.go
  cases p head <;> simp only [cond_false, cond_true]
  exact findIdx_go_succ p tail (n + 1)

Result:
no goals

Proof state:
case cons.false
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
head : α
tail : List α
⊢ findIdx.go p tail (n + 1 + 1) = findIdx.go p tail (n + 1) + 1

Tactic:
exact findIdx_go_succ p tail (n + 1)

Result:
no goals

Proof state:
case cons
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
head : α
tail : List α
⊢ (bif p head then n + 1 else findIdx.go p tail (n + 1 + 1)) = (bif p head then n else findIdx.go p tail (n + 1)) + 1

Tactic:
cases p head <;> simp only [cond_false, cond_true]

Result:
case cons.false
α : Type u_1
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : Nat
head : α
tail : List α
⊢ findIdx.go p tail (n + 1 + 1) = findIdx.go p tail (n + 1) + 1

Proof state:
case true
α : Type u_1
p : α → Bool
b : α
l : List α
H : p b = true
⊢ findIdx p (b :: l) = bif true then 0 else findIdx p l + 1

Tactic:
simp [H, findIdx, findIdx.go]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Lemmas.lean
theorem ne_of_lt {a b : String} (h : a < b) : a ≠ b

Proof state:
a b : String
h : a < b
⊢ a ≠ b

Tactic:
have := String.lt_irrefl a

Result:
a b : String
h : a < b
this : ¬a < a
⊢ a ≠ b

Proof state:
a b : String
h✝ : a < b
this : ¬a < a
h : a = b
⊢ False

Tactic:
subst h

Result:
a : String
this : ¬a < a
h : a < a
⊢ False

Proof state:
a : String
this : ¬a < a
h : a < a
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
a b : String
h : a < b
this : ¬a < a
⊢ a ≠ b

Tactic:
intro h

Result:
a b : String
h✝ : a < b
this : ¬a < a
h : a = b
⊢ False
-- Mathlib/Topology/Algebra/LinearTopology.lean
theorem _root_.IsCentralScalar.isLinearTopology_iff [Module Rᵐᵒᵖ M] [IsCentralScalar R M] :
    IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M

Proof state:
case mp
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
H : IsLinearTopology Rᵐᵒᵖ M
⊢ IsLinearTopology R M

Tactic:
exact mk_of_hasBasis' R (IsLinearTopology.hasBasis_submodule Rᵐᵒᵖ)
  fun S r m hm ↦ op_smul_eq_smul r m ▸ S.smul_mem _ hm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M

Tactic:
constructor <;> intro H

Result:
case mp
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
H : IsLinearTopology Rᵐᵒᵖ M
⊢ IsLinearTopology R M

case mpr
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
H : IsLinearTopology R M
⊢ IsLinearTopology Rᵐᵒᵖ M

Proof state:
case mpr
R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
H : IsLinearTopology R M
⊢ IsLinearTopology Rᵐᵒᵖ M

Tactic:
exact mk_of_hasBasis' Rᵐᵒᵖ (IsLinearTopology.hasBasis_submodule R)
  fun S r m hm ↦ unop_smul_eq_smul r m ▸ S.smul_mem _ hm

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma φ_four :
    W.φ 4 = C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 + 1 = 2 * 2 + 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 - 1 = 3

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 4 = C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
rw [φ, ψ_four, show (4 + 1 : ℤ) = 2 * 2 + 1 by rfl, ψ_odd, two_add_two_eq_four, ψ_four,
  show (2 - 1 : ℤ) = 1 by rfl, ψ_two, ψ_one, two_add_one_eq_three, show (4 - 1 : ℤ) = 3 by rfl,
  ψ_three]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 2 - 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
ring1

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@[simp]
lemma asIdeal_toTwoSided (I : Ideal R) (h) : TwoSidedIdeal.asIdeal (I.toTwoSided h) = I

Proof state:
case h
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ∀ {x y : R}, x ∈ I → x * y ∈ I
x✝ : R
⊢ x✝ ∈ TwoSidedIdeal.asIdeal (I.toTwoSided h) ↔ x✝ ∈ I

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ∀ {x y : R}, x ∈ I → x * y ∈ I
⊢ TwoSidedIdeal.asIdeal (I.toTwoSided h) = I

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ∀ {x y : R}, x ∈ I → x * y ∈ I
x✝ : R
⊢ x✝ ∈ TwoSidedIdeal.asIdeal (I.toTwoSided h) ↔ x✝ ∈ I
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem swap_dist : Function.swap (@dist α _) = dist

Proof state:
case h.h
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y

Tactic:
exact dist_comm _ _

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ Function.swap dist = dist

Tactic:
funext x y

Result:
case h.h
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem strictAntiOn_logb : StrictAntiOn (logb b) (Set.Iio 0)

Proof state:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x

Tactic:
rw [← logb_abs y, ← logb_abs x]

Result:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |y| < logb b |x|

Proof state:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b |y| < logb b |x|

Tactic:
refine logb_lt_logb hb (abs_pos.2 hy.ne) ?_

Result:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Proof state:
b : ℝ
hb : 1 < b
⊢ StrictAntiOn (logb b) (Iio 0)

Tactic:
rintro x (hx : x < 0) y (hy : y < 0) hxy

Result:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b y < logb b x

Proof state:
b : ℝ
hb : 1 < b
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Tactic:
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_eq_natAbs_iff {a b : Int} : a.natAbs = b.natAbs ↔ a = b ∨ a = -b

Proof state:
case mpr.inl
b : Int
⊢ b.natAbs = b.natAbs

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.inl
a b : Int
h✝ : a = b
⊢ a.natAbs = b.natAbs

Tactic:
subst a

Result:
case mpr.inl
b : Int
⊢ b.natAbs = b.natAbs

Proof state:
case mp.inr.inr
a b : Int
h : a.natAbs = b.natAbs
h₁ : a = -↑a.natAbs
h₂ : b = -↑b.natAbs
⊢ a = b ∨ a = -b

Tactic:
rw [h₁, h₂]

Result:
case mp.inr.inr
a b : Int
h : a.natAbs = b.natAbs
h₁ : a = -↑a.natAbs
h₂ : b = -↑b.natAbs
⊢ -↑a.natAbs = -↑b.natAbs ∨ -↑a.natAbs = - -↑b.natAbs

Proof state:
case mpr.inl
b : Int
⊢ b.natAbs = b.natAbs

Tactic:
try rfl

Result:
no goals

Proof state:
case mp.inr.inr
a b : Int
h : a.natAbs = b.natAbs
h₁ : a = -↑a.natAbs
h₂ : b = -↑b.natAbs
⊢ -↑a.natAbs = -↑b.natAbs ∨ -↑a.natAbs = - -↑b.natAbs

Tactic:
simp [h]

Result:
no goals

Proof state:
a b : Int
⊢ a.natAbs = b.natAbs ↔ a = b ∨ a = -b

Tactic:
constructor <;> intro h

Result:
case mp
a b : Int
h : a.natAbs = b.natAbs
⊢ a = b ∨ a = -b

case mpr
a b : Int
h : a = b ∨ a = -b
⊢ a.natAbs = b.natAbs

Proof state:
case mpr
a b : Int
h : a = b ∨ a = -b
⊢ a.natAbs = b.natAbs

Tactic:
cases h with (subst a; try rfl)
| inr h => rw [Int.natAbs_neg]

Result:
no goals

Proof state:
case mp.inr
a b : Int
h : a.natAbs = b.natAbs
h₁ : a = -↑a.natAbs
⊢ a = b ∨ a = -b

Tactic:
cases Int.natAbs_eq b with
| inl h₂ | inr h₂ => rw [h₁, h₂]; simp [h]

Result:
no goals

Proof state:
case mpr.inr
b : Int
⊢ (-b).natAbs = b.natAbs

Tactic:
rw [Int.natAbs_neg]

Result:
no goals

Proof state:
case mp
a b : Int
h : a.natAbs = b.natAbs
⊢ a = b ∨ a = -b

Tactic:
cases Int.natAbs_eq a with
| inl h₁ | inr h₁ =>
  cases Int.natAbs_eq b with
  | inl h₂ | inr h₂ => rw [h₁, h₂]; simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem iInf_comap_proj :
    ⨅ i, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi Set.univ p

Proof state:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i, comap (proj i) (p i) = pi Set.univ p

Tactic:
ext x

Result:
case h
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i, comap (proj i) (p i) ↔ x ∈ pi Set.univ p

Proof state:
case h
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i, comap (proj i) (p i) ↔ x ∈ pi Set.univ p

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem specializes_prod {x₁ x₂ : X} {y₁ y₂ : Y} : (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂

Tactic:
simp only [Specializes, nhds_prod_eq, prod_le_prod]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem eq_zero_of_lt {n ν : ℕ} (h : n < ν) : bernsteinPolynomial R n ν = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : n < ν
⊢ bernsteinPolynomial R n ν = 0

Tactic:
simp [bernsteinPolynomial, Nat.choose_eq_zero_of_lt h]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_eq_neg_floor (a b : α) : toIocDiv hp a b = -⌊(a + p - b) / p⌋

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p

Tactic:
rw [← add_lt_add_iff_right p, add_assoc, add_comm b, ← sub_lt_iff_lt_add, add_comm (_ * _), ←
  sub_lt_iff_lt_add]

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b - ↑⌊(a + p - b) / p⌋ * p < p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b = -⌊(a + p - b) / p⌋

Tactic:
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc hp ?_

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p - b - ↑⌊(a + p - b) / p⌋ * p < p

Tactic:
exact Int.sub_floor_div_mul_lt _ hp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)

Tactic:
rw [Set.mem_Ioc, zsmul_eq_mul, Int.cast_neg, neg_mul, sub_neg_eq_add, ← sub_nonneg,
  sub_add_eq_sub_sub]

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p ∧ 0 ≤ a + p - b - ↑⌊(a + p - b) / p⌋ * p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p ∧ 0 ≤ a + p - b - ↑⌊(a + p - b) / p⌋ * p

Tactic:
refine ⟨?_, Int.sub_floor_div_mul_nonneg _ hp⟩

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p
-- Mathlib/Data/ZMod/Basic.lean
theorem val_pow {m n : ℕ} {a : ZMod n} [ilt : Fact (1 < n)] (h : a.val ^ m < n) :
    (a ^ m).val = a.val ^ m

Proof state:
case succ
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
this : a.val ^ m < n
⊢ (a ^ (m + 1)).val = a.val ^ (m + 1)

Tactic:
rw [pow_succ, ZMod.val_mul, ih this, ← pow_succ, Nat.mod_eq_of_lt h]

Result:
no goals

Proof state:
case pos.refl
n : ℕ
ilt : Fact (1 < n)
ih : val 0 ^ 0 < n → (0 ^ 0).val = val 0 ^ 0
h : val 0 ^ (0 + 1) < n
⊢ val 0 ^ 0 < n

Tactic:
simp [ilt.out]

Result:
no goals

Proof state:
case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Tactic:
exact lt_of_le_of_lt
 (Nat.pow_le_pow_of_le_right (by rwa [gt_iff_lt, ZMod.val_pos]) (Nat.le_succ m)) h

Result:
no goals

Proof state:
case zero
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
h : a.val ^ 0 < n
⊢ (a ^ 0).val = a.val ^ 0

Tactic:
simp [ZMod.val_one]

Result:
no goals

Proof state:
case pos
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : m = 0
⊢ val 0 ^ m < n

Tactic:
cases hm

Result:
case pos.refl
n : ℕ
ilt : Fact (1 < n)
ih : val 0 ^ 0 < n → (0 ^ 0).val = val 0 ^ 0
h : val 0 ^ (0 + 1) < n
⊢ val 0 ^ 0 < n

Proof state:
case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n

Tactic:
simp only [val_zero, ne_eq, hm, not_false_eq_true, zero_pow, Nat.zero_lt_of_lt h]

Result:
no goals

Proof state:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
⊢ a.val ^ m < n

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n

case inr
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val ^ m < n

Proof state:
case inl
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
⊢ val 0 ^ m < n

Tactic:
by_cases hm : m = 0

Result:
case pos
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : m = 0
⊢ val 0 ^ m < n

case neg
n : ℕ
ilt : Fact (1 < n)
m : ℕ
ih : val 0 ^ m < n → (0 ^ m).val = val 0 ^ m
h : val 0 ^ (m + 1) < n
hm : ¬m = 0
⊢ val 0 ^ m < n

Proof state:
n : ℕ
a : ZMod n
ilt : Fact (1 < n)
m : ℕ
ih : a.val ^ m < n → (a ^ m).val = a.val ^ m
h : a.val ^ (m + 1) < n
ha : a ≠ 0
⊢ a.val > 0

Tactic:
rwa [gt_iff_lt, ZMod.val_pos]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem eLpNorm_lt_top (f : 𝓢(E, F)) (p : ℝ≥0∞) (μ : Measure E

Proof state:
E : Type u_4
F : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
⊢ eLpNorm (⇑f) p μ < ⊤

Tactic:
rcases eLpNorm_le_seminorm ℝ F p μ with ⟨k, C, hC⟩

Result:
case intro.intro
E : Type u_4
F : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily ℝ E F)) f)
⊢ eLpNorm (⇑f) p μ < ⊤

Proof state:
case intro.intro
E : Type u_4
F : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
f : 𝓢(E, F)
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily ℝ E F)) f)
⊢ eLpNorm (⇑f) p μ < ⊤

Tactic:
exact lt_of_le_of_lt (hC f) (ENNReal.mul_lt_top ENNReal.coe_lt_top ENNReal.ofReal_lt_top)

Result:
no goals