harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem integerSetToAssociates_eq_iff (a b : integerSet K) :
    integerSetToAssociates K a = integerSetToAssociates K b ↔
      ∃ ζ : torsion K, ζ • a = b

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ unitsNonZeroDivisorsEquiv u ∈ torsion K

Tactic:
exact (unit_smul_mem_iff_mem_torsion a.prop.1 _).mp (by simpa [h] using b.prop.1)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ integerSetToAssociates K a = integerSetToAssociates K b ↔ ∃ ζ, ζ • a = b

Tactic:
simp_rw [integerSetToAssociates_apply, Associates.quotient_mk_eq_mk,
  Associates.mk_eq_mk_iff_associated, Associated, mul_comm, Subtype.ext_iff,
  RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, Submonoid.coe_mul, map_mul,
  mixedEmbedding_preimageOfMemIntegerSet, integerSetTorsionSMul_smul_coe]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ (∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b) ↔ ∃ ζ, ↑ζ • ↑a = ↑b

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
⊢ (∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b) ↔ ∃ ζ, ↑ζ • ↑a = ↑b

Tactic:
refine ⟨fun ⟨u, h⟩ ↦  ⟨⟨unitsNonZeroDivisorsEquiv u, ?_⟩, by simpa using h⟩,
  fun ⟨⟨u, _⟩, h⟩ ↦ ⟨unitsNonZeroDivisorsEquiv.symm u, by simpa using h⟩⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ unitsNonZeroDivisorsEquiv u ∈ torsion K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ ↑⟨unitsNonZeroDivisorsEquiv u, ?m.167507⟩ • ↑a = ↑b

