harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
/-- See `Real.rpow_inv_log` for the equality when `x ≠ 1` is strictly positive. -/
lemma rpow_inv_log_le_exp_one : x ^ (log x)⁻¹ ≤ exp 1

Proof state:
x : ℝ
⊢ x ^ (log x)⁻¹ ≤ rexp 1

Tactic:
calc
  _ ≤ |x ^ (log x)⁻¹| := le_abs_self _
  _ ≤ |x| ^ (log x)⁻¹ := abs_rpow_le_abs_rpow ..

Result:
case calc.step
x : ℝ
⊢ |x| ^ (log x)⁻¹ ≤ rexp 1

Proof state:
case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1

Tactic:
gcongr

Result:
case calc.step.inr.h
x : ℝ
hx : 0 < |x|
⊢ log |x| * (log |x|)⁻¹ ≤ 1

Proof state:
case calc.step
x : ℝ
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
obtain hx | hx := (abs_nonneg x).eq_or_gt

Result:
case calc.step.inl
x : ℝ
hx : |x| = 0
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Proof state:
case calc.step
x : ℝ
⊢ |x| ^ (log x)⁻¹ ≤ rexp 1

Tactic:
rw [← log_abs]

Result:
case calc.step
x : ℝ
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Proof state:
case calc.step.inl
x : ℝ
hx : |x| = 0
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
simp [hx]

Result:
no goals

Proof state:
case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ |x| ^ (log |x|)⁻¹ ≤ rexp 1

Tactic:
rw [rpow_def_of_pos hx]

Result:
case calc.step.inr
x : ℝ
hx : 0 < |x|
⊢ rexp (log |x| * (log |x|)⁻¹) ≤ rexp 1

Proof state:
case calc.step.inr.h
x : ℝ
hx : 0 < |x|
⊢ log |x| * (log |x|)⁻¹ ≤ 1

Tactic:
exact mul_inv_le_one

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma ge_of_forall_gt_iff_ge {x y : EReal} : (∀ z : ℝ, z < y → z ≤ x) ↔ y ≤ x

Proof state:
x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ ∀ (z : WithTop ℝ), ↑z < y → ↑z ≤ x

Tactic:
rw [WithTop.forall]

Result:
x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ (↑⊤ < y → ↑⊤ ≤ x) ∧ ∀ (x_1 : ℝ), ↑↑x_1 < y → ↑↑x_1 ≤ x

Proof state:
x y : EReal
⊢ (∀ (z : ℝ), ↑z < y → ↑z ≤ x) ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ WithBot.ge_of_forall_gt_iff_ge.1 ?_, fun h _ x_z ↦ x_z.le.trans h⟩

Result:
x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ ∀ (z : WithTop ℝ), ↑z < y → ↑z ≤ x

Proof state:
x y : EReal
h : ∀ (z : ℝ), ↑z < y → ↑z ≤ x
⊢ (↑⊤ < y → ↑⊤ ≤ x) ∧ ∀ (x_1 : ℝ), ↑↑x_1 < y → ↑↑x_1 ≤ x

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_nonneg_iff_pos_imp_nonneg [ExistsAddOfLE α] [PosMulStrictMono α] [MulPosStrictMono α]
    [AddLeftMono α] [AddLeftReflectLE α] :
    0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
this : a ≤ 0 ∨ 0 ≤ a
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
have := le_total b 0

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
this✝ : a ≤ 0 ∨ 0 ≤ a
this : b ≤ 0 ∨ 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
this✝ : a ≤ 0 ∨ 0 ≤ a
this : b ≤ 0 ∨ 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
simp_rw [← not_le, ← or_iff_not_imp_left]

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
have := le_total a 0

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
this : a ≤ 0 ∨ 0 ≤ a
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
refine mul_nonneg_iff.trans ?_

Result:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
a b : α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem dvd_and_not_dvd_iff [CancelCommMonoidWithZero α] {x y : α} :
    x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x y :=
  ⟨fun ⟨⟨d, hd⟩, hyx⟩ =>
    ⟨fun hx0 => by simp [hx0] at hyx,
      ⟨d, mt isUnit_iff_dvd_one.1 fun ⟨e, he⟩ => hyx ⟨e, by rw [hd, mul_assoc, ← he, mul_one]⟩,
        hd⟩⟩,
    fun ⟨hx0, d, hdu, hdx⟩ =>
    ⟨⟨d, hdx⟩, fun ⟨e, he⟩ =>
      hdu
        (isUnit_of_dvd_one
          ⟨e, mul_left_cancel₀ hx0 <| by conv =>
            lhs
            rw [he, hdx]
            simp [mul_assoc]⟩)⟩⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)

