harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Deriv.lean
/-- The abscissa of absolute convergence of the point-wise product of `log` and `f`
is the same as that of `f`. -/
@[simp]
lemma LSeries.abscissaOfAbsConv_logMul {f : ℕ → ℂ} :
    abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f

Proof state:
case h
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖f n / ↑n ^ ↑s‖ ≤ ‖Real.log ↑n‖ * ‖f n / ↑n ^ ↑s‖

Tactic:
refine le_mul_of_one_le_left (norm_nonneg _) (.trans ?_ <| Real.le_norm_self _)

Result:
case h
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ 1 ≤ Real.log ↑n

Proof state:
case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < ↑s
⊢ LSeriesSummable (logMul f) ↑s

Tactic:
exact LSeriesSummable_logMul_of_lt_re <| by simp [hs]

Result:
no goals

Proof state:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < ↑s
⊢ abscissaOfAbsConv f < ↑(↑s).re

Tactic:
simp [hs]

Result:
no goals

Proof state:
case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖term f (↑s) i‖ ≤ (fun x => ‖term (logMul f) (↑s) x‖) i

Tactic:
filter_upwards [Filter.eventually_ge_atTop <| max 1 (Nat.ceil (Real.exp 1))] with n hn

Result:
case h
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖term f (↑s) n‖ ≤ ‖term (logMul f) (↑s) n‖

Proof state:
case h
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖term f (↑s) n‖ ≤ ‖term (logMul f) (↑s) n‖

Tactic:
simp only [term_of_ne_zero (show n ≠ 0 by omega), logMul, norm_mul, mul_div_assoc,
  ← natCast_log, norm_real]

Result:
case h
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ ‖f n / ↑n ^ ↑s‖ ≤ ‖Real.log ↑n‖ * ‖f n / ↑n ^ ↑s‖

Proof state:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ abscissaOfAbsConv (logMul f) < ↑(↑s).re

Tactic:
simp [hs]

Result:
no goals

Proof state:
case h
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ 1 ≤ Real.log ↑n

Tactic:
simpa using Real.log_le_log (Real.exp_pos 1) <| Nat.ceil_le.mp <| (le_max_right _ _).trans hn

Result:
no goals

Proof state:
f : ℕ → ℂ
⊢ abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f

Tactic:
apply le_antisymm <;> refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' fun s hs ↦ ?_

Result:
case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv f < ↑s
⊢ LSeriesSummable (logMul f) ↑s

case a
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
⊢ LSeriesSummable f ↑s

Proof state:
f : ℕ → ℂ
s : ℝ
hs : abscissaOfAbsConv (logMul f) < ↑s
n : ℕ
hn : 1 ⊔ ⌈Real.exp 1⌉₊ ≤ n
⊢ n ≠ 0

Tactic:
omega

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_self : a ⇔ a = ⊤

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a : α
⊢ a ⇔ a = ⊤

Tactic:
rw [bihimp, inf_idem, himp_self]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- If `p` is a prime and `n` is `s`-factored, then every product `p^e * n`
is `s ∪ {p}`-factored. -/
lemma pow_mul_mem_factoredNumbers {s : Finset ℕ} {p n : ℕ} (hp : p.Prime) (e : ℕ)
    (hn : n ∈ factoredNumbers s) :
    p ^ e * n ∈ factoredNumbers (insert p s)

Proof state:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Tactic:
have hp' := pow_ne_zero e hp.ne_zero

Result:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Proof state:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q ∈ insert p s

