harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem ext_of_forall_integral_eq [HasOuterApproxClosed Ω] [BorelSpace Ω]
    {μ ν : FiniteMeasure Ω} (h : ∀ (f : Ω →ᵇ ℝ), ∫ x, f x ∂μ = ∫ x, f x ∂ν) :
    μ = ν

Proof state:
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
⊢ μ = ν

Tactic:
apply ext_of_forall_lintegral_eq

Result:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
⊢ ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν

Proof state:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ ∫ (x : Ω), ↑(f x) ∂↑μ = ∫ (x : Ω), ↑(f x) ∂↑ν

Tactic:
exact h ⟨⟨fun x => (f x).toReal, Continuous.comp' NNReal.continuous_coe f.continuous⟩,
    f.map_bounded'⟩

Result:
no goals

Proof state:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
⊢ ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν

Tactic:
intro f

Result:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν

Proof state:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω), ↑(f x) ∂↑μ = ∫⁻ (x : Ω), ↑(f x) ∂↑ν

Tactic:
apply (ENNReal.toReal_eq_toReal_iff' (lintegral_lt_top_of_nnreal μ f).ne
    (lintegral_lt_top_of_nnreal ν f).ne).mp

Result:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal = (∫⁻ (x : Ω), ↑(f x) ∂↑ν).toReal

Proof state:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (x : Ω), ↑(f x) ∂↑μ).toReal = (∫⁻ (x : Ω), ↑(f x) ∂↑ν).toReal

Tactic:
rw [toReal_lintegral_coe_eq_integral f μ, toReal_lintegral_coe_eq_integral f ν]

Result:
case h
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : HasOuterApproxClosed Ω
inst✝ : BorelSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (f : Ω →ᵇ ℝ), ∫ (x : Ω), f x ∂↑μ = ∫ (x : Ω), f x ∂↑ν
f : Ω →ᵇ ℝ≥0
⊢ ∫ (x : Ω), ↑(f x) ∂↑μ = ∫ (x : Ω), ↑(f x) ∂↑ν
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrable_map_homeomorph [BorelSpace X] [BorelSpace Y] (e : X ≃ₜ Y) {f : Y → E}
    {μ : Measure X} : LocallyIntegrable f (Measure.map e μ) ↔ LocallyIntegrable (f ∘ e) μ

Proof state:
case refine_2
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
⊢ IntegrableAtFilter f (𝓝 x) (map (⇑e) μ)

Tactic:
rcases h (e.symm x) with ⟨U, hU, h'U⟩

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableAtFilter f (𝓝 x) (map (⇑e) μ)

Proof state:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableAtFilter f (𝓝 x) (map (⇑e) μ)

Tactic:
refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩

Result:
case refine_2.intro.intro
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : TopologicalSpace Y
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → E
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
U : Set X
hU : U ∈ 𝓝 (e.symm x)
h'U : IntegrableOn (f ∘ ⇑e) U μ
⊢ IntegrableOn f (⇑e.symm ⁻¹' U) (map (⇑e) μ)
-- Mathlib/Tactic/Positivity/Core.lean
lemma pos_of_isNat {n : ℕ} [OrderedSemiring A] [Nontrivial A]
    (h : NormNum.IsNat e n) (w : Nat.ble 1 n = true) : 0 < (e : A)

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝¹ : OrderedSemiring A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Result:
A : Type u_1
e : A
n : ℕ
inst✝¹ : OrderedSemiring A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝¹ : OrderedSemiring A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n

Tactic:
simpa using w

Result:
no goals

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝¹ : OrderedSemiring A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < ↑n

Tactic:
apply Nat.cast_pos.2

Result:
A : Type u_1
e : A
n : ℕ
inst✝¹ : OrderedSemiring A
inst✝ : Nontrivial A
h : NormNum.IsNat e n
w : Nat.ble 1 n = true
⊢ 0 < n
-- Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean
@[reassoc (attr := simp)]
lemma hom_inv_id : hom f g ≫ inv f g = 𝟙 _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ hom f g ≫ inv f g = 𝟙 (mappingCone g)

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ (hom f g ≫ inv f g).f n = (𝟙 (mappingCone g)).f n

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ (hom f g ≫ inv f g).f n = (𝟙 (mappingCone g)).f n

Tactic:
simp [hom, inv, lift_desc_f _ _ _ _ _ _ _ n (n+1) rfl, ext_from_iff _ (n + 1) _ rfl]

Result:
no goals
-- Mathlib/RingTheory/Localization/Ideal.lean
theorem ideal_eq_iInf_comap_map_away {S : Finset R} (hS : Ideal.span (α := R) S = ⊤) (I : Ideal R) :
    I = ⨅ f ∈ S, (I.map (algebraMap R (Localization.Away f))).comap
    (algebraMap R (Localization.Away f))

Proof state:
case a.H.mk.intro.mk.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e :
  (algebraMap R (Localization.Away s)) x * (algebraMap R (Localization.Away s)) (s ^ n) =
    (algebraMap R (Localization.Away s)) ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Tactic:
rw [← map_mul, IsLocalization.eq_iff_exists (.powers s)] at e

Result:
case a.H.mk.intro.mk.mk.intro
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x s : R
hs : s ∈ ↑S
hx : ∀ i ∈ S, (algebraMap R (Localization.Away i)) x ∈ Ideal.map (algebraMap R (Localization.Away i)) I
y : ↥I
n : ℕ
e : ∃ c, ↑c * (x * s ^ n) = ↑c * ↑y
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I

Proof state:
case a.H
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
⊢ ∀ (r : ↑↑S), ∃ n, ↑r ^ n • x ∈ I

Tactic:
rintro ⟨s, hs⟩

Result:
case a.H.mk
R : Type u_1
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
I : Ideal R
x : R
hx : x ∈ ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
s : R
hs : s ∈ ↑S
⊢ ∃ n, ↑⟨s, hs⟩ ^ n • x ∈ I
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem exists_lt_finrank_of_infinite_dimensional
    [Algebra.IsAlgebraic F E] (hnfd : ¬ FiniteDimensional F E) (n : ℕ) :
    ∃ L : IntermediateField F E, FiniteDimensional F L ∧ n < finrank F L

Proof state:
case succ.intro.intro.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥L
hn : n < finrank F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional F ↥F⟮x⟯
h : ¬n + 1 < finrank F ↥L'
⊢ False

Tactic:
have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)

Result:
case succ.intro.intro.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
hnfd : ¬FiniteDimensional F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥L
hn : n < finrank F ↥L
x : E
hx : x ∉ L
L' : IntermediateField F E := L ⊔ F⟮x⟯
this : FiniteDimensional F ↥F⟮x⟯
h : ¬n + 1 < finrank F ↥L'
h1 : L = L'
⊢ False

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥L
hn : n < finrank F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E

Tactic:
rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
n : ℕ
L : IntermediateField F E
fin : FiniteDimensional F ↥⊤
hn : n < finrank F ↥L
hnfd : ∀ (x : E), x ∈ L
⊢ FiniteDimensional F E
-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem withDensity_eq_iff {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) :
    μ.withDensity f = μ.withDensity g ↔ f =ᵐ[μ] g :=
  ⟨fun hfg ↦ by
    refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_
    · rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
        withDensity_apply f MeasurableSet.univ, setLIntegral_univ]
    · rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg], withDensity_congr_ae⟩

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᶠ[ae μ] g

Tactic:
refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfg : μ.withDensity f = μ.withDensity g
⊢ ∫⁻ (x : α), g x ∂μ ≠ ⊤

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ⊤
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ⊤
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfg : μ.withDensity f = μ.withDensity g
⊢ ∫⁻ (x : α), g x ∂μ ≠ ⊤

Tactic:
rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
  withDensity_apply f MeasurableSet.univ, setLIntegral_univ]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β)
    (h : Injective f) : lift.{v} #(f ⁻¹' s) ≤ lift.{u} #s

Proof state:
case inj'
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective (Subtype.coind (fun x => f ↑x) ⋯)

Tactic:
apply Subtype.coind_injective

Result:
case inj'.hf
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x => f ↑x

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift.{v, u} #↑(f ⁻¹' s) ≤ lift.{u, v} #↑s

Tactic:
rw [lift_mk_le.{0}]

Result:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)

Proof state:
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)

Tactic:
use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2

Result:
case inj'
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective (Subtype.coind (fun x => f ↑x) ⋯)

Proof state:
case inj'.hf
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x => f ↑x

Tactic:
exact h.comp Subtype.val_injective

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem eq_enumOrd (f : Ordinal → Ordinal) (hs : ¬ BddAbove s) :
    enumOrd s = f ↔ StrictMono f ∧ range f = s

Proof state:
case mpr.intro
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ enumOrd s = f

Tactic:
rwa [← (enumOrd_strictMono hs).range_inj h₁, range_enumOrd hs, eq_comm]

Result:
no goals

Proof state:
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s

Tactic:
constructor

Result:
case mp
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f → StrictMono f ∧ range f = s

case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f

