harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sum/Interval.lean
lemma inl_mem_sumLexLift {c₁ : γ₁} :
    inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
      (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨
        ∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f₁ : α₁ → β₁ → Finset γ₁
f₂ : α₂ → β₂ → Finset γ₂
g₁ : α₁ → β₂ → Finset γ₁
g₂ : α₁ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
c₁ : γ₁
⊢ inl c₁ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ c₁ ∈ f₁ a₁ b₁) ∨ ∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₁ ∈ g₁ a₁ b₂

Tactic:
simp [mem_sumLexLift]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_smul (P Q : Fin 3 → R) (u v : R) :
    W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q

Tactic:
simp only [addX, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ u ^ 2 * P x * (v ^ 2 * Q x) ^ 2 * (u * P z) ^ 2 - 2 * (u ^ 3 * P y) * (v ^ 3 * Q y) * (u * P z) * (v * Q z) +
                      (u ^ 2 * P x) ^ 2 * (v ^ 2 * Q x) * (v * Q z) ^ 2 -
                    W'.a₁ * (u ^ 2 * P x) * (v ^ 3 * Q y) * (u * P z) ^ 2 * (v * Q z) -
                  W'.a₁ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) * (v * Q z) ^ 2 +
                2 * W'.a₂ * (u ^ 2 * P x) * (v ^ 2 * Q x) * (u * P z) ^ 2 * (v * Q z) ^ 2 -
              W'.a₃ * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) -
            W'.a₃ * (u ^ 3 * P y) * (u * P z) * (v * Q z) ^ 4 +
          W'.a₄ * (v ^ 2 * Q x) * (u * P z) ^ 4 * (v * Q z) ^ 2 +
        W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 2 * (v * Q z) ^ 4 +
      2 * W'.a₆ * (u * P z) ^ 4 * (v * Q z) ^ 4 =
    ((u * v) ^ 2) ^ 2 *
      (P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 -
                      W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                    W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                  2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                W'.a₃ * Q y * P z ^ 4 * Q z -
              W'.a₃ * P y * P z * Q z ^ 4 +
            W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
          W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
        2 * W'.a₆ * P z ^ 4 * Q z ^ 4)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ u ^ 2 * P x * (v ^ 2 * Q x) ^ 2 * (u * P z) ^ 2 - 2 * (u ^ 3 * P y) * (v ^ 3 * Q y) * (u * P z) * (v * Q z) +
                      (u ^ 2 * P x) ^ 2 * (v ^ 2 * Q x) * (v * Q z) ^ 2 -
                    W'.a₁ * (u ^ 2 * P x) * (v ^ 3 * Q y) * (u * P z) ^ 2 * (v * Q z) -
                  W'.a₁ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) * (v * Q z) ^ 2 +
                2 * W'.a₂ * (u ^ 2 * P x) * (v ^ 2 * Q x) * (u * P z) ^ 2 * (v * Q z) ^ 2 -
              W'.a₃ * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) -
            W'.a₃ * (u ^ 3 * P y) * (u * P z) * (v * Q z) ^ 4 +
          W'.a₄ * (v ^ 2 * Q x) * (u * P z) ^ 4 * (v * Q z) ^ 2 +
        W'.a₄ * (u ^ 2 * P x) * (u * P z) ^ 2 * (v * Q z) ^ 4 +
      2 * W'.a₆ * (u * P z) ^ 4 * (v * Q z) ^ 4 =
    ((u * v) ^ 2) ^ 2 *
      (P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 -
                      W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                    W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                  2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                W'.a₃ * Q y * P z ^ 4 * Q z -
              W'.a₃ * P y * P z * Q z ^ 4 +
            W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
          W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
        2 * W'.a₆ * P z ^ 4 * Q z ^ 4)

Tactic:
ring1

Result:
no goals
-- Mathlib/FieldTheory/Normal/Basic.lean
theorem exists_algEquiv_of_root' [Normal K L]{x y : L} (hy : IsAlgebraic K y)
    (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ y = x

Proof state:
case h
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
σ : L ≃ₐ[K] L
hσ : σ x = y
⊢ σ.symm y = x

Tactic:
rw [← hσ, symm_apply_apply]

Result:
no goals

Proof state:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
⊢ ∃ σ, σ y = x

Tactic:
obtain ⟨σ, hσ⟩ := exists_algEquiv_of_root hy h_ev

Result:
case intro
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
σ : L ≃ₐ[K] L
hσ : σ x = y
⊢ ∃ σ, σ y = x

Proof state:
case intro
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
σ : L ≃ₐ[K] L
hσ : σ x = y
⊢ ∃ σ, σ y = x

Tactic:
use σ.symm

Result:
case h
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
σ : L ≃ₐ[K] L
hσ : σ x = y
⊢ σ.symm y = x
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma mod_two_not_eq_one : ¬n % 2 = 1 ↔ n % 2 = 0

Proof state:
n : ℕ
⊢ ¬n % 2 = 1 ↔ n % 2 = 0

Tactic:
cases mod_two_eq_zero_or_one n <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem _root_.BddAbove.convolutionExistsAt [MeasurableAdd₂ G] [SFinite μ] {x₀ : G} {s : Set G}
    (hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))) (hs : MeasurableSet s)
    (h2s : (support fun t => L (f t) (g (x₀ - t))) ⊆ s) (hf : IntegrableOn f s μ)
    (hmg : AEStronglyMeasurable g μ) : ConvolutionExistsAt f g x₀ L μ

Proof state:
case refine_2
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd₂ G
inst✝ : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))
hs : MeasurableSet s
h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))

