harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem ofReal_rpow_of_nonneg {x p : ℝ} (hx_nonneg : 0 ≤ x) (hp_nonneg : 0 ≤ p) :
    ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Proof state:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp [hp0]

Result:
no goals

Proof state:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)

Result:
no goals

Proof state:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
rw [← Ne] at hp0

Result:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Proof state:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm

Result:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Proof state:
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
by_cases hp0 : p = 0

Result:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Proof state:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
simp [hx0, hp_pos, hp_pos.ne.symm]

Result:
no goals

Proof state:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
by_cases hx0 : x = 0

Result:
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Proof state:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

Tactic:
rw [← Ne] at hx0

Result:
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem inverse_compare : pkg.compare pkg' ∘ pkg'.compare pkg = id

Proof state:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
apply pkg'.funext (uc.comp uc').continuous continuous_id

Result:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ ∀ (a : α), (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Proof state:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg'.coe a = id (pkg'.coe a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
have uc' := pkg'.uniformContinuous_compare pkg

Result:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Proof state:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ ∀ (a : α), (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Tactic:
intro a

Result:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Proof state:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Tactic:
have uc := pkg.uniformContinuous_compare pkg'

Result:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id

Proof state:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)

Tactic:
rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']

Result:
α : Type u_1
inst✝ : UniformSpace α
pkg pkg' : AbstractCompletion α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ pkg'.coe a = id (pkg'.coe a)
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem ae_dirac_eq [MeasurableSingletonClass α] (a : α) : ae (dirac a) = pure a

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
⊢ ae (dirac a) = pure a

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a

Tactic:
simp [mem_ae_iff, imp_false]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem smul_single {S} [SMulZeroClass S k] (s : S) (a : G) (b : k) :
    s • single a b = single a (s • b) :=
  toFinsupp_injective <| by simp;

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : SMulZeroClass S k
s : S
a : G
b : k
⊢ (s • single a b).toFinsupp = (single a (s • b)).toFinsupp

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
lemma ker_evalStarAlgHom_eq_closure_adjoin_id (s : Set 𝕜) (h0 : 0 ∈ s) [CompactSpace s] :
    (RingHom.ker (evalStarAlgHom 𝕜 𝕜 (⟨0, h0⟩ : s)) : Set C(s, 𝕜)) =
      closure (adjoin 𝕜 {(restrict s (.id 𝕜))})

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) = closure ↑(adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)})

Tactic:
rw [← ker_evalStarAlgHom_inter_adjoin_id s h0,
  AlgHom.closure_ker_inter (φ := evalStarAlgHom 𝕜 𝕜 (X := s) ⟨0, h0⟩) (continuous_eval_const _) _]

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) =
    closure ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩)) =
    closure ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) ∩ ↑(RingHom.ker (evalStarAlgHom 𝕜 𝕜 ⟨0, h0⟩))

Tactic:
convert (Set.univ_inter _).symm

Result:
case h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ closure ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) = Set.univ

Proof state:
case h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ closure ↑(polynomialFunctions s).starClosure = Set.univ

Tactic:
congrm(($(polynomialFunctions.starClosure_topologicalClosure s) : Set C(s, 𝕜)))

Result:
no goals

Proof state:
case h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ closure ↑(StarAlgebra.adjoin 𝕜 {restrict s (ContinuousMap.id 𝕜)}) = Set.univ

Tactic:
rw [← Polynomial.toContinuousMapOn_X_eq_restrict_id, ← Polynomial.toContinuousMapOnAlgHom_apply,
  ← polynomialFunctions.starClosure_eq_adjoin_X s]

Result:
case h.e'_3.h.e'_3
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
h0 : 0 ∈ s
inst✝ : CompactSpace ↑s
⊢ closure ↑(polynomialFunctions s).starClosure = Set.univ
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_pi_Ioc_toReal {a b : ι → ℝ} (h : a ≤ b) :
    (volume (pi univ fun i => Ioc (a i) (b i))).toReal = ∏ i, (b i - a i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (univ.pi fun i => Ioc (a i) (b i))).toReal = ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_pi_Ioc, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem piecewise {m : MeasurableSpace α} [TopologicalSpace β] {s : Set α}
    {_ : DecidablePred (· ∈ s)} (hs : MeasurableSet s) (hf : StronglyMeasurable f)
    (hg : StronglyMeasurable g) : StronglyMeasurable (Set.piecewise s f g)

