harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Norm.lean
theorem isCauSeq_im (f : CauSeq ℂ (‖·‖)) : IsCauSeq abs fun n ↦ (f n).im := fun ε ε0 ↦
  (f.cauchy ε0).imp fun i H j ij ↦ by
    simpa only [← ofReal_sub, norm_real, sub_re] using (abs_im_le_norm _).trans_lt <| H _ ij

Proof state:
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ |(fun n => (↑f n).im) j - (fun n => (↑f n).im) i| < ε

Tactic:
simpa only [← ofReal_sub, norm_real, sub_re] using (abs_im_le_norm _).trans_lt <| H _ ij

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_mono {m₁ m₂ : ℝ≥0∞ → ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂) :
    (mkMetric m₁ : Measure X) ≤ mkMetric m₂

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m₁ m₂ : ℝ≥0∞ → ℝ≥0∞
hle : m₁ ≤ᶠ[𝓝[≥] 0] m₂
⊢ mkMetric m₁ ≤ mkMetric m₂

Tactic:
convert @mkMetric_mono_smul X _ _ _ _ m₂ _ ENNReal.one_ne_top one_ne_zero _ <;> simp [*]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem mem_iInf {ι : Sort*} {S : ι → L.Substructure M} {x : M} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
theorem map_add_add (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (x x' : E) (y y' : Fₗ) :
    f (x + x') (y + y') = f x y + f.deriv₂ (x, y) (x', y') + f x' y'

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup Fₗ
inst✝⁴ : SeminormedAddCommGroup Gₗ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
⊢ (f x) y + ((f x') y + ((f x) y' + (f x') y')) = (f x) y + ((f x) y' + ((f x') y + (f x') y'))

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup Fₗ
inst✝⁴ : SeminormedAddCommGroup Gₗ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
⊢ (f (x + x')) (y + y') = (f x) y + (f.deriv₂ (x, y)) (x', y') + (f x') y'

Tactic:
simp only [map_add, add_apply, coe_deriv₂, add_assoc]

Result:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup Fₗ
inst✝⁴ : SeminormedAddCommGroup Gₗ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
f : E →L[𝕜] Fₗ →L[𝕜] Gₗ
x x' : E
y y' : Fₗ
⊢ (f x) y + ((f x') y + ((f x) y' + (f x') y')) = (f x) y + ((f x) y' + ((f x') y + (f x') y'))
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x

Proof state:
p : Prop
inst✝ : Decidable p
x : Prop
y : ¬p → Prop
⊢ ((if h : p then x else y h) ↔ x) ↔ ∀ (h : ¬p), y h ↔ x

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma succ_div_of_dvd (hba : b ∣ a + 1) : (a + 1) / b = a / b + 1

Proof state:
a b : ℕ
hba : b ∣ a + 1
⊢ (a + 1) / b = a / b + 1

Tactic:
rw [succ_div, if_pos hba]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {l : Array α} {a₁ a₂} :
     l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)

Proof state:
α : Type u_1
op : α → α → α
ha : Std.Associative op
l : Array α
a₁ a₂ : α
⊢ foldl op (op a₁ a₂) l = op a₁ (foldl op a₂ l)

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : List α
⊢ foldl op (op a₁ a₂) { toList := l } = op a₁ (foldl op a₂ { toList := l })

Proof state:
case mk
α : Type u_1
op : α → α → α
ha : Std.Associative op
a₁ a₂ : α
l : List α
⊢ foldl op (op a₁ a₂) { toList := l } = op a₁ (foldl op a₂ { toList := l })

Tactic:
simp [List.foldl_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_reverse (l : Array α) : countP p l.reverse = countP p l

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ countP p { toList := toList✝ }.reverse = countP p { toList := toList✝ }

Tactic:
simp [List.countP_reverse]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p l.reverse = countP p l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ countP p { toList := toList✝ }.reverse = countP p { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_mod_gcd_left (xs ys : IntList) : dot xs ys % xs.gcd = 0

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), dot xs ys % ↑(gcd xs) = 0
y : Int
ys : List Int
⊢ dot (x :: xs) (y :: ys) % ↑(gcd (x :: xs)) = 0

Tactic:
rw [dot_cons₂, Int.add_emod,
  ← Int.emod_emod_of_dvd (x * y) (gcd_cons_div_left),
  ← Int.emod_emod_of_dvd (dot xs ys) (Int.ofNat_dvd.mpr gcd_cons_div_right)]

Result:
case cons.cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), dot xs ys % ↑(gcd xs) = 0
y : Int
ys : List Int
⊢ (x * y % x % ↑(gcd (x :: xs)) + dot xs ys % ↑(gcd xs) % ↑(gcd (x :: xs))) % ↑(gcd (x :: xs)) = 0

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), dot xs ys % ↑(gcd xs) = 0
y : Int
ys : List Int
⊢ (x * y % x % ↑(gcd (x :: xs)) + dot xs ys % ↑(gcd xs) % ↑(gcd (x :: xs))) % ↑(gcd (x :: xs)) = 0

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), dot xs ys % ↑(gcd xs) = 0
ys : IntList
⊢ dot (x :: xs) ys % ↑(gcd (x :: xs)) = 0