Tactic:
have : AEStronglyMeasurable g (map (fun t : G => x₀ - t) μ) :=
  hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous

Result:
case refine_2
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup E'
inst✝¹⁰ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 E'
inst✝⁶ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁵ : MeasurableSpace G
μ : Measure G
inst✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd₂ G
inst✝ : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))
hs : MeasurableSet s
h2s : (support fun t => (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
this : AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) μ)
⊢ AEStronglyMeasurable g (Measure.map (fun t => x₀ - t) (μ.restrict s))
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem dirac_bind {f : α → Measure β} (hf : Measurable f) (a : α) : bind (dirac a) f = f a

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((dirac a).bind f) s = (f a) s

Tactic:
erw [bind_apply hs hf, lintegral_dirac' a ((measurable_coe hs).comp hf)]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((fun μ => μ s) ∘ f) a = (f a) s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
⊢ (dirac a).bind f = f a

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((dirac a).bind f) s = (f a) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((fun μ => μ s) ∘ f) a = (f a) s

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
theorem jacobiTheta₂'_functional_equation (z τ : ℂ) :
    jacobiTheta₂' z τ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-1 / τ).im

Tactic:
rw [div_eq_mul_inv, neg_one_mul, neg_im, inv_im, neg_div, neg_neg]

Result:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < τ.im / normSq τ

Proof state:
z τ : ℂ
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rcases le_or_lt (im τ) 0 with hτ | hτ

Result:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
this : HasDerivAt (fun x => jacobiTheta₂ x (-1 / τ)) (jacobiTheta₂' (z / τ) (-1 / τ)) (z / τ)
⊢ HasDerivAt (fun w => jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z

Tactic:
simpa only [mul_comm, one_div] using this.comp z (hasDerivAt_mul_const τ⁻¹)

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < τ.im / normSq τ

Tactic:
exact div_pos hτ (normSq_pos.mpr (fun h ↦ lt_irrefl 0 (zero_im ▸ h ▸ hτ)))

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lq (f g : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
    ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Proof state:
case inr.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i => f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
let g' i := g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)

Result:
case inr.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i => f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i => f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
this : (∑ i ∈ s, f i * g i) / ((∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ 0 < (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
exact mul_pos (rpow_pos hf) (rpow_pos hg)

Result:
no goals

Proof state:
case inr.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
let f' i := f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)

Result:
case inr.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
hg : 0 < ∑ i ∈ s, g i ^ q
f' : ι → ℝ≥0 := fun i => f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem _root_.Real.multiset_prod_map_rpow {ι} (s : Multiset ι) (f : ι → ℝ)
    (hs : ∀ i ∈ s, (0 : ℝ) ≤ f i) (r : ℝ) :
    (s.map (f · ^ r)).prod = (s.map f).prod ^ r

Proof state:
ι : Type u_1
s : Multiset ι
f : ι → ℝ
hs : ∀ i ∈ s, 0 ≤ f i
r : ℝ
⊢ (Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r

Tactic:
induction' s using Quotient.inductionOn with l

Result:
case h
ι : Type u_1
f : ι → ℝ
r : ℝ
l : List ι
hs : ∀ i ∈ ⟦l⟧, 0 ≤ f i
⊢ (Multiset.map (fun x => f x ^ r) ⟦l⟧).prod = (Multiset.map f ⟦l⟧).prod ^ r

Proof state:
case h
ι : Type u_1
f : ι → ℝ
r : ℝ
l : List ι
hs : ∀ i ∈ ⟦l⟧, 0 ≤ f i
⊢ (Multiset.map (fun x => f x ^ r) ⟦l⟧).prod = (Multiset.map f ⟦l⟧).prod ^ r

Tactic:
simpa using Real.list_prod_map_rpow' l f hs r

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem lift_inv_comp_right {A B : Grp_ C} (f : A ⟶ B) :
    lift f.hom (A.inv ≫ f.hom) ≫ B.mul = toUnit _ ≫ B.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
this : (lift (𝟙 A.X) A.inv ≫ A.mul) ≫ f.hom = (toUnit A.X ≫ A.one) ≫ f.hom
⊢ lift f.hom (A.inv ≫ f.hom) ≫ B.mul = toUnit A.X ≫ B.one

Tactic:
rwa [assoc, f.mul_hom, assoc, f.one_hom, lift_map_assoc, id_comp] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
⊢ lift f.hom (A.inv ≫ f.hom) ≫ B.mul = toUnit A.X ≫ B.one

Tactic:
have := A.right_inv =≫ f.hom

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A B : Grp_ C
f : A ⟶ B
this : (lift (𝟙 A.X) A.inv ≫ A.mul) ≫ f.hom = (toUnit A.X ≫ A.one) ≫ f.hom
⊢ lift f.hom (A.inv ≫ f.hom) ≫ B.mul = toUnit A.X ≫ B.one
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrable.integrable_of_isBigO_atTop [IsMeasurablyGenerated (atTop (α := α))]
    [OrderBot α] (hf : LocallyIntegrable f μ) (ho : f =O[atTop] g)
    (hg : IntegrableAtFilter g atTop μ) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atTop.IsMeasurablyGenerated
inst✝ : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atTop.IsMeasurablyGenerated
inst✝ : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
f : α → E
g : α → F
inst✝⁷ : TopologicalSpace α
inst✝⁶ : SecondCountableTopology α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup F
inst✝³ : LinearOrder α
inst✝² : CompactIccSpace α
inst✝¹ : atTop.IsMeasurablyGenerated
inst✝ : OrderBot α
hf : LocallyIntegrable f μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem natDegree_of_c_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) :
    P.toPoly.natDegree = 1

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.natDegree = 1

Tactic:
rw [of_b_eq_zero ha hb, natDegree_linear hc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
theorem pullback {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} (h : IsKernelPair g a₁ a₂)
    (f : X ⟶ Z) [HasPullback f g] [HasPullback f (a₁ ≫ g)] :
    IsKernelPair (pullback.fst f g)
      (pullback.map f _ f _ (𝟙 X) a₁ (𝟙 Z) (by simp) <| Category.comp_id _)
      (pullback.map _ _ _ _ (𝟙 X) a₂ (𝟙 Z) (by simp) <| (Category.comp_id _).trans h.1.1)

Proof state:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (s.fst ≫ pullback.fst f g) ≫ f = h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯ ≫ a₁ ≫ g

Tactic:
simp only [assoc, lift_fst_assoc, pullback.condition]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem isPrimal_mk {a : M} : IsPrimal (Associates.mk a) ↔ IsPrimal a

Proof state:
case mp.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : Associates.mk a = Associates.mk (a₁ * a₂)
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
obtain ⟨u, rfl⟩ := mk_eq_mk_iff_associated.mp eq.symm

Result:
case mp.intro.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
b c a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
u : Mˣ
h :
  ∀ (a a_1 : M),
    a₁ * a₂ * ↑u ∣ a * a_1 → ∃ x x_1, x ∣ a ∧ x_1 ∣ a_1 ∧ Associates.mk (a₁ * a₂ * ↑u) = Associates.mk (x * x_1)
dvd : a₁ * a₂ * ↑u ∣ b * c
eq : Associates.mk (a₁ * a₂ * ↑u) = Associates.mk (a₁ * a₂)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ b ∧ a₂_1 ∣ c ∧ a₁ * a₂ * ↑u = a₁_1 * a₂_1

Proof state:
case mp.intro.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
b c a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
u : Mˣ
h :
  ∀ (a a_1 : M),
    a₁ * a₂ * ↑u ∣ a * a_1 → ∃ x x_1, x ∣ a ∧ x_1 ∣ a_1 ∧ Associates.mk (a₁ * a₂ * ↑u) = Associates.mk (x * x_1)
dvd : a₁ * a₂ * ↑u ∣ b * c
eq : Associates.mk (a₁ * a₂ * ↑u) = Associates.mk (a₁ * a₂)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ b ∧ a₂_1 ∣ c ∧ a₁ * a₂ * ↑u = a₁_1 * a₂_1

Tactic:
exact ⟨a₁, a₂ * u, h₁, Units.mul_right_dvd.mpr h₂, mul_assoc _ _ _⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
constructor <;> intro h b c dvd <;> obtain ⟨a₁, a₂, h₁, h₂, eq⟩ := @h b c dvd

Result:
case mp.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : Associates.mk a = Associates.mk (a₁ * a₂)
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

case mpr.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ IsPrimal (Associates.mk a) ↔ IsPrimal a

Tactic:
simp_rw [IsPrimal, forall_associated, mk_surjective.exists, mk_mul_mk, mk_dvd_mk]

Result:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Proof state:
case mpr.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
a₁ a₂ : M
h₁ : a₁ ∣ b
h₂ : a₂ ∣ c
eq : a = a₁ * a₂
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)

Tactic:
exact ⟨a₁, a₂, h₁, h₂, congr_arg _ eq⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_Ioc (a b : ℝ) : f.measure (Ioc a b) = ofReal (f b - f a)

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ f.measure (Ioc a b) = ofReal (↑f b - ↑f a)

Tactic:
rw [StieltjesFunction.measure]

Result:
f : StieltjesFunction
a b : ℝ
⊢ { toOuterMeasure := f.outer, m_iUnion := ⋯, trim_le := ⋯ } (Ioc a b) = ofReal (↑f b - ↑f a)

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ { toOuterMeasure := f.outer, m_iUnion := ⋯, trim_le := ⋯ } (Ioc a b) = ofReal (↑f b - ↑f a)

Tactic:
exact f.outer_Ioc a b

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem LipschitzWith.to_rightInverse [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0}
    {f : α → β} (hf : LipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) :
    AntilipschitzWith K g := fun x y => by simpa only [hg _] using hf (g x) (g y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist x y ≤ ↑K * edist (g x) (g y)

Tactic:
simpa only [hg _] using hf (g x) (g y)

Result:
no goals