Proof state:
case pos
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto (fun n => ((fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 (s.piecewise f g x))

Tactic:
simpa [@Set.piecewise_eq_of_mem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx,
  hx] using hf.tendsto_approx x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ((fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 (s.piecewise f g x))

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto (fun n => ((fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 (s.piecewise f g x))

case neg
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun n => ((fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 (s.piecewise f g x))

Proof state:
case neg
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun n => ((fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 (s.piecewise f g x))

Tactic:
simpa [@Set.piecewise_eq_of_not_mem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx,
  hx] using hg.tendsto_approx x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (s.piecewise f g)

Tactic:
refine ⟨fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n), fun x => ?_⟩

Result:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ((fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n) x) atTop
    (𝓝 (s.piecewise f g x))
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem _root_.VectorBundleCore.inCoordinates_eq {ι ι'} (Z : VectorBundleCore 𝕜₁ B F ι)
    (Z' : VectorBundleCore 𝕜₂ B' F' ι') {x₀ x : B} {y₀ y : B'} (ϕ : F →SL[σ] F')
    (hx : x ∈ Z.baseSet (Z.indexAt x₀)) (hy : y ∈ Z'.baseSet (Z'.indexAt y₀)) :
    inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
      (Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp
        (ϕ.comp <| Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x)

Proof state:
B : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : TopologicalSpace B
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst✝⁵ : NontriviallyNormedField 𝕜₁
inst✝⁴ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst✝³ : TopologicalSpace B'
inst✝² : NormedSpace 𝕜₁ F
F' : Type u_8
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜₂ F'
ι : Type u_10
ι' : Type u_11
Z : VectorBundleCore 𝕜₁ B F ι
Z' : VectorBundleCore 𝕜₂ B' F' ι'
x₀ x : B
y₀ y : B'
ϕ : F →SL[σ] F'
hx : x ∈ Z.baseSet (Z.indexAt x₀)
hy : y ∈ Z'.baseSet (Z'.indexAt y₀)
⊢ inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
    (Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y).comp (ϕ.comp (Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x))

Tactic:
simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy,
  Z.trivializationAt_symmL hx]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ico_succ_right_eq_insert_of_not_isMax (h₁ : a ≤ b) (h₂ : ¬IsMax b) :
    Ico a (succ b) = insert b (Ico a b)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)

Tactic:
simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
lemma Set.Subsingleton.isClosed [T1Space X] {A : Set X} (h : A.Subsingleton) : IsClosed A

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
h : A.Subsingleton
⊢ IsClosed A

Tactic:
rcases h.eq_empty_or_singleton with rfl | ⟨x, rfl⟩

Result:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : ∅.Subsingleton
⊢ IsClosed ∅

case inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
h : {x}.Subsingleton
⊢ IsClosed {x}

Proof state:
case inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
h : {x}.Subsingleton
⊢ IsClosed {x}

Tactic:
exact isClosed_singleton

Result:
no goals

Proof state:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : ∅.Subsingleton
⊢ IsClosed ∅

Tactic:
exact isClosed_empty

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem mul_le_sin {x : ℝ} (hx : 0 ≤ x) (hx' : x ≤ π / 2) : 2 / π * x ≤ sin x

Proof state:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ 2 / π * x ≤ sin x

Tactic:
rw [← inv_div]

Result:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x

Proof state:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ sin x

Tactic:
simpa [-inv_div, mul_inv_cancel_left₀ pi_div_two_pos.ne'] using @le_sin_mul ((π / 2)⁻¹ * x)
  (mul_nonneg (inv_nonneg.2 pi_div_two_pos.le) hx)
  (by rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos])

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1

Tactic:
rwa [← div_eq_inv_mul, div_le_one pi_div_two_pos]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map₂_eq_mapAccumr₂ {f : α → β → γ} :
    map₂ f xs ys = (mapAccumr₂ (fun x y (_ : Unit) ↦ ((), f x y)) xs ys ()).snd

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
xs : Vector α n
ys : Vector β n
f : α → β → γ
⊢ map₂ f xs ys = (mapAccumr₂ (fun x y x_1 => ((), f x y)) xs ys ()).2

Tactic:
induction xs, ys using Vector.revInductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/GroupTheory/Solvable.lean
theorem map_derivedSeries_le_derivedSeries (n : ℕ) :
    (derivedSeries G n).map f ≤ derivedSeries G' n

Proof state:
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : map f (derivedSeries G n) ≤ derivedSeries G' n
⊢ map f (derivedSeries G (n + 1)) ≤ derivedSeries G' (n + 1)

Tactic:
simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n

Tactic:
induction n with
| zero => exact le_top
| succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Result:
no goals

Proof state:
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ map f (derivedSeries G 0) ≤ derivedSeries G' 0

Tactic:
exact le_top

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i

Proof state:
k : ℕ
i : Fin k
⊢ idxOf i (finRange k) = ↑i

Tactic:
simpa using idxOf_getElem (nodup_finRange k) i

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem ker_flip_eq_bot (H : B.IsRefl) (h : LinearMap.ker B = ⊥) : LinearMap.ker B.flip = ⊥

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B = ⊥
x✝ : M₁
hx : B.flip x✝ = 0
⊢ B x✝ = 0

Tactic:
ext

Result:
case h
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B = ⊥
x✝¹ : M₁
hx : B.flip x✝¹ = 0
x✝ : M₁
⊢ (B x✝¹) x✝ = 0 x✝

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B = ⊥
⊢ ker B.flip = ⊥

Tactic:
refine ker_eq_bot'.mpr fun _ hx ↦ ker_eq_bot'.mp h _ ?_

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B = ⊥
x✝ : M₁
hx : B.flip x✝ = 0
⊢ B x✝ = 0

Proof state:
case h
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B = ⊥
x✝¹ : M₁
hx : B.flip x✝¹ = 0
x✝ : M₁
⊢ (B x✝¹) x✝ = 0 x✝

Tactic:
exact H _ _ (LinearMap.congr_fun hx _)

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma pow_dvd_pow_of_sub_pow_eq_zero (hp : n + m ≤ p + 1) (h_comm : Commute x y)
    (h : (x - y) ^ n = 0) : x ^ m ∣ y ^ p

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ y ^ p

Tactic:
rw [← sub_add_cancel y x]

Result:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ (y - x + x) ^ p

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ x ^ m ∣ (y - x + x) ^ p

Tactic:
apply (h_comm.symm.sub_left rfl).pow_dvd_add_pow_of_pow_eq_zero_left hp _

Result:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (y - x) ^ n = 0

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
h : (x - y) ^ n = 0
⊢ (y - x) ^ n = 0

Tactic:
rw [← neg_sub x y, neg_pow, h, mul_zero]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem map_toDual_max (s : Finset α) : s.max.map toDual = (s.image toDual).min

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min

Tactic:
rw [min_eq_inf_withTop, inf_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = s.inf (WithTop.some ∘ ⇑toDual)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = s.inf (WithTop.some ∘ ⇑toDual)

Tactic:
exact congr_fun Option.map_id _

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem norm_id_of_nontrivial_seminorm (h : ∃ x : V, ‖x‖ ≠ 0) : ‖id V‖ = 1 :=
  le_antisymm (norm_id_le V) <| by
    let ⟨x, hx⟩ := h
    have := (id V).ratio_le_opNorm x
    rwa [id_apply, div_self hx] at this

Proof state:
V : Type u_1
inst✝ : SeminormedAddCommGroup V
h : ∃ x, ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖

Tactic:
let ⟨x, hx⟩ := h

Result:
V : Type u_1
inst✝ : SeminormedAddCommGroup V
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖

Proof state:
V : Type u_1
inst✝ : SeminormedAddCommGroup V
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
this : ‖(id V) x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖

Tactic:
rwa [id_apply, div_self hx] at this

Result:
no goals

Proof state:
V : Type u_1
inst✝ : SeminormedAddCommGroup V
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖

Tactic:
have := (id V).ratio_le_opNorm x

Result:
V : Type u_1
inst✝ : SeminormedAddCommGroup V
h : ∃ x, ‖x‖ ≠ 0
x : V
hx : ‖x‖ ≠ 0
this : ‖(id V) x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖
-- Mathlib/MeasureTheory/Measure/Dirac.lean
lemma mutuallySingular_dirac [MeasurableSingletonClass α] (x : α) (μ : Measure α) [NoAtoms μ] :
    Measure.dirac x ⟂ₘ μ :=
  ⟨{x}ᶜ, (MeasurableSet.singleton x).compl, by simp, by simp⟩

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
x : α
μ : Measure α
inst✝ : NoAtoms μ
⊢ (dirac x) {x}ᶜ = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
x : α
μ : Measure α
inst✝ : NoAtoms μ
⊢ μ {x}ᶜᶜ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem factors_one : factors (1 : α) = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ factors 1 = 0

Tactic:
nontriviality α using factors

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ factors 1 = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ 1

Tactic:
exact factors_prod one_ne_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Multiset.Rel ?m.42423 (factors 1) 0

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Type ?u.42420

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ α → ?m.42422 → Prop

Tactic:
refine factors_unique irreducible_of_factor (fun x hx => (Multiset.not_mem_zero x hx).elim) ?_

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ Multiset.prod 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ Multiset.prod 0

Tactic:
rw [Multiset.prod_zero]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ (factors 1).prod ~ᵤ 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ factors 1 = 0

Tactic:
rw [← Multiset.rel_zero_right]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Multiset.Rel ?m.42423 (factors 1) 0

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ Type ?u.42420

α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a✝ : Nontrivial α
⊢ α → ?m.42422 → Prop