Tactic:
rw [mem_primeFactorsList hp'] at H

Result:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q ∈ insert p s

Proof state:
case inr
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q ∈ insert p s

Tactic:
exact Finset.mem_insert_of_mem <| hn.2 _ H

Result:
no goals

Proof state:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q ∈ insert p s

Tactic:
rcases (mem_primeFactorsList_mul hp' hn.1).mp hq with H | H

Result:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ (p ^ e).primeFactorsList
⊢ q ∈ insert p s

case inr
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : q ∈ n.primeFactorsList
⊢ q ∈ insert p s

Proof state:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ p ∈ insert p s

Tactic:
exact Finset.mem_insert_self p s

Result:
no goals

Proof state:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q ∈ insert p s

Tactic:
rw [(prime_dvd_prime_iff_eq H.1 hp).mp <| H.1.dvd_of_dvd_pow H.2]

Result:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ p ∈ insert p s

Proof state:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
⊢ p ^ e * n ∈ factoredNumbers (insert p s)

Tactic:
refine ⟨mul_ne_zero hp' hn.1, fun q hq ↦ ?_⟩

Result:
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
⊢ q ∈ insert p s
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem functorPushforward_comp (R : Sieve X) :
    R.functorPushforward (F ⋙ G) = (R.functorPushforward F).functorPushforward G

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ : E
f✝ : Y✝ ⟶ (F ⋙ G).obj X
⊢ (functorPushforward (F ⋙ G) R).arrows f✝ ↔ (functorPushforward G (functorPushforward F R)).arrows f✝

Tactic:
simp [R.arrows.functorPushforward_comp F G]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)

Tactic:
ext

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ : E
f✝ : Y✝ ⟶ (F ⋙ G).obj X
⊢ (functorPushforward (F ⋙ G) R).arrows f✝ ↔ (functorPushforward G (functorPushforward F R)).arrows f✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
    (eraseKey k l).isEmpty = (l.isEmpty || (l.length == 1 && containsKey k l))

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).isEmpty = true ↔ l.isEmpty = true ∨ l.length = 1 ∧ containsKey k l = true

Tactic:
rw [List.isEmpty_iff_length_eq_zero, length_eraseKey, List.isEmpty_iff_length_eq_zero]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (if containsKey k l = true then l.length - 1 else l.length) = 0 ↔ l.length = 0 ∨ l.length = 1 ∧ containsKey k l = true

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).isEmpty = true ↔ (l.isEmpty || l.length == 1 && containsKey k l) = true

Tactic:
simp only [Bool.or_eq_true, Bool.and_eq_true, beq_iff_eq]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).isEmpty = true ↔ l.isEmpty = true ∨ l.length = 1 ∧ containsKey k l = true

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).isEmpty = (l.isEmpty || l.length == 1 && containsKey k l)

Tactic:
rw [Bool.eq_iff_iff]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (eraseKey k l).isEmpty = true ↔ (l.isEmpty || l.length == 1 && containsKey k l) = true

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ (if containsKey k l = true then l.length - 1 else l.length) = 0 ↔ l.length = 0 ∨ l.length = 1 ∧ containsKey k l = true

Tactic:
cases containsKey k l <;> cases l <;> simp

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem IsTorsion.not_torsion_free [hN : Nontrivial G] : IsTorsion G → ¬IsTorsionFree G := fun tG =>
  not_isTorsionFree_iff.mpr <| by
    obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN
    exact ⟨x, hx, tG x⟩

Proof state:
case intro
G : Type u_1
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
x : G
hx : x ≠ 1
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g

Tactic:
exact ⟨x, hx, tG x⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g

Tactic:
obtain ⟨x, hx⟩ := (nontrivial_iff_exists_ne (1 : G)).mp hN

Result:
case intro
G : Type u_1
inst✝ : Group G
hN : Nontrivial G
tG : IsTorsion G
x : G
hx : x ≠ 1
⊢ ∃ g, g ≠ 1 ∧ IsOfFinOrder g
-- Mathlib/Order/Filter/Prod.lean
theorem map_fst_prod (f : Filter α) (g : Filter β) [NeBot g] : map Prod.fst (f ×ˢ g) = f

Proof state:
case h
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : g.NeBot
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f

Tactic:
simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
  exists_mem_subset_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map Prod.fst (f ×ˢ g) = f

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
inst✝ : g.NeBot
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
-- Mathlib/RingTheory/LaurentSeries.lean
theorem inducing_coe : IsUniformInducing ((↑) : RatFunc K → K⸨X⸩)

Proof state:
case h.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ Valued.v (↑x✝¹.2 - ↑x✝¹.1) < ↑d

Tactic:
erw [← RatFunc.coe_sub, ← valuation_eq_LaurentSeries_valuation]

Result:
case h.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ (valuation (RatFunc K) (idealX K)) (x✝¹.2 - x✝¹.1) < ↑d

