harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Monoid.lean
theorem Filter.tendsto_cocompact_mul_left {a b : M} (ha : b * a = 1) :
    Filter.Tendsto (fun x : M => a * x) (Filter.cocompact M) (Filter.cocompact M)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x => a * x) (cocompact M) (cocompact M)

Tactic:
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_left b))

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)

Proof state:
case h.e'_3.h
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
x : M
⊢ ((fun b_1 => b * b_1) ∘ fun x => a * x) x = id x

Tactic:
simp [← mul_assoc, ha]

Result:
no goals

Proof state:
case h.e'_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ ((fun b_1 => b * b_1) ∘ fun x => a * x) = id

Tactic:
ext x

Result:
case h.e'_3.h
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
x : M
⊢ ((fun b_1 => b * b_1) ∘ fun x => a * x) x = id x

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto ((fun b_1 => b * b_1) ∘ fun x => a * x) (cocompact M) (cocompact M)

Tactic:
convert Filter.tendsto_id

Result:
case h.e'_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : b * a = 1
⊢ ((fun b_1 => b * b_1) ∘ fun x => a * x) = id
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem exists_frequently_lt_of_liminf_ne_top' {ι : Type*} {l : Filter ι} {x : ι → ℝ}
    (hx : liminf (fun n => (Real.nnabs (x n) : ℝ≥0∞)) l ≠ ∞) : ∃ R, ∃ᶠ n in l, R < x n

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
r : ℝ≥0
⊢ IsCobounded (fun x1 x2 => x1 ≥ x2) (map (fun n => ↑(Real.nnabs (x n))) l)

Tactic:
isBoundedDefault

Result:
no goals

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)

Tactic:
filter_upwards [h (-r)] with i hi using(le_neg.1 hi).trans (neg_le_abs _)

Result:
no goals

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
⊢ False

Tactic:
refine hx (ENNReal.eq_top_of_forall_nnreal_le fun r => le_limsInf_of_le (by isBoundedDefault) ?_)

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun n => ↑(Real.nnabs (x n))) l, ↑r ≤ n

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
r : ℝ≥0
⊢ ∀ᶠ (n : ℝ≥0∞) in map (fun n => ↑(Real.nnabs (x n))) l, ↑r ≤ n

Tactic:
simp only [eventually_map, ENNReal.coe_le_coe]

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
⊢ ∃ R, ∃ᶠ (n : ι) in l, R < x n

Tactic:
by_contra h

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ¬∃ R, ∃ᶠ (n : ι) in l, R < x n
⊢ False

Proof state:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ¬∃ R, ∃ᶠ (n : ι) in l, R < x n
⊢ False

Tactic:
simp_rw [not_exists, not_frequently, not_lt] at h

Result:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤
h : ∀ (x_1 : ℝ), ∀ᶠ (x_2 : ι) in l, x x_2 ≤ x_1
⊢ False
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem eq_X_mul_shift_add_const (φ : R⟦X⟧) :
    φ = (X * mk fun p => coeff R (p + 1) φ) + C R (constantCoeff R φ)

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ = (X * mk fun p => (coeff R (p + 1)) φ) + (C R) ((constantCoeff R) φ)

Tactic:
ext (_ | n)

Result:
case h.zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) φ = (coeff R 0) ((X * mk fun p => (coeff R (p + 1)) φ) + (C R) ((constantCoeff R) φ))

case h.succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff R (n + 1)) φ = (coeff R (n + 1)) ((X * mk fun p => (coeff R (p + 1)) φ) + (C R) ((constantCoeff R) φ))

Proof state:
case h.zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) φ = (coeff R 0) ((X * mk fun p => (coeff R (p + 1)) φ) + (C R) ((constantCoeff R) φ))

Tactic:
simp only [coeff_zero_eq_constantCoeff, map_add, map_mul, constantCoeff_X,
  zero_mul, coeff_zero_C, zero_add]

Result:
no goals

Proof state:
case h.succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff R (n + 1)) φ = (coeff R (n + 1)) ((X * mk fun p => (coeff R (p + 1)) φ) + (C R) ((constantCoeff R) φ))

