harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem mem_torsion {x : (𝓞 K)ˣ} [NumberField K] :
    x ∈ torsion K ↔ ∀ w : InfinitePlace K, w x = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
⊢ x ∈ torsion K ↔ ∀ (w : InfinitePlace K), w ((algebraMap (𝓞 K) K) ↑x) = 1

Tactic:
rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion]

Result:
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
⊢ IsOfFinOrder x ↔ ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ x ^ n = 1

Tactic:
ext

Result:
case a.h
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1

Proof state:
case intro.intro
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n, hn, by ext; rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
  NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
⊢ IsOfFinOrder x ↔ ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1

Tactic:
refine ⟨fun hx φ ↦ (((φ.comp <| algebraMap (𝓞 K) K).toMonoidHom.comp <|
  Units.coeHom _).isOfFinOrder hx).norm_eq_one, fun h ↦ isOfFinOrder_iff_pow_eq_one.2 ?_⟩

Result:
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Tactic:
obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.isIntegral_coe h

Result:
case intro.intro
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

Proof state:
case a.h
K : Type u_1
inst✝¹ : Field K
x : (𝓞 K)ˣ
inst✝ : NumberField K
h : ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ = 1
n : ℕ
hn : 0 < n
hx : (algebraMap (𝓞 K) K) ↑x ^ n = 1
⊢ ↑↑(x ^ n) = ↑↑1

Tactic:
rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem tangentMapWithin_congr (h : ∀ x ∈ s, f x = f₁ x) (p : TangentBundle I M) (hp : p.1 ∈ s)
    (hs : UniqueMDiffWithinAt I s p.1) :
    tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s p

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
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'
f f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj ∈ s
hs : UniqueMDiffWithinAt I s p.proj
⊢ HEq (tangentMapWithin I I' f s p).snd (tangentMapWithin I I' f₁ s p).snd

Tactic:
rw [tangentMapWithin, h p.1 hp, tangentMapWithin, mfderivWithin_congr hs h (h _ hp)]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
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'
f f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj ∈ s
hs : UniqueMDiffWithinAt I s p.proj
⊢ tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s p

Tactic:
refine TotalSpace.ext (h p.1 hp) ?_

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
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'
f f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj ∈ s
hs : UniqueMDiffWithinAt I s p.proj
⊢ HEq (tangentMapWithin I I' f s p).snd (tangentMapWithin I I' f₁ s p).snd
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
@[to_additive]
lemma ne_bot_iff_exists_ne_one {H : Subgroup G} : H ≠ ⊥ ↔ ∃ a : ↥H, a ≠ 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≠ ⊥ ↔ ∃ a, a ≠ 1

Tactic:
rw [← nontrivial_iff_ne_bot, nontrivial_iff_exists_ne_one]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ∃ a, a ≠ 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (∃ x ∈ H, x ≠ 1) ↔ ∃ a, a ≠ 1

Tactic:
simp only [ne_eq, Subtype.exists, mk_eq_one, exists_prop]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma lt_iff_exists_coe : x < y ↔ ∃ a : α, x = a ∧ a < y

Proof state:
α : Type u_1
inst✝ : LT α
x y : WithTop α
⊢ x < y ↔ ∃ a, x = ↑a ∧ ↑a < y

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem variance_eq {f : α → ℝ} {g : β → ℝ} (h : IdentDistrib f g μ ν) :
    variance f μ = variance g ν

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν].toReal = Var[g; ν]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ Var[f; μ] = Var[g; ν]

Tactic:
rw [variance, h.evariance_eq]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν].toReal = Var[g; ν]
-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem nhds_one_hasBasis (B : GroupFilterBasis G) :
    HasBasis (@nhds G B.topology 1) (fun V : Set G ↦ V ∈ B) id

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ toFilterBasis.filter.HasBasis (fun V => V ∈ B) id

Tactic:
exact B.toFilterBasis.hasBasis

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ (𝓝 1).HasBasis (fun V => V ∈ B) id

Tactic:
rw [B.nhds_one_eq]

Result:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ toFilterBasis.filter.HasBasis (fun V => V ∈ B) id
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma tendsto_defaultRatCDF_atTop : Tendsto defaultRatCDF atTop (𝓝 1)

Proof state:
⊢ Tendsto defaultRatCDF atTop (𝓝 1)