Tactic:
simpa using h

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ u, (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
u : (↥(𝓞 K)⁰)ˣ
h : (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑u) * ↑a = ↑b
⊢ unitsNonZeroDivisorsEquiv u • ↑a ∈ fundamentalCone K

Tactic:
simpa [h] using b.prop.1

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : ↑(integerSet K)
x✝ : ∃ ζ, ↑ζ • ↑a = ↑b
u : (𝓞 K)ˣ
property✝ : u ∈ torsion K
h : ↑⟨u, property✝⟩ • ↑a = ↑b
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑(unitsNonZeroDivisorsEquiv.symm u)) * ↑a = ↑b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem ae_kernel_lt_top (a : α) (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
    ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' s) < ∞

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
have h2t : (κ ⊗ₖ η) a t ≠ ∞ := by rwa [measure_toMeasurable]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
    (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i

Proof state:
s n : Nat
p : Nat → Bool
⊢ find? p (List.range' s n).toArray = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

Tactic:
simp only [List.find?_toArray]

Result:
s n : Nat
p : Nat → Bool
⊢ List.find? p (List.range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

Proof state:
s n : Nat
p : Nat → Bool
⊢ List.find? p (List.range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

Tactic:
simp

Result:
no goals

Proof state:
s n : Nat
p : Nat → Bool
⊢ find? p (range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

Tactic:
rw [← List.toArray_range']

Result:
s n : Nat
p : Nat → Bool
⊢ find? p (List.range' s n).toArray = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_map (f : α → β) (l : List α) (h) :
    getLast (map f l) h = f (getLast l (by simpa using h))

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (map f (head✝ :: tail✝)).getLast h = f ((head✝ :: tail✝).getLast ⋯)

Tactic:
simp only [← getElem_cons_length _ _ _ rfl]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (map f (head✝ :: tail✝)).getLast h = f (head✝ :: tail✝)[tail✝.length]

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (f head✝ :: map f tail✝)[(map f tail✝).length] = f (head✝ :: tail✝)[tail✝.length]

Tactic:
simp only [← map_cons, getElem_map]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ f (head✝ :: tail✝)[(map f tail✝).length] = f (head✝ :: tail✝)[tail✝.length]

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (f head✝ :: map f tail✝).getLast ⋯ = f (head✝ :: tail✝)[tail✝.length]

Tactic:
simp only [← getElem_cons_length _ _ _ rfl]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (f head✝ :: map f tail✝)[(map f tail✝).length] = f (head✝ :: tail✝)[tail✝.length]

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (map f (head✝ :: tail✝)).getLast h = f (head✝ :: tail✝)[tail✝.length]

Tactic:
simp only [map_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (f head✝ :: map f tail✝).getLast ⋯ = f (head✝ :: tail✝)[tail✝.length]

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
h : map f [] ≠ []
⊢ (map f []).getLast h = f ([].getLast ⋯)

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
h : map f l ≠ []
⊢ (map f l).getLast h = f (l.getLast ⋯)

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
f : α → β
h : map f [] ≠ []
⊢ (map f []).getLast h = f ([].getLast ⋯)

case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ (map f (head✝ :: tail✝)).getLast h = f ((head✝ :: tail✝).getLast ⋯)

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
head✝ : α
tail✝ : List α
h : map f (head✝ :: tail✝) ≠ []
⊢ f (head✝ :: tail✝)[(map f tail✝).length] = f (head✝ :: tail✝)[tail✝.length]

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.133064
β : Type ?u.133073
f : α → β
l : List α
h : map f l ≠ []
⊢ l ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem gcd_mul_addOrderOf_div_eq {n : ℕ} (m : ℕ) (hn : 0 < n) :
    m.gcd n * addOrderOf (↑(↑m / ↑n * p) : AddCircle p) = n

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul, IsOfFinAddOrder.addOrderOf_nsmul]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * (addOrderOf ↑(p / ↑n) / (addOrderOf ↑(p / ↑n)).gcd m) = n

case h
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * (addOrderOf ↑(p / ↑n) / (addOrderOf ↑(p / ↑n)).gcd m) = n

Tactic:
rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ n.gcd m ∣ n

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ n.gcd m ∣ n

Tactic:
exact n.gcd_dvd_left m

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)

Tactic:
rwa [← addOrderOf_pos_iff, addOrderOf_period_div hn]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean
theorem analyticAt_clog (m : z ∈ slitPlane) : AnalyticAt ℂ log z

Proof state:
case h
z : ℂ
m : z ∈ slitPlane
⊢ ∀ a ∈ slitPlane, DifferentiableAt ℂ log a

Tactic:
intro z m

Result:
case h
z✝ : ℂ
m✝ : z✝ ∈ slitPlane
z : ℂ
m : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z

Proof state:
z : ℂ
m : z ∈ slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z

Tactic:
filter_upwards [isOpen_slitPlane.eventually_mem m]

Result:
case h
z : ℂ
m : z ∈ slitPlane
⊢ ∀ a ∈ slitPlane, DifferentiableAt ℂ log a

Proof state:
case h
z✝ : ℂ
m✝ : z✝ ∈ slitPlane
z : ℂ
m : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z

Tactic:
exact differentiableAt_id.clog m

Result:
no goals

Proof state:
z : ℂ
m : z ∈ slitPlane
⊢ AnalyticAt ℂ log z

Tactic:
rw [analyticAt_iff_eventually_differentiableAt]

Result:
z : ℂ
m : z ∈ slitPlane
⊢ ∀ᶠ (z : ℂ) in 𝓝 z, DifferentiableAt ℂ log z
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_neg_one_X : rescale (-1 : A) X = -X

Proof state:
A : Type u_2
inst✝ : CommRing A
⊢ (rescale (-1)) X = -X

Tactic:
rw [rescale_X, map_neg, map_one, neg_one_mul]

Result:
no goals
-- Mathlib/FieldTheory/PolynomialGaloisGroup.lean
theorem mul_splits_in_splittingField_of_mul {p₁ q₁ p₂ q₂ : F[X]} (hq₁ : q₁ ≠ 0) (hq₂ : q₂ ≠ 0)
    (h₁ : p₁.Splits (algebraMap F q₁.SplittingField))
    (h₂ : p₂.Splits (algebraMap F q₂.SplittingField)) :
    (p₁ * p₂).Splits (algebraMap F (q₁ * q₂).SplittingField)

Proof state:
case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits ((↑(SplittingField.lift q₂ ⋯)).comp (algebraMap F q₂.SplittingField)) p₂

Tactic:
exact splits_comp_of_splits _ _ h₂

Result:
no goals

Proof state:
case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits (algebraMap F (q₁ * q₂).SplittingField) p₂

Tactic:
rw [←
  (SplittingField.lift q₂
      (splits_of_splits_of_dvd (algebraMap F (q₁ * q₂).SplittingField) (mul_ne_zero hq₁ hq₂)
        (SplittingField.splits _) (dvd_mul_left q₂ q₁))).comp_algebraMap]

Result:
case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits ((↑(SplittingField.lift q₂ ⋯)).comp (algebraMap F q₂.SplittingField)) p₂

Proof state:
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂)

Tactic:
apply splits_mul

Result:
case hf
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits (algebraMap F (q₁ * q₂).SplittingField) p₁

case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits (algebraMap F (q₁ * q₂).SplittingField) p₂

Proof state:
case hf
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits ((↑(SplittingField.lift q₁ ⋯)).comp (algebraMap F q₁.SplittingField)) p₁

Tactic:
exact splits_comp_of_splits _ _ h₁

Result:
no goals

Proof state:
case hf
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits (algebraMap F (q₁ * q₂).SplittingField) p₁

Tactic:
rw [←
  (SplittingField.lift q₁
      (splits_of_splits_of_dvd (algebraMap F (q₁ * q₂).SplittingField) (mul_ne_zero hq₁ hq₂)
        (SplittingField.splits _) (dvd_mul_right q₁ q₂))).comp_algebraMap]

Result:
case hf
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : Splits (algebraMap F q₁.SplittingField) p₁
h₂ : Splits (algebraMap F q₂.SplittingField) p₂
⊢ Splits ((↑(SplittingField.lift q₁ ⋯)).comp (algebraMap F q₁.SplittingField)) p₁
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_exp_div_rpow_atTop (s : ℝ) : Tendsto (fun x : ℝ => exp x / x ^ s) atTop atTop

Proof state:
case h.h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n

Tactic:
simpa using rpow_le_rpow_of_exponent_le hx₁ hn.le

Result:
no goals

Proof state:
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x => rexp x / x ^ n) ≤ᶠ[atTop] fun x => rexp x / x ^ s

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)] with x hx₀ hx₁

Result:
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ rexp x / x ^ n ≤ rexp x / x ^ s

Proof state:
case h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ rexp x / x ^ n ≤ rexp x / x ^ s

Tactic:
gcongr

Result:
case h.h
s : ℝ
n : ℕ
hn : s < ↑n
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n

Proof state:
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ Tendsto (fun x => rexp x / x ^ s) atTop atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ (tendsto_exp_div_pow_atTop n)

Result:
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ (fun x => rexp x / x ^ n) ≤ᶠ[atTop] fun x => rexp x / x ^ s

Proof state:
s : ℝ
⊢ Tendsto (fun x => rexp x / x ^ s) atTop atTop

Tactic:
obtain ⟨n, hn⟩ := archimedean_iff_nat_lt.1 Real.instArchimedean s

Result:
case intro
s : ℝ
n : ℕ
hn : s < ↑n
⊢ Tendsto (fun x => rexp x / x ^ s) atTop atTop
-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
theorem hasFDerivAt_norm_rpow (x : E) {p : ℝ} (hp : 1 < p) :
    HasFDerivAt (fun x : E ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • innerSL ℝ x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ Filter.Tendsto (fun x => ‖x‖ ^ (p - 1)) (𝓝 0) (𝓝 0)

Tactic:
convert continuousAt_id.norm.rpow_const (.inr h2p.le) |>.tendsto

Result:
case h.e'_1.h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ 0 = ‖id 0‖ ^ (p - 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : ¬x = 0
⊢ ‖x‖ ^ 2 ≠ 0 ∨ 1 ≤ p / 2

Tactic:
simp [hx]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ 1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_1.h.e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ 0 = ‖id 0‖ ^ (p - 1)

Tactic:
simp [h2p.ne']

Result:
no goals

Proof state:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) x

Tactic:
simp only [hx, norm_zero, map_zero, smul_zero]

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (fun x => ‖x‖ ^ p) 0 0
-- Mathlib/Topology/PartialHomeomorph.lean
theorem nhds_eq_comap_inf_principal {x} (hx : x ∈ e.source) :
    𝓝 x = comap e (𝓝 (e x)) ⊓ 𝓟 e.source

Proof state:
case intro
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ 𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source

Tactic:
rw [← e.open_source.nhdsWithin_eq x.2, ← map_nhds_subtype_val, ← map_comap_setCoe_val,
  e.toHomeomorphSourceTarget.nhds_eq_comap, nhds_subtype_eq_comap]

Result:
case intro
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (⇑e.toHomeomorphSourceTarget) (comap Subtype.val (𝓝 ↑(e.toHomeomorphSourceTarget x)))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))

Proof state:
case intro
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ map Subtype.val (comap (⇑e.toHomeomorphSourceTarget) (comap Subtype.val (𝓝 ↑(e.toHomeomorphSourceTarget x)))) =
    map Subtype.val (comap Subtype.val (comap (↑e) (𝓝 (↑e ↑x))))

Tactic:
simp only [Function.comp_def, toHomeomorphSourceTarget_apply_coe, comap_comap]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
hx : x ∈ e.source
⊢ 𝓝 x = comap (↑e) (𝓝 (↑e x)) ⊓ 𝓟 e.source

Tactic:
lift x to e.source using hx

Result:
case intro
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : { x // x ∈ e.source }
⊢ 𝓝 ↑x = comap (↑e) (𝓝 (↑e ↑x)) ⊓ 𝓟 e.source
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem unifTight_of_subsingleton [Subsingleton ι] (hp_top : p ≠ ∞)
    {f : ι → α → β} (hf : ∀ i, MemLp (f i) p μ) : UnifTight f p μ := fun ε hε ↦ by
  by_cases hε_top : ε = ∞
  · exact ⟨∅, by measurability, fun _ => hε_top.symm ▸ le_top⟩
  by_cases hι : Nonempty ι
  case neg => exact ⟨∅, (by measurability), fun i => False.elim <| hι <| Nonempty.intro i⟩
  obtain ⟨i⟩ := hι
  obtain ⟨s, _, hμs, hfε⟩ := (hf i).exists_eLpNorm_indicator_compl_lt hp_top (coe_ne_zero.2 hε.ne')
  refine ⟨s, ne_of_lt hμs, fun j => ?_⟩
  convert hfε.le

Proof state:
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
p : ℝ≥0∞
inst✝ : Subsingleton ι
hp_top : p ≠ ⊤
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ≥0
hε : 0 < ε
hε_top : ↑ε = ⊤
⊢ ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε

Tactic:
exact ⟨∅, by measurability, fun _ => hε_top.symm ▸ le_top⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem mul_left_index_le {K : Set G} (hK : IsCompact K) {V : Set G} (hV : (interior V).Nonempty)
    (g : G) : index ((fun h => g * h) '' K) V ≤ index K V

Proof state:
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K V
⊢ s.card ∈ Finset.card '' {t | (fun h => g * h) '' K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
rw [mem_image]

Result:
case intro.intro.hm
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K V
⊢ ∃ x ∈ {t | (fun h => g * h) '' K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}, x.card = s.card

Proof state:
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ (fun h => g * h) g₁ ∈ ⋃ g_1 ∈ Finset.map (Equiv.toEmbedding (Equiv.mulRight g⁻¹)) s, (fun h => g_1 * h) ⁻¹' V

Tactic:
simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight,
  exists_exists_and_eq_and, mem_preimage, Equiv.toEmbedding_apply]

Result:
case intro.intro.hm.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
V : Set G
hV : (interior V).Nonempty
g : G
s : Finset G
h1s : K ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K V
g₁ g₂ : G
hg₂ : g₂ ∈ s
hg₁ : g₂ * g₁ ∈ V
⊢ ∃ a ∈ s, a * g⁻¹ * (g * g₁) ∈ V
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem reduce_invRev {w : List (α × Bool)} : reduce (invRev w) = invRev (reduce w)

Proof state:
case H.h
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red w (invRev (reduce (invRev w)))

Tactic:
have : Red (invRev (invRev w)) (invRev (reduce (invRev w))) := reduce.red.invRev

Result:
case H.h
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))

Proof state:
case H.h
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))

