harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem hasMFDerivAt_snd (x : M × M') :
    HasMFDerivAt (I.prod I') I' Prod.snd x
      (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x : M × M'
this :
  ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x,
    (↑(extChartAt I' x.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod I') x).symm) y = y.2
⊢ HasFDerivWithinAt (writtenInExtChartAt (I.prod I') I' x Prod.snd)
    (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)) (range ↑(I.prod I'))
    (↑(extChartAt (I.prod I') x) x)

Tactic:
apply HasFDerivWithinAt.congr_of_eventuallyEq hasFDerivWithinAt_snd this

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
x : M × M'
this :
  ∀ᶠ (y : E × E') in 𝓝[range ↑(I.prod I')] ↑(extChartAt (I.prod I') x) x,
    (↑(extChartAt I' x.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod I') x).symm) y = y.2
⊢ (↑(extChartAt I' x.2) ∘ Prod.snd ∘ ↑(extChartAt (I.prod I') x).symm) (↑(extChartAt (I.prod I') x) x) =
    (↑(extChartAt (I.prod I') x) x).2
-- Mathlib/RingTheory/Localization/Defs.lean
lemma at_units (S : Submonoid R)
    (hS : S ≤ IsUnit.submonoid R) : IsLocalization S R where
  map_units' y := hS y.prop
  surj' := fun s ↦ ⟨⟨s, 1⟩, by simp⟩
  exists_of_eq := fun {x y} (e : x = y) ↦ ⟨1, e ▸ rfl⟩

Proof state:
R : Type u_1
inst✝ : CommSemiring R
S : Submonoid R
hS : S ≤ IsUnit.submonoid R
s : R
⊢ s * (algebraMap R R) ↑(s, 1).2 = (algebraMap R R) (s, 1).1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem posPart_sub_negPart (f : α →ₛ ℝ) : f.posPart - f.negPart = f

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map (fun b => b ⊔ 0) f - map (fun b => b ⊔ 0) (-f) = f

Tactic:
ext a

Result:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (map (fun b => b ⊔ 0) f - map (fun b => b ⊔ 0) (-f)) a = f a

Proof state:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (⇑(map (fun b => b ⊔ 0) f) - ⇑(map (fun b => b ⊔ 0) (-f))) a = f a

Tactic:
exact max_zero_sub_eq_self (f a)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ f.posPart - f.negPart = f

Tactic:
simp only [posPart, negPart]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map (fun b => b ⊔ 0) f - map (fun b => b ⊔ 0) (-f) = f

Proof state:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (map (fun b => b ⊔ 0) f - map (fun b => b ⊔ 0) (-f)) a = f a

Tactic:
rw [coe_sub]

Result:
case H
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (⇑(map (fun b => b ⊔ 0) f) - ⇑(map (fun b => b ⊔ 0) (-f))) a = f a
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem IsNormal.conjugation_bij (Sn : IsNormal S) {c d} (p : c ⟶ d) :
    Set.BijOn (fun γ : c ⟶ c => Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
⊢ BijOn (fun γ => Groupoid.inv p ≫ γ ≫ p) (S.arrows c c) (S.arrows d d)

Tactic:
refine ⟨fun γ γS => Sn.conj p γS, fun γ₁ _ γ₂ _ h => ?_, fun δ δS =>
  ⟨p ≫ δ ≫ Groupoid.inv p, Sn.conj' p δS, ?_⟩⟩

Result:
case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ => Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ => Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂

case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun γ => Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ

Proof state:
case refine_1
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
γ₁ : c ⟶ c
x✝¹ : γ₁ ∈ S.arrows c c
γ₂ : c ⟶ c
x✝ : γ₂ ∈ S.arrows c c
h : (fun γ => Groupoid.inv p ≫ γ ≫ p) γ₁ = (fun γ => Groupoid.inv p ≫ γ ≫ p) γ₂
⊢ γ₁ = γ₂

Tactic:
simpa only [inv_eq_inv, Category.assoc, IsIso.hom_inv_id, Category.comp_id,
  IsIso.hom_inv_id_assoc] using p ≫= h =≫ inv p

Result:
no goals

Proof state:
case refine_2
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c d : C
p : c ⟶ d
δ : d ⟶ d
δS : δ ∈ S.arrows d d
⊢ (fun γ => Groupoid.inv p ≫ γ ≫ p) (p ≫ δ ≫ Groupoid.inv p) = δ

Tactic:
simp only [inv_eq_inv, Category.assoc, IsIso.inv_hom_id, Category.comp_id,
  IsIso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.polynomial_mul [ContinuousAdd β] [ContinuousMul β]
    (hf : SuperpolynomialDecay l k f) (p : β[X]) :
    SuperpolynomialDecay l k fun x => (p.eval <| k x) * f x :=
  Polynomial.induction_on' p (fun p q hp hq => by simpa [add_mul] using hp.add hq) fun n c => by
    simpa [mul_assoc] using (hf.param_pow_mul n).const_mul c

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
n : ℕ
c : β
⊢ SuperpolynomialDecay l k fun x => eval (k x) ((monomial n) c) * f x

Tactic:
simpa [mul_assoc] using (hf.param_pow_mul n).const_mul c

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p✝ p q : β[X]
hp : SuperpolynomialDecay l k fun x => eval (k x) p * f x
hq : SuperpolynomialDecay l k fun x => eval (k x) q * f x
⊢ SuperpolynomialDecay l k fun x => eval (k x) (p + q) * f x

Tactic:
simpa [add_mul] using hp.add hq

Result:
no goals
-- Mathlib/Probability/Kernel/WithDensity.lean
@[simp]
lemma withDensity_zero (κ : Kernel α β) [IsSFiniteKernel κ] :
    Kernel.withDensity κ 0 = 0

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (0 a✝¹)) s✝ = (0 a✝¹) s✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
⊢ κ.withDensity 0 = 0

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity 0) a✝¹) s✝ = (0 a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.withDensity 0) a✝¹) s✝ = (0 a✝¹) s✝

Tactic:
rw [Kernel.withDensity_apply _ measurable_const]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ a✝¹).withDensity (0 a✝¹)) s✝ = (0 a✝¹) s✝
-- Mathlib/Algebra/Star/Basic.lean
theorem semiconjBy_star_star_star {x y z : R} :
    SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z

Tactic:
simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y%n) n = Int.bmod (x - y) n

Proof state:
y x : Int
n : Nat
⊢ (x - (y - ↑n * (y / ↑n))).bmod n = (x - y).bmod n

Tactic:
rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, ← Int.add_assoc, Int.add_right_comm,
  Int.bmod_add_mul_cancel, Int.sub_eq_add_neg]

Result:
no goals

Proof state:
y x : Int
n : Nat
⊢ (x - y % ↑n).bmod n = (x - y).bmod n

Tactic:
simp only [emod_def]

Result:
y x : Int
n : Nat
⊢ (x - (y - ↑n * (y / ↑n))).bmod n = (x - y).bmod n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem lt_of_div_eq_zero (h : 0 < k) (h' : x / k = 0) : x < k

Proof state:
k x : Nat
h : 0 < k
h' : x / k = 0
⊢ x < k

Tactic:
rw [Nat.div_eq_iff h] at h'

Result:
k x : Nat
h : 0 < k
h' : x ≤ 0 * k + k - 1 ∧ 0 * k ≤ x
⊢ x < k

Proof state:
k x : Nat
h : 0 < k
h' : x ≤ 0 * k + k - 1 ∧ 0 * k ≤ x
⊢ x < k

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma degreeOf_monomial_eq (s : σ →₀ ℕ) (i : σ) {a : R} (ha : a ≠ 0) :
    (monomial s a).degreeOf i = s i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf i ((monomial s) a) = s i

Tactic:
classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
i : σ
a : R
ha : a ≠ 0
⊢ degreeOf i ((monomial s) a) = s i

Tactic:
rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_Prop {p : Prop} : IsEmpty p ↔ ¬p

Proof state:
p : Prop
⊢ IsEmpty p ↔ ¬p

Tactic:
simp only [← not_nonempty_iff, nonempty_prop]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem gcd_mul_gcd_of_coprime_of_mul_eq_mul
    (cop : Coprime c d) (h : a * b = c * d) : a.gcd c * b.gcd c = c

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c ∣ c * d

Tactic:
rw [← h]

Result:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c ∣ a * b

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ c

Tactic:
apply Nat.dvd_refl

Result:
no goals

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c ∣ c

Tactic:
apply ((cop.gcd_left _).mul (cop.gcd_left _)).dvd_of_dvd_mul_right

Result:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c ∣ c * d

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ c.gcd a * c.gcd b

Tactic:
refine Nat.dvd_trans ?_ (gcd_mul_dvd_mul_gcd ..)

Result:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ c.gcd (a * b)

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ a.gcd c * b.gcd c

Tactic:
rw [gcd_comm a, gcd_comm b]

Result:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ c.gcd a * c.gcd b

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ c.gcd (a * b)

Tactic:
rw [h, gcd_mul_right_right d c]

Result:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ c

Proof state:
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c = c

Tactic:
apply Nat.dvd_antisymm

Result:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c ∣ c

case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ c ∣ a.gcd c * b.gcd c

Proof state:
case a
c d a b : Nat
cop : c.Coprime d
h : a * b = c * d
⊢ a.gcd c * b.gcd c ∣ a * b

Tactic:
apply Nat.mul_dvd_mul (gcd_dvd ..).1 (gcd_dvd ..).1

Result:
no goals
-- Mathlib/RingTheory/ReesAlgebra.lean
theorem adjoin_monomial_eq_reesAlgebra :
    Algebra.adjoin R (Submodule.map (monomial 1 : R →ₗ[R] R[X]) I : Set R[X]) = reesAlgebra I

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∀ x ∈ p.support, (monomial x) (p.coeff x) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rintro i -

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ (monomial i) (p.coeff i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) = reesAlgebra I

Tactic:
apply le_antisymm

Result:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I

case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
i : ℕ
⊢ (monomial i) (p.coeff i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
exact monomial_mem_adjoin_monomial (hp i)

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I

Tactic:
apply Algebra.adjoin_le _

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ ↑(Submodule.map (monomial 1) I) ⊆ ↑(reesAlgebra I)

Tactic:
rintro _ ⟨r, hr, rfl⟩

Result:
case intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ (monomial 1) r ∈ ↑(reesAlgebra I)

Proof state:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ p ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
rw [p.as_sum_support]

Result:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∑ i ∈ p.support, (monomial i) (p.coeff i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
intro p hp

Result:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ p ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
case intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ (monomial 1) r ∈ ↑(reesAlgebra I)

Tactic:
exact reesAlgebra.monomial_mem.mpr (by rwa [pow_one])

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∑ i ∈ p.support, (monomial i) (p.coeff i) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
apply Subalgebra.sum_mem _ _

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
p : R[X]
hp : p ∈ reesAlgebra I
⊢ ∀ x ∈ p.support, (monomial x) (p.coeff x) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
r : R
hr : r ∈ ↑I
⊢ r ∈ I ^ 1

Tactic:
rwa [pow_one]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
lemma LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : ℕ → ℂ} {x : ℝ}
    (h : ∀ y : ℝ, x < y → LSeriesSummable f y) :
    abscissaOfAbsConv f ≤ x

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x | LSeriesSummable f ↑x})
a : EReal
⊢ ↑x < a → y ≤ a

Tactic:
replace hy : ∀ (a : ℝ), LSeriesSummable f a → y ≤ a := by simpa [mem_lowerBounds] using hy

Result:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < a → y ≤ a

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x | LSeriesSummable f ↑x})
a : EReal
⊢ ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a

Tactic:
simpa [mem_lowerBounds] using hy

Result:
no goals

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y a : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < a → y ≤ a

Tactic:
cases a with
| h_real a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
| h_bot => simp
| h_top => simp

Result:
no goals

Proof state:
case h_real
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
a₀ : ℝ
⊢ ↑x < ↑a₀ → y ≤ ↑a₀

Tactic:
exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)

Result:
no goals

Proof state:
case h_top
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < ⊤ → y ≤ ⊤

Tactic:
simp

Result:
no goals

Proof state:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
⊢ abscissaOfAbsConv f ≤ ↑x

Tactic:
refine sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_

Result:
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : y ∈ lowerBounds (Real.toEReal '' {x | LSeriesSummable f ↑x})
a : EReal
⊢ ↑x < a → y ≤ a

Proof state:
case h_bot
f : ℕ → ℂ
x : ℝ
h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y
y : EReal
hy : ∀ (a : ℝ), LSeriesSummable f ↑a → y ≤ ↑a
⊢ ↑x < ⊥ → y ≤ ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_nonneg_left_iff_sameRay (hx : x ≠ 0) :
    (∃ r : R, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
h : ∃ r, 0 ≤ r ∧ r • x = y
⊢ SameRay R x y

Tactic:
rcases h with ⟨r, hr, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)

Proof state:
case intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 ≤ r
⊢ SameRay R x (r • x)

Tactic:
exact SameRay.sameRay_nonneg_smul_right x hr

Result:
no goals

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y

Tactic:
refine ⟨fun h => ?_, fun h => h.exists_nonneg_left hx⟩

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
h : ∃ r, 0 ≤ r ∧ r • x = y
⊢ SameRay R x y
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_count (I : Ideal R) (hI : I ≠ 0) : (Associates.mk v.asIdeal).count
    (Associates.mk (∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
have h_ne_zero := Associates.finprod_ne_zero I

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
@[simp] lemma piAntidiag_empty_zero : piAntidiag (∅ : Finset ι) (0 : μ) = {0}

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
⊢ ∅.piAntidiag 0 = {0}

Tactic:
ext

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a✝ : ι → μ
⊢ a✝ ∈ ∅.piAntidiag 0 ↔ a✝ ∈ {0}

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a✝ : ι → μ
⊢ a✝ ∈ ∅.piAntidiag 0 ↔ a✝ ∈ {0}

Tactic:
simp [Fintype.sum_eq_zero_iff_of_nonneg, funext_iff, not_imp_comm, ← forall_and]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_modify [BEq α] (a : α) (l : AssocList α β) :
    (modify a f l).toList =
    l.toList.replaceF fun (k, v) => bif k == a then some (a, f k v) else none

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a : α
l : AssocList α β
⊢ (modify a f l).toList =
    List.replaceF
      (fun x =>
        match x.fst == a with
        | true => some (a, f x.fst x.snd)
        | false => none)
      l.toList

Tactic:
induction l with simp [List.replaceF]
| cons k v es ih => cases k == a <;> simp [ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a : α
l : AssocList α β
⊢ (modify a f l).toList =
    List.replaceF
      (fun x =>
        match x with
        | (k, v) => bif k == a then some (a, f k v) else none)
      l.toList

Tactic:
simp [cond]

Result:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a : α
l : AssocList α β
⊢ (modify a f l).toList =
    List.replaceF
      (fun x =>
        match x.fst == a with
        | true => some (a, f x.fst x.snd)
        | false => none)
      l.toList

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β → β
inst✝ : BEq α
a k : α
v : β
es : AssocList α β
ih :
  (modify a f es).toList =
    List.replaceF
      (fun x =>
        match x.fst == a with
        | true => some (a, f x.fst x.snd)
        | false => none)
      es.toList
⊢ (match k == a with
      | true => cons a (f k v) es
      | false => cons k v (modify a f es)).toList =
    match
      match k == a with
      | true => some (a, f k v)
      | false => none with
    | none =>
      (k, v) ::
        List.replaceF
          (fun x =>
            match x.fst == a with
            | true => some (a, f x.fst x.snd)
            | false => none)
          es.toList
    | some a => a :: es.toList

Tactic:
cases k == a <;> simp [ih]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
theorem IsInitial.strict_hom_ext (hI : IsInitial I) {A : C} (f g : A ⟶ I) : f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
⊢ f = g

Tactic:
haveI := hI.isIso_to f

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this : IsIso f
⊢ f = g

Tactic:
haveI := hI.isIso_to g

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
I : C
hI : IsInitial I
A : C
f g : A ⟶ I
this✝ : IsIso f
this : IsIso g
⊢ f = g

Tactic:
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem iInf_eq {u : ι → UniformSpace γ} : 𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)

Proof state:
case h
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ i, 𝓤 γ) = ⨅ i, 𝓤 (α →ᵤ γ)

Tactic:
exact (UniformFun.gc α γ).u_iInf

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ uniformSpace α γ = ⨅ i, uniformSpace α γ

Tactic:
ext : 1

Result:
case h
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)

Proof state:
case h
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)

Tactic:
change UniformFun.filter α γ 𝓤[⨅ i, u i] = 𝓤[⨅ i, 𝒰(α, γ, u i)]

Result:
case h
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)

Proof state:
case h
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)

Tactic:
rw [iInf_uniformity, iInf_uniformity]

Result:
case h
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ i, 𝓤 γ) = ⨅ i, 𝓤 (α →ᵤ γ)