harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive]
lemma max_prod_le [LinearOrderedCommMonoid α] {s : Multiset ι} {f g : ι → α} :
    max (s.map f).prod (s.map g).prod ≤ (s.map fun i ↦ max (f i) (g i)).prod

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (List.map f l).prod ⊔ (List.map g l).prod ≤ (List.map (fun i => f i ⊔ g i) l).prod

Tactic:
apply List.max_prod_le

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
⊢ (map f s).prod ⊔ (map g s).prod ≤ (map (fun i => f i ⊔ g i) s).prod

Tactic:
obtain ⟨l⟩ := s

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod ⊔ (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map (fun i => f i ⊔ g i) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Proof state:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (map f (Quot.mk (⇑(List.isSetoid ι)) l)).prod ⊔ (map g (Quot.mk (⇑(List.isSetoid ι)) l)).prod ≤
    (map (fun i => f i ⊔ g i) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]

Result:
case mk
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedCommMonoid α
s : Multiset ι
f g : ι → α
l : List ι
⊢ (List.map f l).prod ⊔ (List.map g l).prod ≤ (List.map (fun i => f i ⊔ g i) l).prod
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_of_le (h : a ≤ b) : [[a, b]] = Icc a b

Proof state:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem embDomain_image : s.embDomain f (f a) = s a

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ (s.embDomain f) (f a) = s a

Tactic:
rw [embDomain_apply, dif_pos (Set.mem_range_self a)]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ s (Classical.choose ⋯) = s a

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_7
β : Type u_8
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ s (Classical.choose ⋯) = s a

Tactic:
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_range_self a)))

Result:
no goals
-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma transGen_oneStep_of_isDershowitzMannaLT :
    IsDershowitzMannaLT M N → TransGen OneStep M N

Proof state:
case intro.intro.intro.intro.intro.intro.cons.inr
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
⊢ TransGen Multiset.OneStep M N

Tactic:
refine .tail (b := X + Y' + Z) (ih (X + Y') (Y - Y') hZ ?_ rfl fun y hy ↦ ?_) <|
  ⟨X + Z, Y', z, add_right_comm .., by simp [hN, add_comm (_ + _)], by simp [Y']⟩

Result:
case intro.intro.intro.intro.intro.intro.cons.inr.refine_1
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
⊢ M = X + Y' + (Y - Y')

case intro.intro.intro.intro.intro.intro.cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z ∈ Z, y < z

Proof state:
case intro.intro.intro.intro.intro.intro.cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ y ∈ Y, ∃ z ∈ Z, y < z) → TransGen Multiset.OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ y ∈ Y, ∃ z_1 ∈ z ::ₘ Z, y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x => x < z) Y
y : α
hy : y ∈ Y ∧ ¬y < z
⊢ ∃ z ∈ Z, y < z

