harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/FinitePresentation.lean
/--
Let `M` `N` be a finitely presented `R`-modules.
Any `Mₛ ≃ₗ[R] Nₛ` between the localizations at `S : Submonoid R` can be lifted to an
isomorphism between `Mᵣ ≃ₗ[R] Nᵣ` for some `r ∈ S`.
-/
lemma Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule
    [Module.FinitePresentation R M] [Module.FinitePresentation R N]
    (l : M' ≃ₗ[R] N') :
    ∃ (r : R) (hr : r ∈ S)
      (l' : LocalizedModule (.powers r) M ≃ₗ[Localization (.powers r)]
        LocalizedModule (.powers r) N),
      (LocalizedModule.lift (.powers r) g fun s ↦ map_units g ⟨s.1, SetLike.le_def.mp
        (Submonoid.powers_le.mpr hr) s.2⟩) ∘ₗ l'.toLinearMap =
        l ∘ₗ (LocalizedModule.lift (.powers r) f fun s ↦ map_units f ⟨s.1, SetLike.le_def.mp
        (Submonoid.powers_le.mpr hr) s.2⟩)

Proof state:
case intro.intro.intro.intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Tactic:
have hsu : IsUnit (algebraMap R Rᵣₛ s) := isUnit_of_dvd_unit
    (hu := IsLocalization.map_units (M := rs) Rᵣₛ ⟨_, Submonoid.mem_powers _⟩)
    (map_dvd (algebraMap R Rᵣₛ) ⟨r, mul_comm _ _⟩)

Result:
case intro.intro.intro.intro
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
⊢ ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_sub_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a)
    (hfin : FiniteMultiplicity p b) : multiplicity p (a - b) = multiplicity p b

Proof state:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p a

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p (a - b) = multiplicity p b

Tactic:
rw [sub_eq_add_neg, hfin.neg.multiplicity_add_of_gt] <;> rw [multiplicity_neg]

Result:
α : Type u_1
inst✝ : Ring α
p a b : α
h : multiplicity p b < multiplicity p a
hfin : FiniteMultiplicity p b
⊢ multiplicity p b < multiplicity p a
-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : NonAssocSemiring R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
case mk
R : Type u
inst₂ : NonAssocSemiring R
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
this✝ : toAddCommMonoidWithOne = toAddCommMonoidWithOne
this : toNatCast = toNatCast
⊢ mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝ = inst₂

Tactic:
cases inst₂

Result:
case mk.mk
R : Type u
toNonUnitalNonAssocSemiring✝¹ : NonUnitalNonAssocSemiring R
toOne✝¹ : One R
one_mul✝¹ : ∀ (a : R), 1 * a = a
mul_one✝¹ : ∀ (a : R), a * 1 = a
toNatCast✝¹ : NatCast R
natCast_zero✝¹ : NatCast.natCast 0 = 0
natCast_succ✝¹ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
toNonUnitalNonAssocSemiring✝ : NonUnitalNonAssocSemiring R
toOne✝ : One R
one_mul✝ : ∀ (a : R), 1 * a = a
mul_one✝ : ∀ (a : R), a * 1 = a
toNatCast✝ : NatCast R
natCast_zero✝ : NatCast.natCast 0 = 0
natCast_succ✝ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
h : toNonUnitalNonAssocSemiring = toNonUnitalNonAssocSemiring
h_zero : Zero.zero = Zero.zero
h_one' : MulOneClass.toOne = MulOneClass.toOne
h_one : One.one = One.one
this✝ : toAddCommMonoidWithOne = toAddCommMonoidWithOne
this : toNatCast = toNatCast
⊢ mk one_mul✝¹ mul_one✝¹ natCast_zero✝¹ natCast_succ✝¹ = mk one_mul✝ mul_one✝ natCast_zero✝ natCast_succ✝
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_compQuasiMeasurePreserving (g : β →ₘ[ν] γ) (hf : QuasiMeasurePreserving f μ ν) :
    g.compQuasiMeasurePreserving f hf =ᵐ[μ] g ∘ f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ ↑(g.compQuasiMeasurePreserving f hf) =ᶠ[ae μ] ↑g ∘ f

Tactic:
rw [compQuasiMeasurePreserving_eq_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ ↑(mk (↑g ∘ f) ⋯) =ᶠ[ae μ] ↑g ∘ f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace γ
inst✝ : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ ↑(mk (↑g ∘ f) ⋯) =ᶠ[ae μ] ↑g ∘ f

Tactic:
apply coeFn_mk

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem Associates.finite_factors {I : Ideal R} (hI : I ≠ 0) :
    ∀ᶠ v : HeightOneSpectrum R in Filter.cofinite,
      ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ) = 0

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬(Associates.mk v.asIdeal).count (Associates.mk I).factors = 0} ↔ v ∈ {v | v.asIdeal ∣ I}

Tactic:
exact Associates.count_ne_zero_iff_dvd hI v.irreducible

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ {v | v.asIdeal ∣ I}.Finite