Tactic:
simp only [coeff_succ_X_mul, coeff_mk, LinearMap.map_add, coeff_C, n.succ_ne_zero, sub_zero,
  if_false, add_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem eq_rootMultiplicity_map {p : A[X]} {f : A →+* B} (hf : Function.Injective f) (a : A) :
    rootMultiplicity a p = rootMultiplicity (f a) (p.map f)

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity (f a) (map f p) ≤ rootMultiplicity a p

Tactic:
rw [le_rootMultiplicity_iff hp0, ← map_dvd_map f hf ((monic_X_sub_C a).pow _),
  Polynomial.map_pow, Polynomial.map_sub, map_X, map_C]

Result:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ (X - C (f a)) ^ rootMultiplicity (f a) (map f p) ∣ map f p

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Tactic:
apply le_antisymm (le_rootMultiplicity_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) a)

Result:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity (f a) (map f p) ≤ rootMultiplicity a p

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Tactic:
by_cases hp0 : p = 0

Result:
case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : p = 0
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : ¬p = 0
⊢ (X - C (f a)) ^ rootMultiplicity (f a) (map f p) ∣ map f p

Tactic:
apply pow_rootMultiplicity_dvd

Result:
no goals

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
a : A
hp0 : p = 0
⊢ rootMultiplicity a p = rootMultiplicity (f a) (map f p)