Tactic:
conv =>
lhs
rw [he, hdx]
simp [mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False

Tactic:
simp [hx0] at hyx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = y * e

Tactic:
rw [hd, mul_assoc, ← he, mul_one]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Product.lean
theorem eq_of_forall_π_app_eq (a b : C)
    (h : ∀ (J : Finset ι), π_app C (· ∈ J) a = π_app C (· ∈ J) b) : a = b

Proof state:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : (fun j => ↑a ↑j) = fun j => ↑b ↑j
⊢ ↑a i = ↑b i

Tactic:
exact congr_fun h ⟨i, Finset.mem_singleton.mpr rfl⟩

Result:
no goals

Proof state:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
h : ∀ (J : Finset ι), (π_app C fun x => x ∈ J) a = (π_app C fun x => x ∈ J) b
⊢ a = b

Tactic:
ext i

Result:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
h : ∀ (J : Finset ι), (π_app C fun x => x ∈ J) a = (π_app C fun x => x ∈ J) b
i : ι
⊢ ↑a i = ↑b i

Proof state:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : (π_app C fun x => x ∈ {i}) a = (π_app C fun x => x ∈ {i}) b
⊢ ↑a i = ↑b i

Tactic:
rw [Subtype.ext_iff] at h

Result:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x => x ∈ {i}) a) = ↑((π_app C fun x => x ∈ {i}) b)
⊢ ↑a i = ↑b i

Proof state:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
h : ∀ (J : Finset ι), (π_app C fun x => x ∈ J) a = (π_app C fun x => x ∈ J) b
i : ι
⊢ ↑a i = ↑b i

Tactic:
specialize h ({i} : Finset ι)

Result:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : (π_app C fun x => x ∈ {i}) a = (π_app C fun x => x ∈ {i}) b
⊢ ↑a i = ↑b i

Proof state:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : ↑((π_app C fun x => x ∈ {i}) a) = ↑((π_app C fun x => x ∈ {i}) b)
⊢ ↑a i = ↑b i

Tactic:
simp only [π_app, ContinuousMap.precomp, ContinuousMap.coe_mk,
  Set.MapsTo.val_restrict_apply] at h

Result:
case a.h
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
i : ι
h : (fun j => ↑a ↑j) = fun j => ↑b ↑j
⊢ ↑a i = ↑b i
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
    (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Proof state:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)

Tactic:
simp only [subgroupOf, map_comap_eq, map_sup, range_subtype]

Result:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'

Proof state:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Tactic:
refine
  map_injective_of_ker_le B.subtype (ker_le_comap _ _)
    (le_trans (ker_le_comap B.subtype _) le_sup_left) ?_

Result:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)

Proof state:
G : Type u_1
inst✝ : Group G
A A' B : Subgroup G
hA : A ≤ B
hA' : A' ≤ B
⊢ B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'

Tactic:
rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_cWeight_eq_smul_wInner_one (f g : ∀ i, E i) :
    ⟪f, g⟫ₙ_[𝕜] = (Fintype.card ι : ℚ≥0)⁻¹ • ⟪f, g⟫_[𝕜]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
f g : (i : ι) → E i
⊢ wInner cWeight f g = (↑(Fintype.card ι))⁻¹ • wInner 1 f g

Tactic:
simp [wInner, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
lemma isConnected :
    IsConnected ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _)
      (Functor.rightUnitor _).inv).CostructuredArrowDownwards y)

Proof state:
case intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : L.obj (Φ.functor.obj c) ⟶ X₃
fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))
⊢ Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝)
    ((fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯))

Tactic:
have := zigzag_obj_of_zigzag
  (fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac)
    (isPreconnected_zigzag (RightResolution.mk (𝟙 _) (W₂.id_mem _))
      (RightResolution.mk ρ.w.right ρ.hw.2))

Result:
case intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
inst✝⁷ : Category.{u_4, u_1} C₁
inst✝⁶ : Category.{u_5, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{u_6, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this✝ : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : L.obj (Φ.functor.obj c) ⟶ X₃
fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯))
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯))
⊢ Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝)
    ((fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯))
-- Mathlib/Algebra/IsPrimePow.lean
theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) : IsPrimePow m

Proof state:
case intro.intro.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ 0 < i

Tactic:
apply Nat.pos_of_ne_zero

Result:
case intro.intro.intro.intro.intro.intro.a
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ i ≠ 0

Proof state:
case intro.intro.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i

Tactic:
refine ⟨p, i, hp, ?_, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ 0 < i

Proof state:
n m : ℕ
hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m

Tactic:
rcases hn with ⟨p, k, hp, _hk, rfl⟩

Result:
case intro.intro.intro.intro
m : ℕ
hm₁ : m ≠ 1
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hm : m ∣ p ^ k
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m

Proof state:
case intro.intro.intro.intro
m : ℕ
hm₁ : m ≠ 1
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hm : m ∣ p ^ k
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m

Tactic:
obtain ⟨i, hik, rfl⟩ := (Nat.dvd_prime_pow hp).1 hm

Result:
case intro.intro.intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ i

Proof state:
case intro.intro.intro.intro.intro.intro.a
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hik : 0 ≤ k
hm₁ : p ^ 0 ≠ 1
hm : p ^ 0 ∣ p ^ k
⊢ False

Tactic:
simp only [pow_zero, ne_eq, not_true_eq_false] at hm₁

Result:
no goals

Proof state:
n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m

Tactic:
rw [isPrimePow_nat_iff] at hn ⊢

Result:
n m : ℕ
hn : ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = m