Tactic:
cases ys with
| nil => simp
| cons y ys =>
  rw [dot_cons₂, Int.add_emod,
    ← Int.emod_emod_of_dvd (x * y) (gcd_cons_div_left),
    ← Int.emod_emod_of_dvd (dot xs ys) (Int.ofNat_dvd.mpr gcd_cons_div_right)]
  simp_all

Result:
no goals

Proof state:
case cons.nil
x : Int
xs : List Int
ih : ∀ (ys : IntList), dot xs ys % ↑(gcd xs) = 0
⊢ dot (x :: xs) [] % ↑(gcd (x :: xs)) = 0

Tactic:
simp

Result:
no goals

Proof state:
case nil
ys : IntList
⊢ dot [] ys % ↑(gcd []) = 0

Tactic:
simp

Result:
no goals

Proof state:
xs ys : IntList
⊢ xs.dot ys % ↑xs.gcd = 0

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys =>
    rw [dot_cons₂, Int.add_emod,
      ← Int.emod_emod_of_dvd (x * y) (gcd_cons_div_left),
      ← Int.emod_emod_of_dvd (dot xs ys) (Int.ofNat_dvd.mpr gcd_cons_div_right)]
    simp_all

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem pow_smul_mod_minimalPeriod (n : ℕ) :
    a ^ (n % minimalPeriod (a • ·) b) • b = a ^ n • b

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ (n % minimalPeriod (fun x => a • x) b) • b = a ^ n • b

