harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.mul' (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :
    HasFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
ha : HasFDerivAt a a' x
hb : HasFDerivAt b b' x
⊢ HasFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x

Tactic:
exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
  (a x, b x)).comp x (ha.prod hb)

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem prod_eq_abs_norm (x : K) :
    ∏ w : InfinitePlace K, w x ^ mult w = abs (Algebra.norm ℚ x)

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ ‖x✝ x‖ = ‖x✝.toRatAlgHom x‖

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, w x ^ w.mult = ∏ x_1 : K →+* ℂ, ‖x_1 x‖

Tactic:
rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]

Result:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, w x ^ w.mult =
    ∏ j : InfinitePlace K, ∏ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, ‖i x‖

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this : ∀ (w : InfinitePlace K), ∀ φ ∈ Finset.filter (fun φ => mk φ = w) Finset.univ, ‖φ x‖ = w x
⊢ ∏ w : InfinitePlace K, w x ^ w.mult =
    ∏ j : InfinitePlace K, ∏ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, ‖i x‖

Tactic:
simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
w : InfinitePlace K
φ : K →+* ℂ
hφ : φ ∈ Finset.filter (fun φ => mk φ = w) Finset.univ
⊢ ‖φ x‖ = w x

Tactic:
rw [← (Finset.mem_filter.mp hφ).2, apply]

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ (fun f => ‖f x‖) x✝ = (fun φ => ‖φ x‖) (RingHom.equivRatAlgHom x✝)

Tactic:
simp [RingHom.equivRatAlgHom_apply]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ ‖x✝ x‖ = ‖x✝.toRatAlgHom x‖

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, w x ^ w.mult = ‖∏ σ : K →ₐ[ℚ] ℂ, σ x‖

Tactic:
rw [norm_prod, ← Fintype.prod_equiv RingHom.equivRatAlgHom (fun f => ‖f x‖)
  (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]; rfl]

Result:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, w x ^ w.mult = ∏ x_1 : K →+* ℂ, ‖x_1 x‖

Proof state:
case h.e'_3
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖

Tactic:
rw [eq_ratCast, Rat.cast_abs, ← Real.norm_eq_abs, ← Complex.norm_real, Complex.ofReal_ratCast]

Result:
no goals

Proof state:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, w x ^ w.mult =
    ∏ j : InfinitePlace K, ∏ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, ‖i x‖

Tactic:
have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
    ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]

Result:
case h.e'_2
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this : ∀ (w : InfinitePlace K), ∀ φ ∈ Finset.filter (fun φ => mk φ = w) Finset.univ, ‖φ x‖ = w x
⊢ ∏ w : InfinitePlace K, w x ^ w.mult =
    ∏ j : InfinitePlace K, ∏ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, ‖i x‖
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem _root_.map_finset_inf [SemilatticeInf β] [OrderTop β]
    [FunLike F α β] [InfTopHomClass F α β]
    (f : F) (s : Finset ι) (g : ι → α) : f (s.inf g) = s.inf (f ∘ g) :=
  Finset.cons_induction_on s (map_top f) fun i s _ h => by
    rw [inf_cons, inf_cons, map_inf, h, Function.comp_apply]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeInf α
inst✝⁴ : OrderTop α
inst✝³ : SemilatticeInf β
inst✝² : OrderTop β
inst✝¹ : FunLike F α β
inst✝ : InfTopHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.inf g) = s.inf (⇑f ∘ g)
⊢ f ((cons i s x✝).inf g) = (cons i s x✝).inf (⇑f ∘ g)

Tactic:
rw [inf_cons, inf_cons, map_inf, h, Function.comp_apply]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem cos_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
exact le_add_of_nonneg_right (mul_self_nonneg _)

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ ≤ ‖x + y‖

Tactic:
rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _),
  norm_add_sq_eq_norm_sq_add_norm_sq_real h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h,
  Real.cos_arccos (le_trans (by norm_num) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
    (div_le_one_of_le₀ _ (norm_nonneg _))]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ ≤ ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ -1 ≤ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
