harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/Jacobian.lean
lemma _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul'
    {f : ℝ → ℝ} (hf : MeasurableEmbedding f) {s : Set ℝ} (hs : MeasurableSet s)
    {f' : ℝ → ℝ} (hf' : ∀ x, HasDerivAt f (f' x) x)
    {g : ℝ → ℝ} (hg : 0 ≤ᵐ[volume] g) (hg_int : Integrable g) :
    (volume.withDensity (fun x ↦ ENNReal.ofReal (g x))).comap f s
      = ENNReal.ofReal (∫ x in s, |f' x| * g (f x)) :=
  hf.withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul hs
    (by filter_upwards [hg] with x hx using fun _ ↦ hx) hg_int.integrableOn
    (fun x _ => (hf' x).hasDerivWithinAt)

Proof state:
f : ℝ → ℝ
hf : MeasurableEmbedding f
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt f (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae volume] g
hg_int : Integrable g volume
⊢ ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x

Tactic:
filter_upwards [hg] with x hx using fun _ ↦ hx

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsion_eq_bot : torsion R (M ⧸ torsion R M) = ⊥ :=
  eq_bot_iff.mpr fun z =>
    Quotient.inductionOn' z fun x ⟨a, hax⟩ => by
      rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax
      rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]
      obtain ⟨b, h⟩ := hax
      exact ⟨b * a, (mul_smul _ _ _).trans h⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ x ∈ torsion R M

Tactic:
obtain ⟨b, h⟩ := hax

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a b : ↥R⁰
h : b • a • x = 0
⊢ x ∈ torsion R M

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a b : ↥R⁰
h : b • a • x = 0
⊢ x ∈ torsion R M

Tactic:
exact ⟨b * a, (mul_smul _ _ _).trans h⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥

Tactic:
rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ x ∈ torsion R M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • Quotient.mk'' x = 0
⊢ Quotient.mk'' x ∈ ⊥

Tactic:
rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥
-- Mathlib/Topology/UniformSpace/Compact.lean
theorem nhdsSet_diagonal_eq_uniformity [CompactSpace α] : 𝓝ˢ (diagonal α) = 𝓤 α

Proof state:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Tactic:
refine (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => ?_

Result:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ diagonal α, ball x ((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α

Proof state:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Tactic:
have :
  (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
    (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U := by
  rw [uniformity_prod_eq_comap_prod]
  exact (𝓤 α).basis_sets.prod_self.comap _

Result:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Proof state:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ 𝓝ˢ (diagonal α) = 𝓤 α

Tactic:
refine nhdsSet_diagonal_le_uniformity.antisymm ?_

Result:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Proof state:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ diagonal α, ball x ((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α

Tactic:
exact mem_of_superset hU fun ⟨x, y⟩ hxy => mem_iUnion₂.2
  ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩

Result:
no goals

Proof state:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
rw [uniformity_prod_eq_comap_prod]

Result:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ (Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
    (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Proof state:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
⊢ (Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
    (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
exact (𝓤 α).basis_sets.prod_self.comap _

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem finsuppTotal_apply (f : ι →₀ I) :
    finsuppTotal ι M I v f = f.sum fun i x => (x : R) • v i

Proof state:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0

Tactic:
exact fun _ => zero_smul _ _

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (Finsupp.linearCombination R v) (Finsupp.mapRange Subtype.val ⋯ f) = f.sum fun i x => ↑x • v i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]

Result:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0

Proof state:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (finsuppTotal ι M I v) f = f.sum fun i x => ↑x • v i

Tactic:
dsimp [finsuppTotal]

Result:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ (Finsupp.linearCombination R v) (Finsupp.mapRange Subtype.val ⋯ f) = f.sum fun i x => ↑x • v i
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem X_pow_comp {k : ℕ} : (X ^ k).comp p = p ^ k

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (X ^ k).comp p = p ^ k

Tactic:
induction k with
| zero => simp
| succ k ih => simp [pow_succ, mul_X_comp, ih]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (X ^ 0).comp p = p ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
ih : (X ^ k).comp p = p ^ k
⊢ (X ^ (k + 1)).comp p = p ^ (k + 1)

Tactic:
simp [pow_succ, mul_X_comp, ih]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem powerset_singleton (x : α) : 𝒫({x} : Set α) = {∅, {x}}

Proof state:
α : Type u
x : α
⊢ 𝒫{x} = {∅, {x}}

Tactic:
ext y

Result:
case h
α : Type u
x : α
y : Set α
⊢ y ∈ 𝒫{x} ↔ y ∈ {∅, {x}}

Proof state:
case h
α : Type u
x : α
y : Set α
⊢ y ∈ 𝒫{x} ↔ y ∈ {∅, {x}}

Tactic:
rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem ringHom_ext {f1 f2 : K →+* L}
    (hf : ∀ x : A, f1 (algebraMap A K x) = f2 (algebraMap A K x)) : f1 = f2

Proof state:
case a
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
z : K
⊢ f1 z = f2 z

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) z

Result:
case a.intro.intro.intro
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
x y : A
hy : y ∈ nonZeroDivisors A
⊢ f1 ((algebraMap A K) x / (algebraMap A K) y) = f2 ((algebraMap A K) x / (algebraMap A K) y)

Proof state:
case a.intro.intro.intro
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
x y : A
hy : y ∈ nonZeroDivisors A
⊢ f1 ((algebraMap A K) x / (algebraMap A K) y) = f2 ((algebraMap A K) x / (algebraMap A K) y)

Tactic:
rw [map_div₀, map_div₀, hf, hf]

Result:
no goals

Proof state:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
⊢ f1 = f2

Tactic:
ext z

Result:
case a
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
z : K
⊢ f1 z = f2 z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_ediv_of_dvd : ∀ {a b : Int}, b ∣ a → (-a) / b = -(a / b)
  | _, b, ⟨c, rfl⟩ => by
    by_cases bz : b = 0
    · simp [bz]
    · rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]

Proof state:
b c : Int
⊢ -(b * c) / b = -(b * c / b)

Tactic:
by_cases bz : b = 0

Result:
case pos
b c : Int
bz : b = 0
⊢ -(b * c) / b = -(b * c / b)

case neg
b c : Int
bz : ¬b = 0
⊢ -(b * c) / b = -(b * c / b)

Proof state:
case pos
b c : Int
bz : b = 0
⊢ -(b * c) / b = -(b * c / b)

Tactic:
simp [bz]

Result:
no goals

Proof state:
case neg
b c : Int
bz : ¬b = 0
⊢ -(b * c) / b = -(b * c / b)

Tactic:
rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma le_of_forall_lt_iff_le {x y : EReal} : (∀ z : ℝ, x < z → y ≤ z) ↔ y ≤ x

Proof state:
x y : EReal
h : ∀ (z : ℝ), x < ↑z → y ≤ ↑z
⊢ ∀ (z : WithTop ℝ), x < ↑z → y ≤ ↑z

Tactic:
rw [WithTop.forall]

Result:
x y : EReal
h : ∀ (z : ℝ), x < ↑z → y ≤ ↑z
⊢ (x < ↑⊤ → y ≤ ↑⊤) ∧ ∀ (x_1 : ℝ), x < ↑↑x_1 → y ≤ ↑↑x_1

Proof state:
x y : EReal
⊢ (∀ (z : ℝ), x < ↑z → y ≤ ↑z) ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ WithBot.le_of_forall_lt_iff_le.1 ?_, fun h _ x_z ↦ h.trans x_z.le⟩

Result:
x y : EReal
h : ∀ (z : ℝ), x < ↑z → y ≤ ↑z
⊢ ∀ (z : WithTop ℝ), x < ↑z → y ≤ ↑z

Proof state:
x y : EReal
h : ∀ (z : ℝ), x < ↑z → y ≤ ↑z
⊢ (x < ↑⊤ → y ≤ ↑⊤) ∧ ∀ (x_1 : ℝ), x < ↑↑x_1 → y ≤ ↑↑x_1

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_of_eq_mul'' (h : a = c * b) : a / b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a / b = c

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_set_exists : ∃ C, 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C

Tactic:
rcases isBounded_iff.1 (f.isBounded_range.union g.isBounded_range) with ⟨C, hC⟩

Result:
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C

Proof state:
case intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
hC : ∀ ⦃x : β⦄, x ∈ range ⇑f ∪ range ⇑g → ∀ ⦃y : β⦄, y ∈ range ⇑f ∪ range ⇑g → dist x y ≤ C
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C

Tactic:
refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩
  <;> [left; right]
  <;> apply mem_range_self

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
/-- Values of an absolute value on the rationals are determined by the values on the natural
numbers. -/
lemma eq_on_nat_iff_eq : (∀ n : ℕ , f n = g n) ↔ f = g

Proof state:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
⊢ f = g

Tactic:
ext1 z

Result:
case a
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f z = g z

Proof state:
case a
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
z : ℚ
⊢ f z = g z

Tactic:
rw [← Rat.num_div_den z, map_div₀, map_div₀, h, eq_on_nat_iff_eq_on_int.mp h]

Result:
no goals

Proof state:
f g : AbsoluteValue ℚ ℝ
⊢ (∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g

Tactic:
refine ⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩

Result:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
⊢ f = g
-- Mathlib/Data/List/Basic.lean
theorem head!_mem_self [Inhabited α] {l : List α} (h : l ≠ nil) : l.head! ∈ l

Proof state:
α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
⊢ l.head! ∈ l

Tactic:
rwa [cons_head!_tail h] at h'

Result:
no goals

Proof state:
α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l

Tactic:
have h' := mem_cons_self l.head! l.tail

Result:
α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
⊢ l.head! ∈ l
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem symm_trans_target_eq (e e' : Pretrivialization F proj) :
    (e.toPartialEquiv.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e e' : Pretrivialization F proj
⊢ (e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ univ

Tactic:
rw [← PartialEquiv.symm_source, symm_trans_symm, symm_trans_source_eq, inter_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem _root_.AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
    (f : AlgebraicGeometry.Scheme.Hom X Y) [H : IsOpenImmersion f] {U : X.Opens} :
    IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U

Proof state:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ ⇑(ConcreteCategory.hom f.base) '' Set.range ⇑(ConcreteCategory.hom (X.ofRestrict ⋯).base) =
    Set.range ⇑(ConcreteCategory.hom (Y.ofRestrict ⋯).base)

Tactic:
dsimp [Opens.coe_inclusion', Scheme.restrict]

Result:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ ⇑(ConcreteCategory.hom f.base) '' Set.range Subtype.val = Set.range Subtype.val

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsAffineOpen (f ''ᵁ U) ↔ IsAffineOpen U

Tactic:
refine ⟨fun hU => @isAffine_of_isIso _ _
  (IsOpenImmersion.isoOfRangeEq (X.ofRestrict U.isOpenEmbedding ≫ f) (Y.ofRestrict _) ?_).hom
    ?_ hU, fun hU => hU.image_of_isOpenImmersion f⟩

Result:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ Set.range ⇑(ConcreteCategory.hom (X.ofRestrict ⋯ ≫ f).base) = Set.range ⇑(ConcreteCategory.hom (Y.ofRestrict ⋯).base)

case refine_2
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ IsIso (IsOpenImmersion.isoOfRangeEq (X.ofRestrict ⋯ ≫ f) (Y.ofRestrict ⋯) ?refine_1).hom

Proof state:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ Set.range ⇑(ConcreteCategory.hom (X.ofRestrict ⋯ ≫ f).base) = Set.range ⇑(ConcreteCategory.hom (Y.ofRestrict ⋯).base)

Tactic:
rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp]

Result:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ ⇑(ConcreteCategory.hom f.base) '' Set.range ⇑(ConcreteCategory.hom (X.ofRestrict ⋯).base) =
    Set.range ⇑(ConcreteCategory.hom (Y.ofRestrict ⋯).base)

Proof state:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ ⇑(ConcreteCategory.hom f.base) '' Set.range Subtype.val = Set.range Subtype.val

Tactic:
rw [Subtype.range_coe, Subtype.range_coe]

Result:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ ⇑(ConcreteCategory.hom f.base) '' ↑U = ↑(f ''ᵁ U)

Proof state:
case refine_1
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ ⇑(ConcreteCategory.hom f.base) '' ↑U = ↑(f ''ᵁ U)

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen (f ''ᵁ U)
⊢ IsIso (IsOpenImmersion.isoOfRangeEq (X.ofRestrict ⋯ ≫ f) (Y.ofRestrict ⋯) ⋯).hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem liftpPreservation_iff_uniform : q.LiftpPreservation ↔ q.IsUniform

Proof state:
F : Type u → Type u
q : QPF F
⊢ LiftpPreservation ↔ IsUniform

Tactic:
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_uniform]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem mk_subset_mk_lt_cof {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) :
    #{ s : Set α // #s < cof (#α).ord } = #α

Proof state:
case inr.intro.intro.a.refine_1
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
x : α
⊢ #↑{x} < (#α).ord.cof

Tactic:
rw [mk_singleton]

Result:
case inr.intro.intro.a.refine_1
α : Type u_1
h : ∀ x < #α, 2 ^ x < #α
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : IsWellOrder α r
x : α
⊢ 1 < (#α).ord.cof
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem comap_coe_nhdsGT_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s) :
    comap ((↑) : s → α) (𝓝[>] a) = atBot

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
⊢ (⇑ofDual ⁻¹' s).Nonempty → ∃ a_2, toDual a_2 < toDual a ∧ ⇑ofDual ⁻¹' Ioo a a_2 ⊆ ⇑ofDual ⁻¹' s

Tactic:
exact hs

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
⊢ (⇑ofDual ⁻¹' s).Nonempty → ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Tactic:
simp only [OrderDual.exists, dual_Ioo]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
⊢ (⇑ofDual ⁻¹' s).Nonempty → ∃ a_2, toDual a_2 < toDual a ∧ ⇑ofDual ⁻¹' Ioo a a_2 ⊆ ⇑ofDual ⁻¹' s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
⊢ comap Subtype.val (𝓝[>] a) = atBot

Tactic:
apply comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha)

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
⊢ (⇑ofDual ⁻¹' s).Nonempty → ∃ a_2 < toDual a, Ioo a_2 (toDual a) ⊆ ⇑ofDual ⁻¹' s
-- Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
theorem eq_on_inv₀ [MonoidWithZeroHomClass F' G₀ M₀'] (f g : F') (h : f a = g a) :
    f a⁻¹ = g a⁻¹

Proof state:
case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ f 0⁻¹ = g 0⁻¹

Tactic:
rw [inv_zero, map_zero, map_zero]

Result:
no goals

Proof state:
case inr
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
ha : a ≠ 0
⊢ f a⁻¹ = g a⁻¹

Tactic:
exact (IsUnit.mk0 a ha).eq_on_inv f g h

Result:
no goals

Proof state:
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
⊢ f a⁻¹ = g a⁻¹

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f 0 = g 0
⊢ f 0⁻¹ = g 0⁻¹

case inr
G₀ : Type u_3
M₀' : Type u_4
F' : Type u_7
inst✝³ : GroupWithZero G₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : FunLike F' G₀ M₀'
a : G₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f g : F'
h : f a = g a
ha : a ≠ 0
⊢ f a⁻¹ = g a⁻¹
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_smul_measure_of_ne_top {p : ℝ≥0∞} (hp_ne_top : p ≠ ∞) (f : α → F) (c : ℝ≥0∞) :
    eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
hp_ne_top : p ≠ ⊤
f : α → F
c : ℝ≥0∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
hp_ne_top : p ≠ ⊤
f : α → F
c : ℝ≥0∞
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
hp_ne_top : p ≠ ⊤
f : α → F
c : ℝ≥0∞
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
hp_ne_top : p ≠ ⊤
f : α → F
c : ℝ≥0∞
hp0 : ¬p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_ne_top c

Result:
no goals

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
hp_ne_top : p ≠ ⊤
f : α → F
c : ℝ≥0∞
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp [hp0]

Result:
no goals