Tactic:
rw [← period_eq_minimalPeriod, pow_mod_period_smul]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem iff_comap_eq :
    MeasurableEmbedding f ↔
      Injective f ∧ MeasurableSpace.comap f ‹_› = ‹_› ∧ MeasurableSet (range f) :=
  ⟨fun hf ↦ ⟨hf.injective, hf.comap_eq, hf.measurableSet_range⟩, fun hf ↦
    { injective := hf.1
      measurable

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

Tactic:
rintro _ ⟨s, hs, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f '' (f ⁻¹' s))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ Measurable f

Tactic:
exact comap_measurable f

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (f '' (f ⁻¹' s))

Tactic:
simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toSignedMeasure_smul (r : ℝ≥0) : (r • j).toSignedMeasure = r • j.toSignedMeasure

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (r • j).toSignedMeasure = r • j.toSignedMeasure

Tactic:
ext1 i hi

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(r • j).toSignedMeasure i = ↑(r • j.toSignedMeasure) i

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(r • j).toSignedMeasure i = ↑(r • j.toSignedMeasure) i

Tactic:
rw [VectorMeasure.smul_apply, toSignedMeasure, toSignedMeasure,
  toSignedMeasure_sub_apply hi, toSignedMeasure_sub_apply hi, smul_sub, smul_posPart,
  smul_negPart, ← ENNReal.toReal_smul, ← ENNReal.toReal_smul, Measure.smul_apply,
  Measure.smul_apply]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_pair {f : β → α} {a b : β} : ⨆ x ∈ ({a, b} : Set β), f x = f a ⊔ f b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ ⨆ x ∈ {a, b}, f x = f a ⊔ f b

Tactic:
rw [iSup_insert, iSup_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_set (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
    a ∈ as.set i a

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ ∃ i_1 h_1, (as.set i a h)[i_1] = a

Tactic:
exact ⟨i, (by simpa using h), by simp⟩

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ i < as.size

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ (as.set i a h)[i] = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ a ∈ as.set i a h

Tactic:
simp [mem_iff_getElem]

Result:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ ∃ i_1 h_1, (as.set i a h)[i_1] = a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.abs_eq (x : BitVec w) : x.abs = bif x.getLsbD (w - 1) then -x else x

Proof state:
w : Nat
x : BitVec w
⊢ x.abs = bif x.getLsbD (w - 1) then -x else x

Tactic:
simp [_root_.BitVec.abs_eq, BitVec.msb_eq_getLsbD_last]

Result:
no goals
-- Mathlib/Topology/Separation/SeparatedNhds.lean
theorem Set.hasSeparatingCover_empty_right (s : Set X) : HasSeparatingCover s ∅ :=
  ⟨fun _ ↦ univ, (subset_univ s).trans univ.iUnion_const.symm.subset,
   fun _ ↦ ⟨isOpen_univ, by apply disjoint_empty⟩⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure ((fun x => univ) x✝)) ∅

Tactic:
apply disjoint_empty

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
protected lemma norm_zero : ‖(0 : E)‖ = 0

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
⊢ ‖0‖ = 0

Tactic:
simp [norm_eq_sqrt_norm_inner_self]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
@[simp]
lemma algebraMap_galRestrictHom_apply (σ : L →ₐ[K] L) (x : B) :
    algebraMap B L (galRestrictHom A K L B σ x) = σ (algebraMap B L x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
σ : L →ₐ[K] L
x : B
⊢ (algebraMap B L) (((galRestrictHom A K L B) σ) x) = σ ((algebraMap B L) x)

Tactic:
simp [galRestrictHom, Subalgebra.algebraMap_eq, AlgHom.restrictDomain]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem dvd_gcd_iff {a : α} : a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Tactic:
simp only [Multiset.mem_map, and_imp, exists_imp]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b

Tactic:
apply Iff.trans Multiset.dvd_gcd

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ (b : α), ∀ x ∈ s.val, f x = b → a ∣ b) ↔ ∀ b ∈ s, a ∣ f b

Tactic:
exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem mapOfLE_comp_valuation (R S : ValuationSubring K) (h : R ≤ S) :
    R.mapOfLE S h ∘ R.valuation = S.valuation

Proof state:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ ⇑(R.mapOfLE S h) ∘ ⇑R.valuation = ⇑S.valuation

Tactic:
ext

Result:
case h
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x✝ : K
⊢ (⇑(R.mapOfLE S h) ∘ ⇑R.valuation) x✝ = S.valuation x✝

Proof state:
case h
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
x✝ : K
⊢ (⇑(R.mapOfLE S h) ∘ ⇑R.valuation) x✝ = S.valuation x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem drop_left' {l₁ l₂ : List α} {n} (h : length l₁ = n) : drop n (l₁ ++ l₂) = l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : l₁.length = n
⊢ drop n (l₁ ++ l₂) = l₂

Tactic:
rw [← h]

Result:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : l₁.length = n
⊢ drop l₁.length (l₁ ++ l₂) = l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
n : Nat
h : l₁.length = n
⊢ drop l₁.length (l₁ ++ l₂) = l₂

Tactic:
apply drop_left

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_succ_le : (∫ x in (0)..π, sin x ^ (n + 1)) ≤ ∫ x in (0)..π, sin x ^ n

Proof state:
n : ℕ
H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n

Tactic:
refine integral_mono_on pi_pos.le ?_ ?_ H <;> exact (continuous_sin.pow _).intervalIntegrable 0 π

Result:
no goals

Proof state:
n : ℕ
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n

Tactic:
let H x h := pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (n.le_add_right 1)

Result:
n : ℕ
H : ∀ x ∈ Set.Icc 0 π, sin x ^ (n + 1) ≤ sin x ^ n :=
  fun x h => pow_le_pow_of_le_one (sin_nonneg_of_mem_Icc h) (sin_le_one x) (Nat.le_add_right n 1)
⊢ ∫ (x : ℝ) in 0 ..π, sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ n
-- Mathlib/Data/NNReal/Defs.lean
theorem coe_iSup {ι : Sort*} (s : ι → ℝ≥0) : (↑(⨆ i, s i) : ℝ) = ⨆ i, ↑(s i)

Proof state:
ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(⨆ i, s i) = ⨆ i, ↑(s i)

Tactic:
rw [iSup, iSup, coe_sSup, ← Set.range_comp]

Result:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i => s i)) = sSup (Set.range fun i => ↑(s i))

Proof state:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i => s i)) = sSup (Set.range fun i => ↑(s i))

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_sup (f : Filter α) (g₁ g₂ : Filter β) : f ×ˢ (g₁ ⊔ g₂) = (f ×ˢ g₁) ⊔ (f ×ˢ g₂)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂

Tactic:
simp only [prod_eq_inf, comap_sup, inf_sup_left]

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem linearIndependent_right' (H : A.LinearDisjoint L) {ι : Type*} {b : ι → L}
    (hb : LinearIndependent F b) : LinearIndependent A (algebraMap L E ∘ b)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
b : ι → L
hb : LinearIndependent F b
⊢ LinearIndependent (↥A) (⇑(algebraMap L E) ∘ b)

Tactic:
apply Subalgebra.LinearDisjoint.linearIndependent_right_of_flat H <| hb.map' _
  (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.ker

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncate_surjective {m : ℕ} (hm : n ≤ m) : Surjective (truncate (p := p) (R := R) hm)

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p n R
⊢ ∃ a, (truncate hm) a = x

Tactic:
obtain ⟨x, rfl⟩ := WittVector.truncate_surjective (p := p) _ R x

Result:
case intro
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ ∃ a, (truncate hm) a = (WittVector.truncate n) x

Proof state:
case intro
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : 𝕎 R
⊢ ∃ a, (truncate hm) a = (WittVector.truncate n) x

Tactic:
exact ⟨WittVector.truncate _ x, truncate_wittVector_truncate _ _⟩

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
⊢ Surjective ⇑(truncate hm)

Tactic:
intro x

Result:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : TruncatedWittVector p n R
⊢ ∃ a, (truncate hm) a = x
-- Mathlib/Data/Set/Function.lean
theorem univ_pi_piecewise_univ {ι : Type*} {α : ι → Type*} (s : Set ι) (t : ∀ i, Set (α i))
    [∀ x, Decidable (x ∈ s)] : pi univ (s.piecewise t fun _ => univ) = pi s t

Proof state:
ι : Type u_8
α : ι → Type u_9
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : (x : ι) → Decidable (x ∈ s)
⊢ univ.pi (s.piecewise t fun x => univ) = s.pi t

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem ContMDiffWithinAt.mfderivWithin_const {x₀ : M} {f : M → M'}
    (hf : ContMDiffWithinAt I I' n f s x₀)
    (hmn : m + 1 ≤ n) (hx : x₀ ∈ s) (hs : UniqueMDiffOn I s) :
    haveI : IsManifold I 1 M := .of_le (le_trans le_add_self hmn)
    haveI : IsManifold I' 1 M' := .of_le (le_trans le_add_self hmn)
    ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
      (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀) s x₀

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
⊢ ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀) s x₀

Tactic:
have : ContMDiffWithinAt (I.prod I) I' n (fun x : M × M => f x.2) (s ×ˢ s) (x₀, x₀) :=
  ContMDiffWithinAt.comp (x₀, x₀) hf contMDiffWithinAt_snd mapsTo_snd_prod

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
this : ContMDiffWithinAt (I.prod I) I' n (fun x => f x.2) (s ×ˢ s) (x₀, x₀)
⊢ ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀) s x₀

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : M
f : M → M'
hf : ContMDiffWithinAt I I' n f s x₀
hmn : m + 1 ≤ n
hx : x₀ ∈ s
hs : UniqueMDiffOn I s
this : ContMDiffWithinAt (I.prod I) I' n (fun x => f x.2) (s ×ˢ s) (x₀, x₀)
⊢ ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m (inTangentCoordinates I I' id f (mfderivWithin I I' f s) x₀) s x₀

Tactic:
exact this.mfderivWithin contMDiffWithinAt_id hx (mapsTo_id _) hmn hs

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem convexOn_of_deriv2_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
    (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D))
    (hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x) : ConvexOn ℝ D f :=
  (monotoneOn_of_deriv_nonneg hD.interior hf''.continuousOn (by rwa [interior_interior]) <| by
        rwa [interior_interior]).convexOn_of_deriv
    hD hf hf'

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
rwa [interior_interior]

Result:
no goals

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 ≤ deriv (deriv f) x

Tactic:
rwa [interior_interior]

Result:
no goals