Proof state:
case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ enumOrd s = f

Proof state:
case mp
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f → StrictMono f ∧ range f = s

Tactic:
rintro rfl

Result:
case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s) ∧ range (enumOrd s) = s

Proof state:
case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s) ∧ range (enumOrd s) = s

Tactic:
exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Defs.lean
theorem subsingleton_of_subsingleton [Subsingleton (Subsemigroup M)] : Subsingleton M

Proof state:
case allEq
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ x = y

Tactic:
have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]

Result:
case allEq
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
this : ∀ (a : M), a ∈ ⊥
⊢ x = y

Proof state:
case allEq
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
this : ∀ (a : M), a ∈ ⊥
⊢ x = y

Tactic:
exact absurd (this x) not_mem_bot

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ ∀ (a : M), a ∈ ⊥

Tactic:
simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]

Result:
no goals

Proof state:
case allEq
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b

Tactic:
intro x y

Result:
case allEq
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
x y : M
⊢ x = y

Proof state:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ Subsingleton M

Tactic:
constructor

Result:
case allEq
M : Type u_1
inst✝¹ : Mul M
inst✝ : Subsingleton (Subsemigroup M)
⊢ ∀ (a b : M), a = b
-- Mathlib/Data/Nat/Find.lean
lemma find_eq_iff (h : ∃ n : ℕ, p n) : Nat.find h = m ↔ p m ∧ ∀ n < m, ¬ p n

Proof state:
case mp
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (Nat.find h) ∧ ∀ (n : ℕ), n < Nat.find h → ¬p n

Tactic:
exact ⟨Nat.find_spec h, fun _ ↦ Nat.find_min h⟩

Result:
no goals

Proof state:
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n

Tactic:
constructor

Result:
case mp
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n

case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m

Proof state:
case mpr.intro
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find h = m

Tactic:
exact le_antisymm (Nat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| Nat.find_spec h)

Result:
no goals

Proof state:
case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m

Tactic:
rintro ⟨hm, hlt⟩

Result:
case mpr.intro
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find h = m

Proof state:
case mp
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n

Tactic:
rintro rfl

Result:
case mp
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ p (Nat.find h) ∧ ∀ (n : ℕ), n < Nat.find h → ¬p n
-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem PairwiseDisjoint.prod_left {f : ι × ι' → α}
    (hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i'))
    (ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) :
    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f

Proof state:
case mk.mk
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
rw [mem_prod] at hi hj

Result:
case mk.mk
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Proof state:
case mk.mk.inr.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => ⨆ i' ∈ t, f (i, i')) (j, j').1

Tactic:
convert le_iSup₂ (α := α) j' hj.2

Result:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') = f ((j, j').1, j')

Proof state:
case mk.mk.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')

Tactic:
refine (ht hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 h).mono ?_ ?_

Result:
case mk.mk.inl.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun i' => ⨆ i ∈ s, f (i, i')) (i, i').2

case mk.mk.inl.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun i' => ⨆ i ∈ s, f (i, i')) (i, j').2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_le_of_le_sub {a b c : Nat} (hle : b ≤ c) (h : a ≤ c - b) : a + b ≤ c

Proof state:
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = c

Tactic:
rw [Nat.eq_add_of_sub_eq hle hd.symm]

Result:
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = a + d + b

Proof state:
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
⊢ a + b ≤ c

Tactic:
match le.dest h with
| ⟨d, hd⟩ =>
  apply @le.intro _ _ d
  rw [Nat.eq_add_of_sub_eq hle hd.symm]
  simp [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals

Proof state:
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b ≤ c

Tactic:
apply @le.intro _ _ d

Result:
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = c

Proof state:
a b c : Nat
hle : b ≤ c
h : a ≤ c - b
d : Nat
hd : a + d = c - b
⊢ a + b + d = a + d + b

Tactic:
simp [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean
lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux
    (p₁ p₂ : PrimeSpectrum (S ⊗[R] T))
    (h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂) :
    p₁ ≤ p₂

Proof state:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ False

Tactic:
have h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal := e ▸ p₁.asIdeal.mul_mem_left (1 ⊗ₜ[R] (r • t)) hxp₁

Result:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
h₁ : a ⊗ₜ[R] t ∈ p₁.asIdeal
⊢ False
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_le_iff_coeff_eq_zero : p.natDegree ≤ n ↔ ∀ N : ℕ, n < N → p.coeff N = 0

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree ≤ n ↔ ∀ (N : ℕ), n < N → p.coeff N = 0

Tactic:
simp_rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero, Nat.cast_lt]

Result:
no goals