Tactic:
simpa [hy.2] using hYZ y (by aesop)

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem to_inv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
    ApproximatesLinearOn (hf.toPartialEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s)
      (N * (N⁻¹ - c)⁻¹ * c) := fun x hx y hy ↦ by
  set A := hf.toPartialEquiv hc
  have Af : ∀ z, A z = f z := fun z => rfl
  rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩
  rcases (mem_image _ _ _).1 hy with ⟨y', y's, rfl⟩
  rw [← Af x', ← Af y', A.left_inv x's, A.left_inv y's]
  calc
    ‖x' - y' - f'.symm (A x' - A y')‖ ≤ N * ‖f' (x' - y' - f'.symm (A x' - A y'))‖ :=
      (f' : E →L[𝕜] F).bound_of_antilipschitz f'.antilipschitz _
    _ = N * ‖A y' - A x' - f' (y' - x')‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
⊢ ‖↑(hf.toPartialEquiv hc).symm x - ↑(hf.toPartialEquiv hc).symm y - ↑f'.symm (x - y)‖ ≤
    ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖

Tactic:
set A := hf.toPartialEquiv hc

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
x : F
hx : x ∈ f '' s
y : F
hy : y ∈ f '' s
A : PartialEquiv E F := hf.toPartialEquiv hc
⊢ ‖↑A.symm x - ↑A.symm y - ↑f'.symm (x - y)‖ ≤ ↑(‖↑f'.symm‖₊ * (‖↑f'.symm‖₊⁻¹ - c)⁻¹ * c) * ‖x - y‖
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- A Weierstrass curve is nonsingular at every point if its discriminant is non-zero. -/
lemma nonsingular_of_Δ_ne_zero {x y : R} (h : W'.Equation x y) (hΔ : W'.Δ ≠ 0) :
    W'.Nonsingular x y :=
  (nonsingular_iff_variableChange x y).mpr <|
    nonsingular_zero_of_Δ_ne_zero ((equation_iff_variableChange x y).mp h) <| by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
h : W'.Equation x y
hΔ : Δ W' ≠ 0
⊢ Δ (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine ≠ 0

Tactic:
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
    (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).erase a = if a ∈ l₁ then l₁.erase a ++ l₂ else l₁ ++ l₂.erase a

Tactic:
simp [erase_eq_eraseP, eraseP_append]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : C ⥤ Dᵒᵖ` preserves finite coproducts, then `F.leftOp : Cᵒᵖ ⥤ D` preserves finite
    products. -/
lemma preservesFiniteProducts_leftOp (F : C ⥤ Dᵒᵖ) [PreservesFiniteCoproducts F] :
    PreservesFiniteProducts F.leftOp where
  preserves _

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_leftOp

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem rotateRight_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h : x = x') :
    BitVec.rotateRight x' n = BitVec.rotateRight x n

Proof state:
n w : Nat
x x' : BitVec w
h : x = x'
⊢ x'.rotateRight n = x.rotateRight n

Tactic:
simp[*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx_lt_size_of_exists {xs : Array α} (h : ∃ x ∈ xs, p x) :
    xs.findIdx p < xs.size

Proof state:
α : Type u_1
p : α → Bool
xs : List α
h : ∃ x, x ∈ { toList := xs } ∧ p x = true
⊢ ∃ x, x ∈ xs ∧ p x = true

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
h : ∃ x, x ∈ { toList := xs } ∧ p x = true
⊢ findIdx p { toList := xs } < { toList := xs }.size

Tactic:
simpa using List.findIdx_lt_length_of_exists (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
h : ∃ x, x ∈ xs ∧ p x = true
⊢ findIdx p xs < xs.size

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
h : ∃ x, x ∈ { toList := xs } ∧ p x = true
⊢ findIdx p { toList := xs } < { toList := xs }.size
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem norm_equiv_symm_const {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) (b : β) :
    ‖(WithLp.equiv p (ι → β)).symm (Function.const _ b)‖ =
      (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖ :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_equiv_symm_const hp b).trans <| by simp

Proof state:
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝¹ : Fintype ι
β : Type u_5
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
⊢ ↑(↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊) = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
@[simp] lemma toCircle_neg (θ : Angle) : toCircle (-θ) = (toCircle θ)⁻¹

Proof state:
case h
x✝ : ℝ
⊢ (-↑x✝).toCircle = (↑x✝).toCircle⁻¹

Tactic:
simp_rw [← coe_neg, toCircle_coe, Circle.exp_neg]

Result:
no goals

Proof state:
θ : Angle
⊢ (-θ).toCircle = θ.toCircle⁻¹

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (-↑x✝).toCircle = (↑x✝).toCircle⁻¹
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_negPolynomial : (W'.baseChange B).toAffine.negPolynomial =
    (W'.baseChange A).toAffine.negPolynomial.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toAffine.negPolynomial = Polynomial.map (mapRingHom ↑f) (baseChange W' A).toAffine.negPolynomial

Tactic:
rw [← map_negPolynomial, map_baseChange]

Result:
no goals
-- Mathlib/Analysis/Calculus/Rademacher.lean
theorem ae_lineDifferentiableAt
    (hf : LipschitzWith C f) (v : E) :
    ∀ᵐ p ∂μ, LineDifferentiableAt ℝ f p v

Proof state:
case h.e'_11.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
p : E
this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s
h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (fun t => s + t) 0
x✝ : ℝ
⊢ f (p + s • v + x✝ • v) = ((fun t => f (p + t • v)) ∘ HAdd.hAdd s) x✝

Tactic:
simp only [LineDifferentiableAt, add_assoc, Function.comp_apply, add_smul]

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
p : E
this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s
h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (fun t => s + t) 0
⊢ LineDifferentiableAt ℝ f (p + s • v) v

Tactic:
simp only [LineDifferentiableAt]

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
p : E
this✝ : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t => f (p + t • v)) s
s : ℝ
hs : DifferentiableAt ℝ (fun t => f (p + t • v)) s
h's : DifferentiableAt ℝ (fun t => f (p + t • v)) (s + 0)
this : DifferentiableAt ℝ (fun t => s + t) 0
⊢ DifferentiableAt ℝ (fun t => f (p + s • v + t • v)) 0

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
⊢ ∀ᵐ (p : E) ∂μ, LineDifferentiableAt ℝ f p v

Tactic:
suffices A : ∀ p, ∀ᵐ (t : ℝ) ∂volume, LineDifferentiableAt ℝ f (p + t • v) v from
  ae_mem_of_ae_add_linearMap_mem L.toLinearMap volume μ
    (measurableSet_lineDifferentiableAt hf.continuous) A

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
v : E
L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight 1 v
⊢ ∀ (p : E), ∀ᵐ (t : ℝ), LineDifferentiableAt ℝ f (p + t • v) v
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_comp_subset_range [MeasurableSpace β] (f : β →ₛ γ) {g : α → β} (hgm : Measurable g) :
    (f.comp g hgm).range ⊆ f.range :=
  Finset.coe_subset.1 <| by simp only [coe_range, coe_comp, Set.range_comp_subset_range]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β →ₛ γ
g : α → β
hgm : Measurable g
⊢ ↑(f.comp g hgm).range ⊆ ↑f.range

Tactic:
simp only [coe_range, coe_comp, Set.range_comp_subset_range]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_succ_iff_hasFDerivWithinAt (hn : n ≠ ∞) :
    ContDiffOn 𝕜 (n + 1) f s ↔
      ∀ x ∈ s, ∃ u ∈ 𝓝[insert x s] x, (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f' : E → E →L[𝕜] F,
        (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Proof state:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
⊢ ∃ u ∈ 𝓝[insert x s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Tactic:
rw [insert_eq_of_mem hx] at hu ⊢

Result:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
vu : v ∈ 𝓝[insert x u] x
v'u : v ⊆ insert x u
hv : ContDiffOn 𝕜 n f' v
⊢ ∃ u ∈ 𝓝[s] x, (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn 𝕜 n f' u

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hn : n ≠ ∞
h : ContDiffOn 𝕜 (n + 1) f s
x : E
hx : x ∈ s
u : Set E
hu : u ∈ 𝓝[insert x s] x
f_an : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
hf' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
⊢ n = ∞ → n = ω

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrable_mul_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
    Integrable fun x : ℝ => ↑x * cexp (-b * (x : ℂ) ^ 2)

Proof state:
case refine_1
b : ℂ
hb : 0 < b.re
⊢ Continuous fun x => -b * ↑x ^ 2

Tactic:
exact continuous_const.mul (continuous_ofReal.pow 2)

Result:
no goals

Proof state:
case refine_2
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun x => x * rexp (-b.re * x ^ 2)) volume
⊢ HasFiniteIntegral (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume

Tactic:
rw [← hasFiniteIntegral_norm_iff] at this ⊢

Result:
case refine_2
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun a => ‖a * rexp (-b.re * a ^ 2)‖) volume
⊢ HasFiniteIntegral (fun a => ‖↑a * cexp (-b * ↑a ^ 2)‖) volume

Proof state:
b : ℂ
hb : 0 < b.re
⊢ Integrable (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume

Tactic:
refine ⟨(continuous_ofReal.mul (Complex.continuous_exp.comp ?_)).aestronglyMeasurable, ?_⟩

Result:
case refine_1
b : ℂ
hb : 0 < b.re
⊢ Continuous fun x => -b * ↑x ^ 2

case refine_2
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume

Proof state:
case h.e'_5.h
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun a => ‖a * rexp (-b.re * a ^ 2)‖) volume
x✝ : ℝ
⊢ ‖↑x✝ * cexp (-b * ↑x✝ ^ 2)‖ = ‖x✝ * rexp (-b.re * x✝ ^ 2)‖

Tactic:
rw [norm_mul, norm_mul, norm_cexp_neg_mul_sq b, norm_real, norm_of_nonneg (exp_pos _).le]

Result:
no goals

Proof state:
case refine_2
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun a => ‖a * rexp (-b.re * a ^ 2)‖) volume
⊢ HasFiniteIntegral (fun a => ‖↑a * cexp (-b * ↑a ^ 2)‖) volume

Tactic:
convert this

Result:
case h.e'_5.h
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun a => ‖a * rexp (-b.re * a ^ 2)‖) volume
x✝ : ℝ
⊢ ‖↑x✝ * cexp (-b * ↑x✝ ^ 2)‖ = ‖x✝ * rexp (-b.re * x✝ ^ 2)‖

Proof state:
case refine_2
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume

Tactic:
have := (integrable_mul_exp_neg_mul_sq hb).hasFiniteIntegral

Result:
case refine_2
b : ℂ
hb : 0 < b.re
this : HasFiniteIntegral (fun x => x * rexp (-b.re * x ^ 2)) volume
⊢ HasFiniteIntegral (fun x => ↑x * cexp (-b * ↑x ^ 2)) volume
-- Mathlib/RingTheory/IsTensorProduct.lean
lemma Algebra.IsPushout.equiv_symm_algebraMap_right [Algebra.IsPushout R S R' S'] (a : R') :
    (equiv R S R' S').symm (algebraMap R' S' a) = 1 ⊗ₜ a

Proof state:
R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (equiv R S R' S').symm ((algebraMap R' S') a) = 1 ⊗ₜ[R] a

Tactic:
rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, one_mul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lift_natCast : ∀ n : ℕ, lift.{u, v} n = n
  | 0 => by simp
  | n + 1 => by simp [lift_natCast n]

Proof state:
n : ℕ
⊢ lift.{u, v} ↑(n + 1) = ↑(n + 1)

Tactic:
simp [lift_natCast n]

Result:
no goals

Proof state:
⊢ lift.{u, v} ↑0 = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem frontier_equivFun {E : Type*} [AddCommGroup E] [Module ℝ E] {ι : Type*} [Fintype ι]
    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E]
    (b : Basis ι ℝ E) (s : Set E) :
    frontier (b.equivFun '' s) = b.equivFun '' (frontier s)

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T2Space E
b : Basis ι ℝ E
s : Set E
⊢ frontier (⇑b.equivFun.symm ⁻¹' s) = ⇑b.equivFun.symm ⁻¹' frontier s

Tactic:
exact (Homeomorph.preimage_frontier b.equivFunL.toHomeomorph.symm s).symm

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T2Space E
b : Basis ι ℝ E
s : Set E
⊢ frontier (⇑b.equivFun '' s) = ⇑b.equivFun '' frontier s

Tactic:
rw [LinearEquiv.image_eq_preimage, LinearEquiv.image_eq_preimage]

Result:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
ι : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : T2Space E
b : Basis ι ℝ E
s : Set E
⊢ frontier (⇑b.equivFun.symm ⁻¹' s) = ⇑b.equivFun.symm ⁻¹' frontier s
-- Mathlib/NumberTheory/SumPrimeReciprocals.lean
theorem not_summable_one_div_on_primes :
    ¬ Summable (indicator {p | p.Prime} (fun n : ℕ ↦ (1 : ℝ) / n))

Proof state:
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
⊢ False

Tactic:
obtain ⟨k, hk⟩ := h.nat_tsum_vanishing (Iio_mem_nhds one_half_pos : Iio (1 / 2 : ℝ) ∈ 𝓝 0)

Result:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∀ t ⊆ {n | k ≤ n}, ∑' (n : ↑t), {p | Nat.Prime p}.indicator (fun n => 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False

Proof state:
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
⊢ Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n)

Tactic:
convert h.indicator {n : ℕ | k ≤ n} using 1

Result:
case h.e'_5
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n => 1 / ↑n) x < 1 / 2
⊢ (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n => 1 / ↑n) =
    {n | k ≤ n}.indicator ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)

Proof state:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∀ t ⊆ {n | k ≤ n}, ∑' (n : ↑t), {p | Nat.Prime p}.indicator (fun n => 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False

Tactic:
specialize hk ({p | Nat.Prime p} ∩ {p | k ≤ p}) inter_subset_right

Result:
case intro
h : Summable ({p | Nat.Prime p}.indicator fun n => 1 / ↑n)
k : ℕ
hk : ∑' (n : ↑({p | Nat.Prime p} ∩ {p | k ≤ p})), {p | Nat.Prime p}.indicator (fun n => 1 / ↑n) ↑n ∈ Iio (1 / 2)
⊢ False
-- Mathlib/Logic/Nontrivial/Basic.lean
theorem exists_pair_lt (α : Type*) [Nontrivial α] [LinearOrder α] : ∃ x y : α, x < y

Proof state:
case intro.intro
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ x y, x < y

Tactic:
cases lt_or_gt_of_ne hxy <;> exact ⟨_, _, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
⊢ ∃ x y, x < y

Tactic:
rcases exists_pair_ne α with ⟨x, y, hxy⟩

Result:
case intro.intro
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
⊢ ∃ x y, x < y