Proof state:
case h.a
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x => (↑x.1, ↑x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x => x.2 - x.1) ⁻¹' R ⊆ T
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ R
x✝¹ : RatFunc K × RatFunc K
x✝ : x✝¹ ∈ (fun x => x.2 - x.1) ⁻¹' {P | Valued.v P < ↑d}
⊢ (valuation (RatFunc K) (idealX K)) (x✝¹.2 - x✝¹.1) < ↑d

Tactic:
assumption

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
⊢ ∃ t, (∃ t_1 ∈ nhds 0, (fun x => x.2 - x.1) ⁻¹' t_1 ⊆ t) ∧ (fun x => (↑x.1, ↑x.2)) ⁻¹' t ⊆ S

Tactic:
refine ⟨(fun x : K⸨X⸩ × K⸨X⸩ ↦ x.snd - x.fst) ⁻¹' X, ⟨X, ?_⟩, ?_⟩

Result:
case h.mpr.intro.intro.intro.refine_1
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
⊢ X ∈ nhds 0 ∧ (fun x => x.2 - x.1) ⁻¹' X ⊆ (fun x => x.2 - x.1) ⁻¹' X

case h.mpr.intro.intro.intro.refine_2
K : Type u_2
inst✝ : Field K
S : Set (RatFunc K × RatFunc K)
w✝ : Set (RatFunc K)
hT : w✝ ∈ nhds 0
pre_T : (fun x => x.2 - x.1) ⁻¹' w✝ ⊆ S
d : (WithZero (Multiplicative ℤ))ˣ
hd : {y | Valued.v (y - 0) < ↑d} ⊆ w✝
X : Set K⸨X⸩ := {f | Valued.v f < ↑d}
⊢ (fun x => (↑x.1, ↑x.2)) ⁻¹' ((fun x => x.2 - x.1) ⁻¹' X) ⊆ S
-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
theorem WfDvdMonoid.max_power_factor' [CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α}
    (h : a₀ ≠ 0) (hx : ¬IsUnit x) : ∃ (n : ℕ) (a : α), ¬x ∣ a ∧ a₀ = x ^ n * a

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ False

Tactic:
exact hm d ⟨n + 1, by rw [pow_succ, mul_assoc]⟩
  ⟨(right_ne_zero_of_mul <| right_ne_zero_of_mul h), x, hx, mul_comm _ _⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ¬x ∣ a

Tactic:
rintro ⟨d, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ False

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a

Tactic:
obtain ⟨a, ⟨n, rfl⟩, hm⟩ := wellFounded_dvdNotUnit.has_min
  {a | ∃ n, x ^ n * a = a₀} ⟨a₀, 0, by rw [pow_zero, one_mul]⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ∃ n_1 a_1, ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
n : ℕ
d : α
h : x ^ n * (x * d) ≠ 0
hm : ∀ x_1 ∈ {a | ∃ n_1, x ^ n_1 * a = x ^ n * (x * d)}, ¬DvdNotUnit x_1 (x * d)
⊢ x ^ (n + 1) * d = x ^ n * (x * d)