Tactic:
refine (tendsto_congr' ?_).mp tendsto_const_nhds

Result:
⊢ (fun x => 1) =ᶠ[atTop] defaultRatCDF

Proof state:
⊢ (fun x => 1) =ᶠ[atTop] defaultRatCDF

Tactic:
rw [EventuallyEq, eventually_atTop]

Result:
⊢ ∃ a, ∀ b ≥ a, 1 = defaultRatCDF b

Proof state:
⊢ ∃ a, ∀ b ≥ a, 1 = defaultRatCDF b

Tactic:
exact ⟨0, fun q hq => (if_neg (not_lt.mpr hq)).symm⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma exp_neg_llr [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) :
    (fun x ↦ exp (- llr μ ν x)) =ᵐ[μ] fun x ↦ (ν.rnDeriv μ x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [hx, hx_exp_log]

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [Pi.neg_apply] at hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ (fun x => rexp (-llr μ ν x)) =ᶠ[ae μ] fun x => (ν.rnDeriv μ x).toReal

Tactic:
filter_upwards [neg_llr hμν, exp_llr_of_ac' ν μ hμν] with x hx hx_exp_log

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
-- Mathlib/Algebra/Group/Defs.lean
theorem npowRec_eq {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
    npowRec (k + 1) m = 1 * npowRec' (k + 1) m

Proof state:
case e_a
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m = 1 * npowRec' k.succ m

Tactic:
simp [ih]

Result:
no goals

Proof state:
case ind
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k' → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k' + 1) m = 1 * npowRec' (k' + 1) m

Tactic:
match k' with
| 0 => rfl
| k + 1 =>
  rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
  congr
  simp [ih]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m

Tactic:
congr

Result:
case e_a
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m = 1 * npowRec' k.succ m

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (0 + 1) m = 1 * npowRec' (0 + 1) m

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k : ℕ
m : M
⊢ npowRec (k + 1) m = 1 * npowRec' (k + 1) m

Tactic:
induction k using Nat.strongRecOn with
| ind k' ih =>
  match k' with
  | 0 => rfl
  | k + 1 =>
    rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
    congr
    simp [ih]

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1 + 1) m = 1 * npowRec' (k + 1 + 1) m

Tactic:
rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]

Result:
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' k : ℕ
ih : ∀ (m_1 : ℕ), m_1 < k + 1 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (k + 1) m * m = 1 * npowRec' k.succ m * m
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem exists_eventuallyEq_pow_smul_nonzero_iff (hf : AnalyticAt 𝕜 f z₀) :
    (∃ (n : ℕ), ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧
    ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔ (¬∀ᶠ z in 𝓝 z₀, f z = 0)

Proof state:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) → ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
rintro ⟨n, g, hg_an, hg_ne, hg_eq⟩

Result:
case mp.intro.intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Proof state:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hf_ne : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
rcases hf with ⟨p, hp⟩

Result:
case mpr.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf_ne : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) : (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getKey! k = if (f (m.get? k)).isSome = true then k else default

Tactic:
simp [getKey!_alter h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id)

Proof state:
α : Type u_1
γ : Type u_2
β : Type u_3
f : α → γ
l₁ : List α
l₂ : List β
⊢ (map f l₁).zip l₂ = map (Prod.map f id) (l₁.zip l₂)

Tactic:
rw [← zip_map, map_id]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem strictConvexOn_zpow {m : ℤ} (hm₀ : m ≠ 0) (hm₁ : m ≠ 1) :
    StrictConvexOn ℝ (Ioi 0) fun x : ℝ => x ^ m

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv^[2] (fun x => x ^ m) x

Tactic:
rw [mem_Ioi] at hx

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x => x ^ m) x

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x => x ^ m) x

Tactic:
rw [iter_deriv_zpow]

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i ∈ Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Ico 0 ↑2
⊢ False

Tactic:
rw [← Finset.coe_Ico] at hm

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ ↑(Finset.Ico 0 ↑2)
⊢ False

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i ∈ Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)

Tactic:
refine mul_pos ?_ (zpow_pos hx _)

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i ∈ Finset.range 2, (↑m - ↑i)

Proof state:
case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x => x ^ m) (Ioi 0)

Tactic:
exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx

Result:
no goals

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Finset.Ico 0 2
⊢ False

Tactic:
fin_cases hm <;> simp_all

Result:
no goals

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ ↑(Finset.Ico 0 ↑2)
⊢ False