Tactic:
simp only [hp0, rootMultiplicity_zero, Polynomial.map_zero]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_restrictFreeVar [DecidableEq α] {n : ℕ} {φ : L.BoundedFormula α n}
    {f : φ.freeVarFinset → β} {v : β → M} {xs : Fin n → M}
    (v' : α → M) (hv' : ∀ a, v (f a) = v' a) :
    (φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs

Proof state:
case falsum
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f : { x // x ∈ falsum.freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ falsum.freeVarFinset }), v (f a) = v' ↑a
⊢ (falsum.restrictFreeVar f).Realize v xs ↔ falsum.Realize v' xs

Tactic:
rfl

Result:
no goals

Proof state:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : { x // x ∈ f✝.freeVarFinset }), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : { x // x ∈ (∀'f✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
⊢ ((∀'f✝).restrictFreeVar f).Realize v xs ↔ (∀'f✝).Realize v' xs

Tactic:
simp only [restrictFreeVar, Realize]

Result:
case all
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
n : ℕ
v : β → M
v' : α → M
n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 :
  ∀ {f : { x // x ∈ f✝.freeVarFinset } → β} {xs : Fin (n✝ + 1) → M},
    (∀ (a : { x // x ∈ f✝.freeVarFinset }), v (f a) = v' ↑a) → ((f✝.restrictFreeVar f).Realize v xs ↔ f✝.Realize v' xs)
f : { x // x ∈ (∀'f✝).freeVarFinset } → β
xs : Fin n✝ → M
hv' : ∀ (a : { x // x ∈ (∀'f✝).freeVarFinset }), v (f a) = v' ↑a
⊢ (∀ (x : M), (f✝.restrictFreeVar f).Realize v (snoc xs x)) ↔ ∀ (x : M), f✝.Realize v' (snoc xs x)
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem mapId_eq (Y : T) : map (𝟙 Y) = 𝟭 _

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Over Y
⊢ (map (𝟙 Y)).obj x = (𝟭 (Over Y)).obj x

Tactic:
dsimp [Over, Over.map, Comma.mapRight]

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Over Y
⊢ { left := x.left, right := x.right, hom := x.hom ≫ 𝟙 Y } = x

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Over Y
⊢ { left := x.left, right := x.right, hom := x.hom ≫ 𝟙 Y } = x

Tactic:
simp only [Category.comp_id]

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Over Y
⊢ { left := x.left, right := x.right, hom := x.hom } = x

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Over Y
u : x ⟶ y
⊢ (map (𝟙 Y)).map u = eqToHom ⋯ ≫ (𝟭 (Over Y)).map u ≫ eqToHom ⋯

Tactic:
dsimp [Over, Over.map, Comma.mapRight]

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Over Y
u : x ⟶ y
⊢ { left := u.left, right := 𝟙 x.right, w := ⋯ } = eqToHom ⋯ ≫ u ≫ eqToHom ⋯

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ autoParam (∀ (X Y_1 : Over Y) (f : X ⟶ Y_1), (map (𝟙 Y)).map f = eqToHom ⋯ ≫ (𝟭 (Over Y)).map f ≫ eqToHom ⋯) _auto✝

Tactic:
intros x y u

Result:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Over Y
u : x ⟶ y
⊢ (map (𝟙 Y)).map u = eqToHom ⋯ ≫ (𝟭 (Over Y)).map u ≫ eqToHom ⋯

Proof state:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x y : Over Y
u : x ⟶ y
⊢ { left := u.left, right := 𝟙 x.right, w := ⋯ } = eqToHom ⋯ ≫ u ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Over Y
⊢ { left := x.left, right := x.right, hom := x.hom } = x

Tactic:
exact rfl

Result:
no goals

Proof state:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ ∀ (X : Over Y), (map (𝟙 Y)).obj X = (𝟭 (Over Y)).obj X

Tactic:
intro x

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x : Over Y
⊢ (map (𝟙 Y)).obj x = (𝟭 (Over Y)).obj x

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ map (𝟙 Y) = 𝟭 (Over Y)

Tactic:
fapply Functor.ext

Result:
case h_obj
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ ∀ (X : Over Y), (map (𝟙 Y)).obj X = (𝟭 (Over Y)).obj X

case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
⊢ autoParam (∀ (X Y_1 : Over Y) (f : X ⟶ Y_1), (map (𝟙 Y)).map f = eqToHom ⋯ ≫ (𝟭 (Over Y)).map f ≫ eqToHom ⋯) _auto✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem abs_log_mul_self_rpow_lt (x t : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) (ht : 0 < t) :
    |log x * x ^ t| < 1 / t

Proof state:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1

Tactic:
rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this

Result:
no goals

Proof state:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| < 1 / t

Tactic:
rw [lt_div_iff₀ ht]

Result:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| * t < 1

Proof state:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ |log x * x ^ t| * t < 1

Tactic:
have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)

Result:
x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : |log (x ^ t) * x ^ t| < 1
⊢ |log x * x ^ t| * t < 1
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfc_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
f : ℝ≥0 → ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ cfc f a = cfc (fun x => ↑(f x.toNNReal)) a

Tactic:
replace ha : 0 ≤ a := ha

Result:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ cfc f a = cfc (fun x => ↑(f x.toNNReal)) a

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ cfc f a = cfc (fun x => ↑(f x.toNNReal)) a

Tactic:
apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict _
  isUniformEmbedding_subtype_val ha (.of_nonneg ha)

Result:
no goals
-- Mathlib/Data/Real/IsNonarchimedean.lean
theorem multiset_image_add {F α β : Type*} [AddCommGroup α] [FunLike F α ℝ]
    [AddGroupSeminormClass F α ℝ] [Nonempty β] {f : F} (hna : IsNonarchimedean f)
    (g : β → α) (s : Multiset β) :
    ∃ b : β, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ ‖(Multiset.map g s).sum‖ ≤ ‖g b‖

Tactic:
apply exists_norm_multiset_sum_le

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Tactic:
have := AddGroupSeminormClass.isUltrametricDist hna

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Tactic:
simp only [← AddGroupSeminormClass.toSeminormedAddCommGroup_norm_eq]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
this : IsUltrametricDist α
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ ‖(Multiset.map g s).sum‖ ≤ ‖g b‖

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)

Tactic:
let _ := AddGroupSeminormClass.toSeminormedAddCommGroup f

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : AddCommGroup α
inst✝² : FunLike F α ℝ
inst✝¹ : AddGroupSeminormClass F α ℝ
inst✝ : Nonempty β
f : F
hna : IsNonarchimedean ⇑f
g : β → α
s : Multiset β
x✝ : SeminormedAddCommGroup α := AddGroupSeminormClass.toSeminormedAddCommGroup f
⊢ ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem hasStrictDerivAt_sin (x : ℂ) : HasStrictDerivAt sin (cos x) x

Proof state:
x : ℂ
⊢ HasStrictDerivAt sin (cos x) x

Tactic:
simp only [cos, div_eq_mul_inv]

Result:
x : ℂ
⊢ HasStrictDerivAt sin ((cexp (x * I) + cexp (-x * I)) * 2⁻¹) x

Proof state:
case h.e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹

Tactic:
simp only [Function.comp, id]

Result:
case h.e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹

Proof state:
case h.e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹

Tactic:
rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
  I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]

Result:
no goals

Proof state:
x : ℂ
⊢ HasStrictDerivAt sin ((cexp (x * I) + cexp (-x * I)) * 2⁻¹) x

Tactic:
convert ((((hasStrictDerivAt_id x).neg.mul_const I).cexp.sub
  ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const I).mul_const (2 : ℂ)⁻¹ using 1

Result:
case h.e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem exists_ne_zero {f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) : ∃ x, f x ≠ 0

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
⊢ ∃ x, f x ≠ 0

Tactic:
by_contra! h

Result:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), f x = 0
⊢ False

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), f x = 0
⊢ False

Tactic:
exact hf (ContinuousLinearMap.ext h)

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
theorem abs_pow_sub_pow_le : |a ^ n - b ^ n| ≤ |a - b| * n * max |a| |b| ^ (n - 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |a ^ n - b ^ n| ≤ |a - b| * ↑n * (|a| ⊔ |b|) ^ (n - 1)

Tactic:
obtain _ | n := n

Result:
case zero
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * (|a| ⊔ |b|) ^ (0 - 1)

case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * (|a| ⊔ |b|) ^ (n + 1 - 1)

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * (|a| ⊔ |b|) ^ (n + 1 - 1)

Tactic:
rw [Nat.add_sub_cancel, pow_sub_pow_eq_sub_mul_geomSum, abs_mul, mul_assoc, Nat.cast_succ]

Result:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * ((↑n + 1) * (|a| ⊔ |b|) ^ n)

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ |a - b| * |geomSum a b n| ≤ |a - b| * ((↑n + 1) * (|a| ⊔ |b|) ^ n)

Tactic:
exact mul_le_mul_of_nonneg_left (abs_geomSum_le ..) (abs_nonneg _)

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * (|a| ⊔ |b|) ^ (0 - 1)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma YClass_ne_zero [Nontrivial R] (y : R[X]) : YClass W y ≠ 0 :=
  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (X_sub_C_ne_zero y) <|
    by rw [natDegree_polynomial, natDegree_X_sub_C]; norm_num1

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ (Y - C y).natDegree < W.polynomial.natDegree

Tactic:
rw [natDegree_polynomial, natDegree_X_sub_C]

Result:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ 1 < 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
y : R[X]
⊢ 1 < 2

Tactic:
norm_num1

Result:
no goals
-- Mathlib/Analysis/AbsoluteValue/Equivalence.lean
/-- Equivalence of absolute values is transitive. -/
lemma isEquiv_trans {f g k : AbsoluteValue R ℝ} (hfg : IsEquiv f g) (hgk : IsEquiv g k) :
    IsEquiv f k

Proof state:
case intro.intro
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
hgk : g.IsEquiv k
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
⊢ f.IsEquiv k

Tactic:
rcases hgk with ⟨d, hdPos, hgk⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ f.IsEquiv k

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ (fun x => f x ^ (c * d)) = ⇑k

Tactic:
simp [← hgk, ← hfg, Real.rpow_mul (apply_nonneg f _)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
hfg : f.IsEquiv g
hgk : g.IsEquiv k
⊢ f.IsEquiv k

Tactic:
rcases hfg with ⟨c, hcPos, hfg⟩

Result:
case intro.intro
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
hgk : g.IsEquiv k
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
⊢ f.IsEquiv k

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ f.IsEquiv k

Tactic:
refine ⟨c * d, mul_pos hcPos hdPos, ?_⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g k : AbsoluteValue R ℝ
c : ℝ
hcPos : 0 < c
hfg : (fun x => f x ^ c) = ⇑g
d : ℝ
hdPos : 0 < d
hgk : (fun x => g x ^ d) = ⇑k
⊢ (fun x => f x ^ (c * d)) = ⇑k