lemma functorMap_commSq_succ (n : ℕ) :
    (Functor.ofOpSequence (functorMap f)).map (homOfLE (by omega : n ≤ n+1)).op ≫ Pi.π _ n ≫
      eqToHom (functorObj_eq_neg (by omega : ¬(n < n))) =
        (Pi.π (fun i ↦ if _ : i < (n + 1) then M i else N i) n) ≫
          eqToHom (functorObj_eq_pos (by omega)) ≫ f n

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{?u.33613, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n : ℕ
⊢ ¬n < n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n : ℕ
⊢ (Functor.ofOpSequence (functorMap f)).map (homOfLE ⋯).op ≫
      Pi.π (fun m => if x : m < Opposite.unop (Opposite.op n) then M m else N m) n ≫ eqToHom ⋯ =
    Pi.π (fun i => if x : i < n + 1 then M i else N i) n ≫ eqToHom ⋯ ≫ f n

Tactic:
simp [functorMap]

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{?u.33613, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n : ℕ
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{?u.33613, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
n : ℕ
⊢ n ≤ n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem imp_eq (p q : Prop) : (p → q) = (¬ p ∨ q)

Proof state:
p q : Prop
⊢ (p → q) = (¬p ∨ q)

Tactic:
by_cases p <;> by_cases q <;> simp [*]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem not_summable_iff_tendsto_nat_atTop {f : ℕ → ℝ≥0} :
    ¬Summable f ↔ Tendsto (fun n : ℕ => ∑ i ∈ Finset.range n, f i) atTop atTop

Proof state:
case mp
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
refine ((tendsto_of_monotone ?_).resolve_right h).comp ?_

Result:
case mp.refine_1
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone fun s => ∑ b ∈ s, f b

case mp.refine_2
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto Finset.range atTop atTop

Proof state:
f : ℕ → ℝ≥0
⊢ ¬Summable f ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
constructor

Result:
case mp
f : ℕ → ℝ≥0
⊢ ¬Summable f → Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop

case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f

Proof state:
case mp
f : ℕ → ℝ≥0
⊢ ¬Summable f → Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop

Tactic:
intro h

Result:
case mp
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop

Proof state:
case mpr
f : ℕ → ℝ≥0
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop → ¬Summable f

Tactic:
rintro hnat ⟨r, hr⟩

Result:
case mpr.intro
f : ℕ → ℝ≥0
hnat : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False

Proof state:
case mpr.intro
f : ℕ → ℝ≥0
hnat : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

Result:
no goals

Proof state:
case mp.refine_1
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Monotone fun s => ∑ b ∈ s, f b

case mp.refine_2
f : ℕ → ℝ≥0
h : ¬Summable f
⊢ Tendsto Finset.range atTop atTop

Tactic:
exacts [Finset.sum_mono_set _, tendsto_finset_range]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem Gamma_mul_Gamma_add_half_of_pos {s : ℝ} (hs : 0 < s) :
    Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π

Proof state:
s : ℝ
hs : 0 < s
⊢ Gamma s * Gamma ((s * 2 + 1) / 2) * (√π * 2 ^ (2 * s - 1)) = Gamma s * Gamma ((s * 2 + 1) / 2) * 2 ^ (2 * s - 1) * √π

Tactic:
ring

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
⊢ 1 - 2 * s = -(2 * s - 1)

Tactic:
abel

Result:
no goals

Proof state:
s : ℝ
hs : 0 < s
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma s * Gamma (s + 1 / 2) * 2 ^ (2 * s - 1) / √π * (2 ^ (2 * s - 1))⁻¹ * √π

Tactic:
field_simp [(sqrt_pos_of_pos pi_pos).ne', (rpow_pos_of_pos two_pos (2 * s - 1)).ne']

Result:
s : ℝ
hs : 0 < s
⊢ Gamma s * Gamma ((s * 2 + 1) / 2) * (√π * 2 ^ (2 * s - 1)) = Gamma s * Gamma ((s * 2 + 1) / 2) * 2 ^ (2 * s - 1) * √π

Proof state:
s : ℝ
hs : 0 < s
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π

Tactic:
rw [← doublingGamma_eq_Gamma (mul_pos two_pos hs), doublingGamma,
  mul_div_cancel_left₀ _ (two_ne_zero' ℝ), (by abel : 1 - 2 * s = -(2 * s - 1)),
  rpow_neg zero_le_two]

Result:
s : ℝ
hs : 0 < s
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma s * Gamma (s + 1 / 2) * 2 ^ (2 * s - 1) / √π * (2 ^ (2 * s - 1))⁻¹ * √π
-- Mathlib/Logic/Basic.lean
lemma eq_cast_iff_heq : a = cast e b ↔ HEq a b := ⟨heq_of_eq_cast _, fun h ↦ by cases h; rfl⟩

Proof state:
α β : Sort u
e : β = α
a : α
b : β
h : HEq a b
⊢ a = cast e b

Tactic:
cases h

Result:
case refl
α : Sort u
a : α
e : α = α
⊢ a = cast e a

Proof state:
case refl
α : Sort u
a : α
e : α = α
⊢ a = cast e a

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Mul.lean
/-- `x^n`, `n : ℕ` is convex on the whole real line whenever `n` is even. -/
protected lemma Even.convexOn_pow {n : ℕ} (hn : Even n) : ConvexOn 𝕜 univ fun x : 𝕜 ↦ x ^ n

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * (x - y) ^ 2 = (1 - b) * x ^ 2 + b * y ^ 2 - ((1 - b) * x + b * y) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * b * (x - y) ^ 2 = a • x ^ 2 + b • y ^ 2 - (a • x + b • y) ^ 2

Tactic:
obtain rfl := eq_sub_of_add_eq hab

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * (x - y) ^ 2 = (1 - b) • x ^ 2 + b • y ^ 2 - ((1 - b) • x + b • y) ^ 2

Proof state:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x => x ^ (n + n)

Tactic:
simp_rw [← two_mul, pow_mul]

Result:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x => (x ^ 2) ^ n

Proof state:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ a • x ^ 2 + b • y ^ 2 - (a • x + b • y) ^ 2

Tactic:
calc
  (0 : 𝕜) ≤ (a * b) * (x - y) ^ 2 := by positivity
  _ = _ := by obtain rfl := eq_sub_of_add_eq hab; simp only [smul_eq_mul]; ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x✝¹ : 𝕜
x✝ : x✝¹ ∈ univ
⊢ 0 ≤ x✝¹ ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x => (x ^ 2) ^ n

Tactic:
refine ConvexOn.pow ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ sub_nonneg.1 ?_⟩
  (fun _ _ ↦ by positivity) _

Result:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ a • x ^ 2 + b • y ^ 2 - (a • x + b • y) ^ 2

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ a * b * (x - y) ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
hn : Even n
⊢ ConvexOn 𝕜 univ fun x => x ^ n

Tactic:
obtain ⟨n, rfl⟩ := hn

Result:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 univ fun x => x ^ (n + n)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * (x - y) ^ 2 = (1 - b) • x ^ 2 + b • y ^ 2 - ((1 - b) • x + b • y) ^ 2

Tactic:
simp only [smul_eq_mul]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedCommRing 𝕜
n : ℕ
x : 𝕜
x✝¹ : x ∈ univ
y : 𝕜
x✝ : y ∈ univ
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * (x - y) ^ 2 = (1 - b) * x ^ 2 + b * y ^ 2 - ((1 - b) * x + b * y) ^ 2
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegral_eq_integral_uIoc (f : ℝ → E) (a b : ℝ) (μ : Measure ℝ) :
    ∫ x in a..b, f x ∂μ = (if a ≤ b then 1 else -1 : ℝ) • ∫ x in Ι a b, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
split_ifs with h

Result:
case pos
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 1 • ∫ (x : ℝ) in Ι a b, f x ∂μ

case neg
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : ¬a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = -1 • ∫ (x : ℝ) in Ι a b, f x ∂μ

Proof state:
case neg
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : ¬a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = -1 • ∫ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
simp only [integral_of_ge (not_le.1 h).le, uIoc_of_ge (not_le.1 h).le, neg_one_smul]

Result:
no goals

Proof state:
case pos
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 1 • ∫ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
simp only [integral_of_le h, uIoc_of_le h, one_smul]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Ioo_map_sectL : (Ioo a b).map (.sectL _ c) = Ioo (a, c) (b, c)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioo a b) = Ioo (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem IsSuffix.getElem {x y : List α} (h : x <:+ y) {n} (hn : n < x.length) :
    x[n] = y[y.length - x.length + n]'(by have := h.length_le; omega)

Proof state:
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
⊢ y[y.length - 1 - (x.length - 1 - n)] = y[y.length - x.length + n]

Tactic:
congr

Result:
case e_i
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
⊢ y.length - 1 - (x.length - 1 - n) = y.length - x.length + n

Proof state:
case e_i
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
⊢ y.length - 1 - (x.length - 1 - n) = y.length - x.length + n

Tactic:
have := h.length_le

Result:
case e_i
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
this : x.length ≤ y.length
⊢ y.length - 1 - (x.length - 1 - n) = y.length - x.length + n

Proof state:
case e_i
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
this : x.length ≤ y.length
⊢ y.length - 1 - (x.length - 1 - n) = y.length - x.length + n

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.7
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
this : x.length ≤ y.length
⊢ y.length - x.length + n < y.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.7
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
⊢ y.length - x.length + n < y.length

Tactic:
have := h.length_le

Result:
α : Type ?u.7
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
this : x.length ≤ y.length
⊢ y.length - x.length + n < y.length

Proof state:
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
⊢ x[n] = y[y.length - x.length + n]

Tactic:
rw [getElem_eq_getElem_reverse, h.reverse.getElem, getElem_reverse]

Result:
α : Type u_1
x y : List α
h : x <:+ y
n : Nat
hn : n < x.length
⊢ y[y.length - 1 - (x.length - 1 - n)] = y[y.length - x.length + n]
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
lemma SpectrumRestricts.eq_zero_of_neg {a : A} (ha : IsSelfAdjoint a)
    (ha₁ : SpectrumRestricts a ContinuousMap.realToNNReal)
    (ha₂ : SpectrumRestricts (-a) ContinuousMap.realToNNReal) :
    a = 0

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
a✝ : Nontrivial A
⊢ spectrum ℝ a ⊆ {0}

Tactic:
rw [Set.subset_singleton_iff]

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
a✝ : Nontrivial A
⊢ ∀ y ∈ spectrum ℝ a, y = 0

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
a✝ : Nontrivial A
⊢ a = 0

Tactic:
apply CFC.eq_zero_of_spectrum_subset_zero (R := ℝ) a

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
a✝ : Nontrivial A
⊢ spectrum ℝ a ⊆ {0}

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal
a✝ : Nontrivial A
⊢ a = 0

Tactic:
rw [SpectrumRestricts.nnreal_iff] at ha₁ ha₂

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
a✝ : Nontrivial A
⊢ a = 0

Proof state:
case h.h
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
ha₂ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
x : ℝ
hx : x ∈ spectrum ℝ a
this : 0 ≤ x
⊢ x = 0

Tactic:
linarith [ha₂ (-x) ((neg_neg x).symm ▸ hx)]

Result:
no goals

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
ha₂ : ∀ x ∈ spectrum ℝ (-a), 0 ≤ x
a✝ : Nontrivial A
⊢ ∀ y ∈ spectrum ℝ a, y = 0

Tactic:
simp only [← spectrum.neg_eq, Set.mem_neg] at ha₂

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
ha₂ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
⊢ ∀ y ∈ spectrum ℝ a, y = 0

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
ha₂ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
⊢ ∀ y ∈ spectrum ℝ a, y = 0

Tactic:
peel ha₁ with x hx _

Result:
case h.h
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : ∀ x ∈ spectrum ℝ a, 0 ≤ x
a✝ : Nontrivial A
ha₂ : ∀ (x : ℝ), -x ∈ spectrum ℝ a → 0 ≤ x
x : ℝ
hx : x ∈ spectrum ℝ a
this : 0 ≤ x
⊢ x = 0

Proof state:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal
⊢ a = 0

Tactic:
nontriviality A

Result:
A : Type u_2
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal
a✝ : Nontrivial A
⊢ a = 0
-- Mathlib/Data/ENNReal/Inv.lean
theorem coe_zpow (hr : r ≠ 0) (n : ℤ) : (↑(r ^ n) : ℝ≥0∞) = (r : ℝ≥0∞) ^ n

Proof state:
case ofNat
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n

Tactic:
simp only [Int.ofNat_eq_coe, coe_pow, zpow_natCast]

Result:
no goals

Proof state:
case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ n.succ ≠ 0
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
simp only [zpow_negSucc, coe_inv this, coe_pow]

Result:
no goals

Proof state:
case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Tactic:
have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr

Result:
case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
this : r ^ n.succ ≠ 0
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n

Proof state:
r : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
rcases n with n | n

Result:
case ofNat
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n

case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
-- Mathlib/Topology/Connected/Clopen.lean
lemma Topology.IsQuotientMap.image_connectedComponent {f : α → β} (hf : IsQuotientMap f)
    (h_fibers : ∀ y : β, IsConnected (f ⁻¹' {y})) (a : α) :
    f '' connectedComponent a = connectedComponent (f a)

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsQuotientMap f
h_fibers : ∀ (y : β), IsConnected (f ⁻¹' {y})
a : α
⊢ f '' connectedComponent a = connectedComponent (f a)

Tactic:
rw [← hf.preimage_connectedComponent h_fibers, image_preimage_eq _ hf.surjective]

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem SupIndep.sup [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α}
    (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) :
    (s.sup g).SupIndep f

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i => (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.sup g).SupIndep f

Tactic:
simp_rw [supIndep_iff_pairwiseDisjoint] at hs hg ⊢

Result:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint fun i => (g i).sup f
hg : ∀ i' ∈ s, (↑(g i')).PairwiseDisjoint f
⊢ (↑(s.sup g)).PairwiseDisjoint f

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint fun i => (g i).sup f
hg : ∀ i' ∈ s, (↑(g i')).PairwiseDisjoint f
⊢ (⋃ x ∈ ↑s, ↑(g x)).PairwiseDisjoint f

Tactic:
exact hs.biUnion_finset hg

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint fun i => (g i).sup f
hg : ∀ i' ∈ s, (↑(g i')).PairwiseDisjoint f
⊢ (↑(s.sup g)).PairwiseDisjoint f

Tactic:
rw [sup_eq_biUnion, coe_biUnion]

Result:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : (↑s).PairwiseDisjoint fun i => (g i).sup f
hg : ∀ i' ∈ s, (↑(g i')).PairwiseDisjoint f
⊢ (⋃ x ∈ ↑s, ↑(g x)).PairwiseDisjoint f