Proof state:
case intro.intro.intro.intro.intro.intro.a
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
i : ℕ
hik : i ≤ k
hm₁ : p ^ i ≠ 1
hm : p ^ i ∣ p ^ k
⊢ i ≠ 0

Tactic:
rintro rfl

Result:
case intro.intro.intro.intro.intro.intro.a
p k : ℕ
hp : Nat.Prime p
_hk : 0 < k
hik : 0 ≤ k
hm₁ : p ^ 0 ≠ 1
hm : p ^ 0 ∣ p ^ k
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_eq_arccos {x : ℝ} (h : 0 ≤ x) : arctan x = arccos (√(1 + x ^ 2))⁻¹

Proof state:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

Tactic:
exact inv_nonneg.2 (sqrt_nonneg _)

Result:
no goals

Proof state:
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

Tactic:
swap

Result:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

Proof state:
x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (√(1 + x ^ 2))⁻¹

Tactic:
rw [arctan_eq_arcsin, arccos_eq_arcsin]

Result:
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (√(1 + x ^ 2))⁻¹

Proof state:
case e_a
x : ℝ
h : 0 ≤ x
⊢ x / √(1 + x ^ 2) = √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

Tactic:
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel_left, sqrt_div,
  sqrt_sq h]

Result:
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2

case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0

case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹

Proof state:
case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / √(1 + x ^ 2)) = arcsin √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

Tactic:
congr 1

Result:
case e_a
x : ℝ
h : 0 ≤ x
⊢ x / √(1 + x ^ 2) = √(1 - (√(1 + x ^ 2))⁻¹ ^ 2)

Proof state:
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2

case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0

case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹

Tactic:
all_goals positivity

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem norm_injOn_ray_left (hx : x ≠ 0) : { y | SameRay ℝ x y }.InjOn norm

Proof state:
case intro.intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
z : F
hz : z ∈ {y | SameRay ℝ x y}
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖z‖
⊢ r • x = z

Tactic:
rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩

Result:
case intro.intro.intro.intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖s • x‖
⊢ r • x = s • x

Proof state:
case intro.intro.intro.intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖s • x‖
⊢ r • x = s • x

Tactic:
rw [norm_smul, norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr,
  norm_of_nonneg hs] at h

Result:
case intro.intro.intro.intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : r = s
⊢ r • x = s • x

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ Set.InjOn Norm.norm {y | SameRay ℝ x y}

Tactic:
rintro y hy z hz h

Result:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
y : F
hy : y ∈ {y | SameRay ℝ x y}
z : F
hz : z ∈ {y | SameRay ℝ x y}
h : ‖y‖ = ‖z‖
⊢ y = z

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
y : F
hy : y ∈ {y | SameRay ℝ x y}
z : F
hz : z ∈ {y | SameRay ℝ x y}
h : ‖y‖ = ‖z‖
⊢ y = z

Tactic:
rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩

Result:
case intro.intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
z : F
hz : z ∈ {y | SameRay ℝ x y}
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖z‖
⊢ r • x = z

Proof state:
case intro.intro.intro.intro
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : r = s
⊢ r • x = s • x

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem constr_range {f : ι → M'} :
    LinearMap.range (constr (M' := M') b S f) = span R (range f)

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
S : Type u_10
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : ι → M'
⊢ LinearMap.range ((b.constr S) f) = span R (range f)

Tactic:
rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
  Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
  Finsupp.span_image_eq_map_linearCombination, Set.image_id]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem mul_integral_upcrossingsBefore_le_integral_pos_part_aux [IsFiniteMeasure μ]
    (hf : Submartingale f ℱ μ) (hab : a < b) :
    (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[fun ω => (f N ω - a)⁺]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ =
    (b - a - 0) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ

Tactic:
simp_rw [sub_zero, ← upcrossingsBefore_pos_eq hab]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N x) ∂μ =
    (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ

Tactic:
refine le_trans (le_of_eq ?_)
  (integral_mul_upcrossingsBefore_le_integral (hf.sub_martingale (martingale_const _ _ _)).pos
    (fun ω => posPart_nonneg _)
    (fun ω => posPart_nonneg _) (sub_pos.2 hab))

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ =
    (b - a - 0) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (fun n ω => (f n ω - a)⁺) N x) ∂μ =
    (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore 0 (b - a) (f - fun x x => a)⁺ N x) ∂μ

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioi' (h₁ : c ≤ b) : Ioc a b ∪ Ioi c = Ioi (min a c)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : c < x
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

Tactic:
simp only [hc, or_true]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

Tactic:
by_cases hc : c < x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : c < x
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c < x
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ioc a b ∪ Ioi c ↔ x ∈ Ioi (a ⊓ c)

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c < x
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

Tactic:
have hxb : x ≤ b := (le_of_not_gt hc).trans h₁

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c < x
hxb : x ≤ b
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x

Tactic:
simp only [hxb, and_true]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ x ∈ Ioc a b ∪ Ioi c ↔ x ∈ Ioi (a ⊓ c)

Tactic:
simp_rw [mem_union, mem_Ioc, mem_Ioi, min_lt_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ a < x ∧ x ≤ b ∨ c < x ↔ a < x ∨ c < x