Tactic:
rw [pow_succ, mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a₀ x : α
h : a₀ ≠ 0
hx : ¬IsUnit x
⊢ x ^ 0 * a₀ = a₀

Tactic:
rw [pow_zero, one_mul]

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ∃ n_1 a_1, ¬x ∣ a_1 ∧ x ^ n * a = x ^ n_1 * a_1

Tactic:
refine ⟨n, a, ?_, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
x : α
hx : ¬IsUnit x
a : α
n : ℕ
h : x ^ n * a ≠ 0
hm : ∀ x_1 ∈ {a_1 | ∃ n_1, x ^ n_1 * a_1 = x ^ n * a}, ¬DvdNotUnit x_1 a
⊢ ¬x ∣ a
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
lemma log_exp (a : A) (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc (fun x => Real.log (Real.exp x)) a = a

Tactic:
simp [cfc_id' (R := ℝ) a]

Result:
no goals

Proof state:
case funProp.discharger
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ ∀ x ∈ Real.exp '' spectrum ℝ a, x ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ log (exp ℝ a) = a

Tactic:
rw [log, ← real_exp_eq_normedSpace_exp, ← cfc_comp' Real.log Real.exp a hcont]

Result:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc (fun x => Real.log (Real.exp x)) a = a

Proof state:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ ContinuousOn Real.log (Real.exp '' spectrum ℝ a)

Tactic:
fun_prop (disch := simp)

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ log (exp ℝ a) = a

Tactic:
have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := simp)

Result:
A : Type u_1
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : CompleteSpace A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ log (exp ℝ a) = a
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblY_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblY P = P y ^ 4

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblY P = P y ^ 4

Tactic:
rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblX_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -P y ^ 4 - W'.a₁ * 0 - W'.a₃ * 0 = P y ^ 4

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -P y ^ 4 - W'.a₁ * 0 - W'.a₃ * 0 = P y ^ 4

Tactic:
ring1

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@[simp]
lemma mapObj_refl {j : J} (iter : Φ.Iteration j)
    {k l : J} (h : k ≤ l) (h' : l ≤ j) :
    mapObj iter iter h (h.trans h') h' (by rfl) = iter.F.map (homOfLE h)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
k l : J
h : k ≤ l
h' : l ≤ j
⊢ iter.mapObj iter h ⋯ h' ⋯ = iter.F.map (homOfLE h)

Tactic:
simp [mapObj]

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
iter : Φ.Iteration j
k l : J
h : k ≤ l
h' : l ≤ j
⊢ j ≤ j

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_four [CommMonoid β] (f : Fin 4 → β) : ∏ i, f i = f 0 * f 1 * f 2 * f 3

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 4 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3

Tactic:
rfl

Result:
no goals

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 4 → β
⊢ ∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3

Tactic:
rw [prod_univ_castSucc, prod_univ_three]

Result:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 4 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (last 3) = f 0 * f 1 * f 2 * f 3
-- Mathlib/Data/Set/Image.lean
theorem image_singleton {f : α → β} {a : α} : f '' {a} = {f a}

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
a : α
x✝ : β
⊢ x✝ ∈ f '' {a} ↔ x✝ ∈ {f a}

Tactic:
simp [image, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ f '' {a} = {f a}

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
a : α
x✝ : β
⊢ x✝ ∈ f '' {a} ↔ x✝ ∈ {f a}
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiff.analyticOnNhd (h : ContDiff 𝕜 ω f) : AnalyticOnNhd 𝕜 f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOnNhd 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
exact this.mono (subset_univ _)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
have := h.analyticOn

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOn 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOn 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
rw [analyticOn_univ] at this

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
this : AnalyticOnNhd 𝕜 f univ
⊢ AnalyticOnNhd 𝕜 f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiff 𝕜 ω f
⊢ AnalyticOnNhd 𝕜 f s

Tactic:
rw [← contDiffOn_univ] at h

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
h : ContDiffOn 𝕜 ω f univ
⊢ AnalyticOnNhd 𝕜 f s
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_preimage (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) (s : Set Y) :
    μH[d] (f ⁻¹' s) = μH[d] (s ∩ range f)

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
⊢ μH[d] (f ⁻¹' s) = μH[d] (s ∩ range f)

Tactic:
rw [← hf.hausdorffMeasure_image hd, image_preimage_eq_inter_range]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
theorem toSphere_apply' {s : Set (sphere (0 : E) 1)} (hs : MeasurableSet s) :
    μ.toSphere s = dim E * μ (Ioo (0 : ℝ) 1 • ((↑) '' s))

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
μ : Measure E
inst✝ : BorelSpace E
s : Set ↑(sphere 0 1)
hs : MeasurableSet s
⊢ μ.toSphere s = ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s)

Tactic:
rw [toSphere, smul_apply, fst_apply hs, restrict_apply (measurable_fst hs),
  ((MeasurableEmbedding.subtype_coe (measurableSet_singleton _).compl).comp
    (Homeomorph.measurableEmbedding _)).comap_apply,
  image_comp, Homeomorph.image_symm, univ_prod, ← Set.prod_eq, nsmul_eq_mul, toSphere_apply_aux]

Result:
no goals