harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem exists_primeSpectrum_prod_le (I : Ideal R) :
    ∃ Z : Multiset (PrimeSpectrum R), Multiset.prod (Z.map asIdeal) ≤ I

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + span R {z}
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ span R {x} * (M + span R {y}) ≤ M

Tactic:
rw [mul_add]

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + span R {z}
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ span R {x} * M + span R {x} * span R {y} ≤ M

Proof state:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + span R {z}
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ (M + span R {x}) * (M + span R {y}) ≤ M

Tactic:
rw [add_mul]

Result:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I M : Ideal R
hgt : ∀ J > M, (fun I => ∃ Z, (Multiset.map asIdeal Z).prod ≤ I) J
h_prM : ¬M.IsPrime
htop : ¬M = ⊤
lt_add : ∀ z ∉ M, M < M + span R {z}
x : R
hx : x ∉ M
y : R
hy : y ∉ M
hxy : x * y ∈ M
Wx : Multiset (PrimeSpectrum R)
h_Wx : (Multiset.map asIdeal Wx).prod ≤ M + span R {x}
Wy : Multiset (PrimeSpectrum R)
h_Wy : (Multiset.map asIdeal Wy).prod ≤ M + span R {y}
⊢ M * (M + span R {y}) + span R {x} * (M + span R {y}) ≤ M
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma isBigO_atTop_F_int_zero_sub (a : UnitAddCircle) : ∃ p, 0 < p ∧
    (fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =O[atTop] fun t ↦ exp (-p * t)

Proof state:
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
⊢ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
t : ℝ
ht : 0 < t
⊢ (F_int 0 (↑a) t - if a = 0 then 1 else 0) = (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Tactic:
simp_rw [eq_false_intro (by linarith [ha.2] : 1 - a ≠ 0), if_false, sub_zero] at hq'

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
⊢ ∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)

Proof state:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
⊢ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-(p ⊓ q) * t)

Tactic:
have : (fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =ᶠ[atTop]
    fun t ↦ (F_nat 0 a t - (if a = 0 then 1 else 0)) + F_nat 0 (1 - a) t := by
  filter_upwards [eventually_gt_atTop 0] with t ht
  rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]
  ring