Tactic:
exact Ideal.finite_factors hI

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}

Tactic:
ext v

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} ↔ v ∈ {v | v.asIdeal ∣ I}

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

Tactic:
have h_supp : {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count
    (Associates.mk I).factors : ℤ) = 0} = {v : HeightOneSpectrum R | v.asIdeal ∣ I} := by
  ext v
  simp_rw [Int.natCast_eq_zero]
  exact Associates.count_ne_zero_iff_dvd hI v.irreducible

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

Tactic:
rw [Filter.eventually_cofinite, h_supp]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ {v | v.asIdeal ∣ I}.Finite

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} ↔ v ∈ {v | v.asIdeal ∣ I}

Tactic:
simp_rw [Int.natCast_eq_zero]

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
⊢ v ∈ {v | ¬(Associates.mk v.asIdeal).count (Associates.mk I).factors = 0} ↔ v ∈ {v | v.asIdeal ∣ I}
-- Mathlib/NumberTheory/ClassNumber/AdmissibleAbs.lean
theorem exists_partition_int (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : ℤ} (hb : b ≠ 0) (A : Fin n → ℤ) :
    ∃ t : Fin n → Fin ⌈1 / ε⌉₊,
    ∀ i₀ i₁, t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε

Proof state:
case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁
hi : ↑⌊↑(A i₀ % b) / |b| • ε⌋.natAbs = ↑⌊↑(A i₁ % b) / |b| • ε⌋.natAbs
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε

Tactic:
rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi

Result:
case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁
hi : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε

Proof state:
case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₀ % b) / |b| • ε - ↑(A i₁ % b) / |b| • ε| < 1
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε

Tactic:
rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff₀ hbε, one_mul] at hi

Result:
case refine_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ : (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₀ = (fun i => ⟨⌊↑(A i % b) / |b| • ε⌋.natAbs, ⋯⟩) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₁ % b) - ↑(A i₀ % b)| < |b| • ε
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
-- Mathlib/Algebra/Star/Basic.lean
theorem star_div₀ [CommGroupWithZero R] [StarMul R] (x y : R) : star (x / y) = star x / star y

Proof state:
R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ star (x / y) = star x / star y

Tactic:
apply op_injective

Result:
case a
R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star (x / y)) = op (star x / star y)

Proof state:
case a
R : Type u
inst✝¹ : CommGroupWithZero R
inst✝ : StarMul R
x y : R
⊢ op (star (x / y)) = op (star x / star y)

Tactic:
rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma pow_sub_one_dvd_differentIdeal_aux [IsFractionRing B L] [IsDedekindDomain A]
    [NoZeroSMulDivisors A B] [Module.Finite A B]
    {p : Ideal A} [p.IsMaximal] (P : Ideal B) {e : ℕ} (he : e ≠ 0) (hp : p ≠ ⊥)
    (hP : P ^ e ∣ p.map (algebraMap A B)) : P ^ (e - 1) ∣ differentIdeal A B

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²² : CommRing A
inst✝²¹ : Field K
inst✝²⁰ : CommRing B
inst✝¹⁹ : Field L
inst✝¹⁸ : Algebra A K
inst✝¹⁷ : Algebra B L
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra K L
inst✝¹⁴ : Algebra A L
inst✝¹³ : IsScalarTower A K L
inst✝¹² : IsScalarTower A B L
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsFractionRing A K
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsFractionRing B L
inst✝³ : IsDedekindDomain A
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e

Tactic:
obtain ⟨b, hb⟩ := hP

Result:
case intro
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²² : CommRing A
inst✝²¹ : Field K
inst✝²⁰ : CommRing B
inst✝¹⁹ : Field L
inst✝¹⁸ : Algebra A K
inst✝¹⁷ : Algebra B L
inst✝¹⁶ : Algebra A B
inst✝¹⁵ : Algebra K L
inst✝¹⁴ : Algebra A L
inst✝¹³ : IsScalarTower A K L
inst✝¹² : IsScalarTower A B L
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsFractionRing A K
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
inst✝⁷ : IsIntegralClosure B A L
inst✝⁶ : IsIntegrallyClosed A
inst✝⁵ : IsDedekindDomain B
inst✝⁴ : IsFractionRing B L
inst✝³ : IsDedekindDomain A
inst✝² : NoZeroSMulDivisors A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
hb : Ideal.map (algebraMap A B) p = P ^ e * b
⊢ Ideal.map (algebraMap A B) p ∣ a ^ e
-- Mathlib/CategoryTheory/Sites/Over.lean
lemma overEquiv_pullback {X : C} {Y₁ Y₂ : Over X} (f : Y₁ ⟶ Y₂) (S : Sieve Y₂) :
    overEquiv _ (S.pullback f) = (overEquiv _ S).pullback f.left

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ ((overEquiv Y₁) (pullback f S)).arrows g ↔ (pullback f.left ((overEquiv Y₂) S)).arrows g