Tactic:
norm_cast at hm

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Finset.Ico 0 2
⊢ False

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i ∈ Finset.range 2, (↑m - ↑i)

Tactic:
norm_cast

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i ∈ Finset.range 2, (m - ↑i)

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i ∈ Finset.range 2, (m - ↑i)

Tactic:
refine int_prod_range_pos (by decide) fun hm => ?_

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Ico 0 ↑2
⊢ False

Proof state:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ Even 2

Tactic:
decide

Result:
no goals

Proof state:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ x ∈ Ioi 0, 0 < deriv^[2] (fun x => x ^ m) x

Tactic:
intro x hx

Result:
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv^[2] (fun x => x ^ m) x

Proof state:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (Ioi 0) fun x => x ^ m

Tactic:
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)

Result:
case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x => x ^ m) (Ioi 0)

case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ x ∈ Ioi 0, 0 < deriv^[2] (fun x => x ^ m) x
-- Mathlib/Data/Real/Sqrt.lean
theorem coe_sqrt {x : ℝ≥0} : (NNReal.sqrt x : ℝ) = √(x : ℝ)

Proof state:
x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = √↑x

Tactic:
rw [Real.sqrt, Real.toNNReal_coe]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem NNReal.upper_bound {α : Type*} [TopologicalSpace α] (f : α →ᵇ ℝ≥0) (x : α) :
    f x ≤ nndist f 0

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (f x) (0 x) ≤ nndist f 0
⊢ f x ≤ nndist f 0

Tactic:
simp only [coe_zero, Pi.zero_apply] at key

Result:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (f x) 0 ≤ nndist f 0
⊢ f x ≤ nndist f 0

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (f x) 0 ≤ nndist f 0
⊢ f x ≤ nndist f 0

Tactic:
rwa [NNReal.nndist_zero_eq_val' (f x)] at key

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
⊢ f x ≤ nndist f 0

Tactic:
have key : nndist (f x) ((0 : α →ᵇ ℝ≥0) x) ≤ nndist f 0 := @dist_coe_le_dist α ℝ≥0 _ _ f 0 x

Result:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ≥0
x : α
key : nndist (f x) (0 x) ≤ nndist f 0
⊢ f x ≤ nndist f 0
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem comap_prime (hinv : ∀ a, g (f a : N) = a) (hp : Prime (f p)) : Prime p :=
  ⟨fun h => hp.1 <| by simp [h], fun h => hp.2.1 <| h.map f, fun a b h => by
    refine
        (hp.2.2 (f a) (f b) <| by
              convert map_dvd f h
              simp).imp
          ?_ ?_ <;>
      · intro h
        convert ← map_dvd g h <;> apply hinv⟩

Proof state:
case h.e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f a * f b = f (a * b)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ p ∣ b

Tactic:
convert ← map_dvd g h <;> apply hinv

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
h : p = 0
⊢ f p = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a * f b

Tactic:
convert map_dvd f h

Result:
case h.e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f a * f b = f (a * b)

Proof state:
case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f b → p ∣ b

Tactic:
intro h

Result:
case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ p ∣ b
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem inv_hom {A B : Grp_ C} (f : A ⟶ B) : A.inv ≫ f.hom = f.hom ≫ B.inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
this : lift (lift f.hom (A.inv ≫ f.hom)) f.hom = lift (lift f.hom (f.hom ≫ B.inv)) f.hom
⊢ A.inv ≫ f.hom = f.hom ≫ B.inv

Tactic:
simpa using (this =≫ fst _ _) =≫ snd _ _

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
⊢ lift (lift f.hom (A.inv ≫ f.hom)) f.hom = lift (lift f.hom (f.hom ≫ B.inv)) f.hom

Tactic:
apply B.isPullback.hom_ext <;> apply ChosenFiniteProducts.hom_ext <;>
  simp [lift_inv_comp_right, lift_inv_comp_left]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
⊢ A.inv ≫ f.hom = f.hom ≫ B.inv

Tactic:
suffices lift (lift f.hom (A.inv ≫ f.hom)) f.hom =
    lift (lift f.hom (f.hom ≫ B.inv)) f.hom by simpa using (this =≫ fst _ _) =≫ snd _ _

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
⊢ lift (lift f.hom (A.inv ≫ f.hom)) f.hom = lift (lift f.hom (f.hom ≫ B.inv)) f.hom