Tactic:
rwa [invRev_invRev] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ reduce (invRev w) = invRev (reduce w)

Tactic:
apply reduce.min

Result:
case H
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (reduce (invRev w)) (invRev (reduce w))

Proof state:
case H
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)

Tactic:
apply Red.reduce_left

Result:
case H.h
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red w (invRev (reduce (invRev w)))

Proof state:
case H
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (reduce (invRev w)) (invRev (reduce w))

Tactic:
rw [← red_invRev_iff, invRev_invRev]

Result:
case H
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)
-- Mathlib/GroupTheory/Subgroup/Center.lean
theorem eq_of_left_mem_center {g h : M} (H : IsConj g h) (Hg : g ∈ Set.center M) : g = h

Proof state:
case intro
M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g = h

Tactic:
rwa [← u.mul_left_inj, Hg.comm u]

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Monoid M
g h : M
H : IsConj g h
Hg : g ∈ Set.center M
⊢ g = h

Tactic:
rcases H with ⟨u, hu⟩

Result:
case intro
M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g = h
-- Mathlib/Algebra/Order/Round.lean
theorem round_neg_two_inv : round (-2⁻¹ : α) = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
⊢ round (-2⁻¹) = 0

Tactic:
simp only [round_eq, ← one_div, neg_add_cancel, floor_zero]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem exists_most_significant_bit {n : ℕ} (h : n ≠ 0) :
    ∃ i, testBit n i = true ∧ ∀ j, i < j → testBit n j = false

Proof state:
case pos
b : Bool
n : ℕ
hn : n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
h : bit b n ≠ 0
h' : n = 0
⊢ ∃ i, (bit b n).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b n).testBit j = false

Tactic:
subst h'

Result:
case pos
b : Bool
hn : 0 ≠ 0 → ∃ i, testBit 0 i = true ∧ ∀ (j : ℕ), i < j → testBit 0 j = false
h : bit b 0 ≠ 0
⊢ ∃ i, (bit b 0).testBit i = true ∧ ∀ (j : ℕ), i < j → (bit b 0).testBit j = false