Result:
case intro.intro.intro.intro.intro.intro
a : ℝ
ha : a ∈ Ico 0 1
p : ℝ
hp : 0 < p
hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
q : ℝ
hq : 0 < q
hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)
this :
  (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t =>
    (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t
⊢ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-(p ⊓ q) * t)
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem lcm_dvd {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) : lcm x y ∣ z

Proof state:
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
r : R
hr : x = gcd x y * r
s p g : R
hxy : ¬g = 0
hs : y = g * s
hp : z * g = x * y * p
⊢ z = x * y / g * p

Tactic:
subst hs

Result:
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ z = x * (g * s) / g * p

Proof state:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z

Tactic:
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩

Result:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y / gcd x y ∣ z

Proof state:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
⊢ 0 ∣ z

Tactic:
rwa [hxy.1] at hxz

Result:
no goals

Proof state:
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * g * s * p = x * s * p * g

Tactic:
simp only [mul_right_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
lemma measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet [SFinite μ]
    (ht_subset : t ⊆ μ.sigmaFiniteSetᶜ) :
    μ t = 0 ∨ μ t = ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst✝ : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ ¬μ t = 0 → μ t = ⊤

Tactic:
exact measure_eq_top_of_subset_compl_sigmaFiniteSetWRT ht_subset

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst✝ : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ μ t = 0 ∨ μ t = ⊤

Tactic:
rw [or_iff_not_imp_left]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst✝ : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ ¬μ t = 0 → μ t = ⊤
-- Mathlib/Data/Set/Insert.lean
theorem subset_insert_iff {s t : Set α} {x : α} :
    s ⊆ insert x t ↔ s ⊆ t ∨ (x ∈ s ∧ s \ {x} ⊆ t)

Proof state:
case pos
α : Type u
s t : Set α
x : α
hx : x ∈ s
⊢ s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

Tactic:
rw [and_iff_right hx, or_iff_right_of_imp diff_subset.trans]

Result:
no goals

Proof state:
α : Type u
s t : Set α
x : α
⊢ s ⊆ insert x t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

Tactic:
rw [← diff_singleton_subset_iff]

Result:
α : Type u
s t : Set α
x : α
⊢ s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

Proof state:
case neg
α : Type u
s t : Set α
x : α
hx : x ∉ s
⊢ s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

Tactic:
rw [diff_singleton_eq_self hx, or_iff_left_of_imp And.right]

Result:
no goals

Proof state:
α : Type u
s t : Set α
x : α
⊢ s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u
s t : Set α
x : α
hx : x ∈ s
⊢ s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t

case neg
α : Type u
s t : Set α
x : α
hx : x ∉ s
⊢ s \ {x} ⊆ t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t
-- Mathlib/LinearAlgebra/Prod.lean
theorem ker_prod_ker_le_ker_coprod {M₂ : Type*} [AddCommMonoid M₂] [Module R M₂] {M₃ : Type*}
    [AddCommMonoid M₃] [Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) :
    (ker f).prod (ker g) ≤ ker (f.coprod g)

Proof state:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
⊢ (ker f).prod (ker g) ≤ ker (f.coprod g)

Tactic:
rintro ⟨y, z⟩

Result:
case mk
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
y : M
z : M₂
⊢ (y, z) ∈ (ker f).prod (ker g) → (y, z) ∈ ker (f.coprod g)

Proof state:
case mk
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
y : M
z : M₂
⊢ (y, z) ∈ (ker f).prod (ker g) → (y, z) ∈ ker (f.coprod g)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Bernstein.lean
theorem iterate_derivative_at_1 (n ν : ℕ) (h : ν ≤ n) :
    (Polynomial.derivative^[n - ν] (bernsteinPolynomial R n ν)).eval 1 =
      (-1) ^ (n - ν) * (ascPochhammer R (n - ν)).eval (ν + 1 : R)

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((⇑derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Tactic:
rw [flip' _ _ _ h]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((⇑derivative)^[n - ν] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (ascPochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Tactic:
norm_cast

Result:
case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(Int.negSucc 0 ^ (n - ν)) * ↑(eval (n - (n - ν - 1)) (ascPochhammer ℕ (n - ν))) =
    ↑(Int.negSucc 0 ^ (n - ν)) * ↑(eval (ν + 1) (ascPochhammer ℕ (n - ν)))

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((⇑derivative)^[n - ν] ((bernsteinPolynomial R n (n - ν)).comp (1 - X))) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Tactic:
simp [Polynomial.eval_comp, h]

Result:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (ascPochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ ↑(Int.negSucc 0 ^ (n - ν)) * ↑(eval (n - (n - ν - 1)) (ascPochhammer ℕ (n - ν))) =
    ↑(Int.negSucc 0 ^ (n - ν)) * ↑(eval (ν + 1) (ascPochhammer ℕ (n - ν)))

Tactic:
congr

Result:
case inr.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ n - (n - ν - 1) = ν + 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (ascPochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Tactic:
obtain rfl | h' := h.eq_or_lt

Result:
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
h : ν ≤ ν
⊢ (-1) ^ (ν - ν) * eval (↑(ν - (ν - ν - 1))) (ascPochhammer R (ν - ν)) =
    (-1) ^ (ν - ν) * eval (↑ν + 1) (ascPochhammer R (ν - ν))

case inr
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ (-1) ^ (n - ν) * eval (↑(n - (n - ν - 1))) (ascPochhammer R (n - ν)) =
    (-1) ^ (n - ν) * eval (↑ν + 1) (ascPochhammer R (n - ν))

Proof state:
case inl
R : Type u_1
inst✝ : CommRing R
ν : ℕ
h : ν ≤ ν
⊢ (-1) ^ (ν - ν) * eval (↑(ν - (ν - ν - 1))) (ascPochhammer R (ν - ν)) =
    (-1) ^ (ν - ν) * eval (↑ν + 1) (ascPochhammer R (ν - ν))

Tactic:
simp

Result:
no goals

Proof state:
case inr.e_a.e_a.e_a
R : Type u_1
inst✝ : CommRing R
n ν : ℕ
h : ν ≤ n
h' : ν < n
⊢ n - (n - ν - 1) = ν + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extChartAt_symm_nhdsWithin' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    map (extChartAt I x).symm (𝓝[(extChartAt I x).symm ⁻¹' s ∩ range I] extChartAt I x y) =
      𝓝[s] y :=
  map_extend_symm_nhdsWithin _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x y : M
hy : y ∈ (extChartAt I x).source
⊢ y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_nhds' (hff' : ∀ᶠ x in 𝓝[≠] a, HasDerivAt f (f' x) x)
    (hgg' : ∀ᶠ x in 𝓝[≠] a, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in 𝓝[≠] a, g' x ≠ 0)
    (hfa : Tendsto f (𝓝[≠] a) (𝓝 0)) (hga : Tendsto g (𝓝[≠] a) (𝓝 0))
    (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[≠] a) l) :
    Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Proof state:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0
hfa : Tendsto f (𝓝[≠] a) (𝓝 0)
hga : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[≠] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Tactic:
simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *

Result:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l ∧ Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l ∧ Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
exact ⟨lhopital_zero_nhds_left hff'.1 hgg'.1 hg'.1 hfa.1 hga.1 hdiv.1,
  lhopital_zero_nhds_right hff'.2 hgg'.2 hg'.2 hfa.2 hga.2 hdiv.2⟩

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' {k n : ℕ} [hp : Fact p.Prime] :
    (p - 1) * padicValNat p (choose (n + k) k) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ k ≤ n + k

Tactic:
exact Nat.le_add_left k n

Result:
no goals

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
simp only [sub_one_mul_padicValNat_factorial]

Result:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
simp only [Nat.choose_eq_factorial_div_factorial h]

Result:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
have h : k ≤ n + k := by exact Nat.le_add_left k n

Result:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k - (p.digits k).sum + (n + k - k - (p.digits (n + k - k)).sum)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
rw [← Nat.sub_add_comm <| digit_sum_le p k, Nat.add_sub_cancel n k, ← Nat.add_sub_assoc <|
    digit_sum_le p n, Nat.sub_sub (k + n), ← Nat.sub_right_comm, Nat.sub_sub, sub_add_eq,
    add_comm, tsub_tsub_assoc (Nat.le_refl (k + n)) <| (add_comm k n) ▸ (Nat.add_le_add
    (digit_sum_le p n) (digit_sum_le p k)), Nat.sub_self (k + n), zero_add, add_comm]

Result:
no goals

Proof state:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p ((n + k)! / (k ! * (n + k - k)!)) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
rw [padicValNat.div_of_dvd <| factorial_mul_factorial_dvd_factorial h, Nat.mul_sub_left_distrib,
    padicValNat.mul (factorial_ne_zero _) (factorial_ne_zero _), Nat.mul_add]

Result:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ (p - 1) * padicValNat p (n + k)! - ((p - 1) * padicValNat p k ! + (p - 1) * padicValNat p (n + k - k)!) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem IsPullback.of_map_of_faithful [ReflectsLimit (cospan h i) F] [F.Faithful]
    (H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) : IsPullback f g h i :=
  H.of_map F (F.map_injective <| by simpa only [F.map_comp] using H.w)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsLimit (cospan h i) F
inst✝ : F.Faithful
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
simpa only [F.map_comp] using H.w

Result:
no goals
-- Mathlib/Analysis/NormedSpace/RCLike.lean
theorem norm_smul_inv_norm {x : E} (hx : x ≠ 0) : ‖(‖x‖⁻¹ : 𝕜) • x‖ = 1

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1

Tactic:
field_simp [norm_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
simp [hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem iterated_mateEquiv_conjugateEquiv_symm (α : TwoSquare U₂ R₂ R₁ U₁) :
    (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
      (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans
        (equivNatTrans _ _ _ _).symm α

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare U₂ R₂ R₁ U₁
⊢ (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm) α

Tactic:
ext

Result:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare U₂ R₂ R₁ U₁
X✝ : A
⊢ ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α)).natTrans.app X✝ =
    (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm) α).natTrans.app X✝

Proof state:
case h
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare U₂ R₂ R₁ U₁
X✝ : A
⊢ ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α)).natTrans.app X✝ =
    (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm) α).natTrans.app X✝

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
@[simp]
lemma ofHoms_homFamily (P : MorphismProperty C) : ofHoms P.homFamily = P

Proof state:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ i, Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f

Tactic:
obtain ⟨⟨f, hf⟩, ⟨_, _⟩⟩ := hf

Result:
case h.mp.intro.mk.refl
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
f : Arrow C
hf : f ∈ P.toSet
⊢ P (P.homFamily ⟨f, hf⟩)

Proof state:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f → P f

Tactic:
intro hf

Result:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ofHoms P.homFamily f
⊢ P f

Proof state:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ P f → ofHoms P.homFamily f

Tactic:
intro hf

Result:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : P f
⊢ ofHoms P.homFamily f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ ofHoms P.homFamily = P

Tactic:
ext _ _ f

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f ↔ P f

Proof state:
case h.mp.intro.mk.refl
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
f : Arrow C
hf : f ∈ P.toSet
⊢ P (P.homFamily ⟨f, hf⟩)

Tactic:
exact hf

Result:
no goals

Proof state:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ofHoms P.homFamily f
⊢ P f

Tactic:
rw [ofHoms_iff] at hf

Result:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ i, Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f

Proof state:
case h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : P f
⊢ ofHoms P.homFamily f

Tactic:
exact ⟨(⟨f, hf⟩ : P.toSet)⟩

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f ↔ P f

Tactic:
constructor

Result:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ofHoms P.homFamily f → P f

case h.mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ P f → ofHoms P.homFamily f