Tactic:
dsimp [overEquiv, Presieve.functorPushforward]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left) ↔ ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ f.left = h ≫ g_1.left

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = b ≫ W.hom

Tactic:
rw [← Over.w a, ← reassoc_of% w, Over.w f]

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left) ↔ ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ f.left = h ≫ g_1.left

Tactic:
constructor

Result:
case h.mp
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left) → ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ f.left = h ≫ g_1.left

case h.mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ f.left = h ≫ g_1.left) → ∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ g_1.left

Proof state:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (c ≫ f)

Tactic:
rw [show c ≫ f = d ≫ a by ext; exact w]

Result:
case h.mpr.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ f.left = b ≫ a.left
T : Over ((Functor.fromPUnit X).obj W.right) := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)
-- Mathlib/GroupTheory/Order/Min.lean
@[to_additive (attr := simp)]
lemma minOrder_eq_top : minOrder α = ⊤ ↔ IsTorsionFree α

Proof state:
α : Type u_1
inst✝ : Monoid α
⊢ minOrder α = ⊤ ↔ IsTorsionFree α

Tactic:
simp [minOrder, IsTorsionFree]

Result:
no goals
-- Mathlib/MeasureTheory/Covering/LiminfLimsup.lean
theorem blimsup_thickening_mul_ae_eq (p : ℕ → Prop) (s : ℕ → Set α) {M : ℝ} (hM : 0 < M) (r : ℕ → ℝ)
    (hr : Tendsto r atTop (𝓝 0)) :
    (blimsup (fun i => thickening (M * r i) (s i)) atTop p : Set α) =ᵐ[μ]
      (blimsup (fun i => thickening (r i) (s i)) atTop p : Set α)

Proof state:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun i => p i ∧ 0 < r i
h₁ : blimsup (fun i => thickening (r i) (s i)) atTop p = blimsup (fun i => thickening (r i) (s i)) atTop q
h₂ : blimsup (fun i => thickening (M * r i) (s i)) atTop p = blimsup (fun i => thickening (M * r i) (s i)) atTop q
⊢ blimsup (fun i => thickening (M * r i) (s i)) atTop q =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop q

Tactic:
exact blimsup_thickening_mul_ae_eq_aux μ q s hM r hr (Eventually.of_forall fun i hi => hi.2)

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.open_eq_iUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}
    (ou : IsOpen u) : ∃ (β : Type u) (f : β → Set α), (u = ⋃ i, f i) ∧ ∀ i, f i ∈ B :=
  ⟨↥({ s ∈ B | s ⊆ u }), (↑), by
    rw [← sUnion_eq_iUnion]
    apply hB.open_eq_sUnion' ou, fun s => And.left s.2⟩

Proof state:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}

Tactic:
apply hB.open_eq_sUnion' ou

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃ i, ↑i

Tactic:
rw [← sUnion_eq_iUnion]

Result:
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
lemma ae_eq_trim_of_stronglyMeasurable (hm : m ≤ m₀) (hf : StronglyMeasurable[m] f)
    (hg : StronglyMeasurable[m] g) (hfg : f =ᵐ[μ] g) : f =ᵐ[μ.trim hm] g

Proof state:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.trim hm)] g

Tactic:
rwa [EventuallyEq, ae_iff, trim_measurableSet_eq hm]

Result:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet {a | ¬f a = g a}

Proof state:
α : Type u_1
E : Type u_5
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
hm : m ≤ m₀
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ MeasurableSet {a | ¬f a = g a}

Tactic:
exact (hf.measurableSet_eq_fun hg).compl

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_triangle (fin : hausdorffEdist s t ≠ ⊤) :
    hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
refine toReal_le_add' hausdorffEdist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist s t ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist t s ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤

Tactic:
exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEdist_triangle

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist s t ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤

Tactic:
rw [hausdorffEdist_comm] at fin

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEdist t s ≠ ⊤
h : ¬hausdorffEdist s u = ⊤
⊢ ¬hausdorffEdist t u = ⊤
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
lemma map_comp (i₁ i₂ i₃ : J) (hi : i₁ ≤ i₂) (hi' : i₂ ≤ i₃) (hi₃ : i₃ ≤ j) :
    map c i₁ i₃ (hi.trans hi') hi₃ =
      map c i₁ i₂ hi (hi'.trans hi₃) ≫
        map c i₂ i₃ hi' hi₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

Tactic:
obtain hi₁₂ | rfl := hi.lt_or_eq

Result:
case inl
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

case inr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃
-- Mathlib/Data/Holor.lean
theorem drop_drop : ∀ t : HolorIndex (ds₁ ++ ds₂ ++ ds₃), t.assocRight.drop.drop = t.drop
  | ⟨is, h⟩ => Subtype.eq (by simp [add_comm, assocRight, drop, cast_type, List.drop_drop])

Proof state:
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 => x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).drop.drop = ↑(drop ⟨is, h⟩)

Tactic:
simp [add_comm, assocRight, drop, cast_type, List.drop_drop]

Result:
no goals