harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/Complex.lean
theorem Complex.uniformContinuous_ringHom_eq_id_or_conj (K : Subfield ℂ) {ψ : K →+* ℂ}
    (hc : UniformContinuous ψ) : ψ.toFun = K.subtype ∨ ψ.toFun = conj ∘ K.subtype

Proof state:
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrict r = j (ι x)
⊢ (↑↑ψ).toFun x = K.subtype x

Tactic:
have :=
  RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r

Result:
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrict r = j (ι x)
this : ψ₁ r = ofRealHom r
⊢ (↑↑ψ).toFun x = K.subtype x

Proof state:
case h.e'_2
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = ψ₁ ↑z

Tactic:
exact (IsDenseInducing.extend_eq di hc.continuous z).symm

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma withDensity_one_sub_rnDerivAux (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
    withDensity (κ + η) (fun a x ↦ Real.toNNReal (1 - rnDerivAux κ (κ + η) a x)) = η

Proof state:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
⊢ Measurable (Function.uncurry fun a x => 1)

Tactic:
exact measurable_const

Result:
no goals

Proof state:
case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
⊢ ∀ (a : α), (fun x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᶠ[ae ((κ + η) a)] fun x => 1

Tactic:
intro a

Result:
case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b
a : α
⊢ (fun x => ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᶠ[ae ((κ + η) a)] fun x => 1
-- Mathlib/Algebra/Polynomial/Eval/Algebra.lean
theorem eval₂_comp' : eval₂ (algebraMap R S) x (p.comp q) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p

Proof state:
case h_add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q r s : R[X]
hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r
hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s
⊢ eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)

Tactic:
simp only [add_comp, eval₂_add, hr, hs]

Result:
no goals

Proof state:
case h_monomial
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
n : ℕ
a : R
⊢ eval₂ (algebraMap R S) x (((monomial n) a).comp q) =
    eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) ((monomial n) a)

Tactic:
simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q : R[X]
⊢ eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p

Tactic:
induction p using Polynomial.induction_on' with
| h_add r s hr hs => simp only [add_comp, eval₂_add, hr, hs]
| h_monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow']

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_mul_X_self (j : σ) (f : MvPolynomial σ R) :
    degreeOf j (f * X j) ≤ degreeOf j f + 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1

Tactic:
apply (Multiset.count_le_of_le j degrees_mul_le).trans

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f.degrees + (X j).degrees) ≤ Multiset.count j f.degrees + 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f.degrees + (X j).degrees) ≤ Multiset.count j f.degrees + 1

Tactic:
simp only [Multiset.count_add, add_le_add_iff_left]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (X j).degrees ≤ 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (X j).degrees ≤ 1

Tactic:
convert Multiset.count_le_of_le j <| degrees_X' j

Result:
case h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1

Tactic:
classical
simp only [degreeOf]
apply (Multiset.count_le_of_le j degrees_mul_le).trans
simp only [Multiset.count_add, add_le_add_iff_left]
convert Multiset.count_le_of_le j <| degrees_X' j
rw [Multiset.count_singleton_self]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1

Tactic:
simp only [degreeOf]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ Multiset.count j (f * X j).degrees ≤ Multiset.count j f.degrees + 1

Proof state:
case h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}

Tactic:
rw [Multiset.count_singleton_self]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
lemma Algebra.baseChange_lmul {R B : Type*} [CommSemiring R] [Semiring B] [Algebra R B]
    {A : Type*} [CommSemiring A] [Algebra R A] (f : B) :
    (Algebra.lmul R B f).baseChange A = Algebra.lmul A (A ⊗[R] B) (1 ⊗ₜ f)

Proof state:
case a.h.h
R : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring B
inst✝² : Algebra R B
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f i : B
⊢ ((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B) f))) 1) i =
    ((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f))) 1) i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring B
inst✝² : Algebra R B
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : B
⊢ LinearMap.baseChange A ((lmul R B) f) = (lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f)

Tactic:
ext i

Result:
case a.h.h
R : Type u_1
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring B
inst✝² : Algebra R B
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f i : B
⊢ ((AlgebraTensorModule.curry (LinearMap.baseChange A ((lmul R B) f))) 1) i =
    ((AlgebraTensorModule.curry ((lmul A (A ⊗[R] B)) (1 ⊗ₜ[R] f))) 1) i
-- Mathlib/Topology/Sheaves/Presheaf.lean
theorem map_restrict
    {F G : X.Presheaf C} (e : F ⟶ G) {U V : Opens X} (h : U ≤ V) (x : ToType (F.obj (op V))) :
    e.app _ (x |_ U) = e.app _ x |_ U

Proof state:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : ToType (F.obj (op V))
⊢ (ConcreteCategory.hom (e.app (op U))) ((x |_ U) h) = ((ConcreteCategory.hom (e.app (op V))) x |_ U) h

Tactic:
delta restrictOpen restrict

Result:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : ToType (F.obj (op V))
⊢ (ConcreteCategory.hom (e.app (op U))) ((ConcreteCategory.hom (F.map (homOfLE h).op)) x) =
    (ConcreteCategory.hom (G.map (homOfLE h).op)) ((ConcreteCategory.hom (e.app (op V))) x)

Proof state:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : ToType (F.obj (op V))
⊢ (ConcreteCategory.hom (e.app (op U))) ((ConcreteCategory.hom (F.map (homOfLE h).op)) x) =
    (ConcreteCategory.hom (G.map (homOfLE h).op)) ((ConcreteCategory.hom (e.app (op V))) x)

Tactic:
rw [← ConcreteCategory.comp_apply, NatTrans.naturality, ConcreteCategory.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Expr.toPoly_denote (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx

Proof state:
case var
ctx : Context
v : Var
⊢ Poly.denote ctx (var v).toPoly = denote ctx (var v)

Tactic:
simp!

Result:
no goals

Proof state:
ctx : Context
e : Expr
⊢ Poly.denote ctx e.toPoly = denote ctx e

Tactic:
induction e with
| num k =>
  simp!; by_cases h : k == 0 <;> simp! [*]
  simp [eq_of_beq h]
| var v => simp!
| add a b => simp! [Poly.add_denote, *]
| mul a b => simp! [Poly.mul_denote, *]

Result:
no goals

Proof state:
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (num k).toPoly = denote ctx (num k)

Tactic:
simp!

Result:
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (bif k == 0 then [] else [(k, [])]) = k

Proof state:
case mul
ctx : Context
a b : Expr
a_ih✝ : Poly.denote ctx a.toPoly = denote ctx a
b_ih✝ : Poly.denote ctx b.toPoly = denote ctx b
⊢ Poly.denote ctx (a.mul b).toPoly = denote ctx (a.mul b)

Tactic:
simp! [Poly.mul_denote, *]

Result:
no goals

Proof state:
case add
ctx : Context
a b : Expr
a_ih✝ : Poly.denote ctx a.toPoly = denote ctx a
b_ih✝ : Poly.denote ctx b.toPoly = denote ctx b
⊢ Poly.denote ctx (a.add b).toPoly = denote ctx (a.add b)

Tactic:
simp! [Poly.add_denote, *]

Result:
no goals

Proof state:
case pos
ctx : Context
k : Nat
h : (k == 0) = true
⊢ 0 = k

Tactic:
simp [eq_of_beq h]

Result:
no goals

Proof state:
case num
ctx : Context
k : Nat
⊢ Poly.denote ctx (bif k == 0 then [] else [(k, [])]) = k

Tactic:
by_cases h : k == 0 <;> simp! [*]

Result:
case pos
ctx : Context
k : Nat
h : (k == 0) = true
⊢ 0 = k
-- Mathlib/Algebra/Order/Algebra.lean
theorem algebraMap_monotone : Monotone (algebraMap R A) := fun a b h => by
  rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]
  trans (b - a) • (0 : A)
  · simp
  · exact smul_le_smul_of_nonneg_left zero_le_one (sub_nonneg.mpr h)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 1

Tactic:
trans (b - a) • (0 : A)

Result:
R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 0

R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ (b - a) • 0 ≤ (b - a) • 1

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ (algebraMap R A) a ≤ (algebraMap R A) b

Tactic:
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, ← sub_nonneg, ← sub_smul]

Result:
R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ 0 ≤ (b - a) • 1

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : OrderedCommRing R
inst✝² : OrderedRing A
inst✝¹ : Algebra R A
inst✝ : OrderedSMul R A
a b : R
h : a ≤ b
⊢ (b - a) • 0 ≤ (b - a) • 1

Tactic:
exact smul_le_smul_of_nonneg_left zero_le_one (sub_nonneg.mpr h)

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem nodup_finRange (n : ℕ) : (finRange n).Nodup

Proof state:
n : ℕ
⊢ (pmap Fin.mk (range n) ⋯).Nodup

Tactic:
exact (Pairwise.pmap (nodup_range n) _) fun _ _ _ _ => @Fin.ne_of_val_ne _ ⟨_, _⟩ ⟨_, _⟩

Result:
no goals

Proof state:
n : ℕ
⊢ (finRange n).Nodup

Tactic:
rw [finRange_eq_pmap_range]

Result:
n : ℕ
⊢ (pmap Fin.mk (range n) ⋯).Nodup
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc (attr := simp)]
lemma Spec_map_stalkMap_fromSpecStalk {x} :
    Spec.map (f.stalkMap x) ≫ Y.fromSpecStalk _ = X.fromSpecStalk x ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) = X.fromSpecStalk x ≫ f

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open Y).exists_subset_of_mem_open
  (Set.mem_univ (f.base x)) isOpen_univ

Result:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) = X.fromSpecStalk x ≫ f

Proof state:
case intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) = X.fromSpecStalk x ≫ f

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open
  hxU (f ⁻¹ᵁ U).2

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) = X.fromSpecStalk x ≫ f

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : (ConcreteCategory.hom f.base) x ∈ ↑U
V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk ((ConcreteCategory.hom f.base) x) = X.fromSpecStalk x ≫ f

Tactic:
rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
  IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.stalkMap_germ f _ x hxU,
  IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
  Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
    Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.Spec_map_appLE_fromSpec]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
theorem AEStronglyMeasurable.ae_integrable_condKernel_iff {f : α × Ω → F}
    (hf : AEStronglyMeasurable f ρ) :
    (∀ᵐ a ∂ρ.fst, Integrable (fun ω ↦ f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a ↦ ∫ ω, ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔ Integrable f ρ

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Result:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)

Tactic:
rw [Measure.integrable_compProd_iff hf]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f ρ
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f ρ

Tactic:
rw [← ρ.disintegrate ρ.condKernel] at hf

Result:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst, Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
      Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
    Integrable f ρ
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorZero_hom_app_f (K : CochainComplex C ℤ) (n : ℤ) :
    ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [add_zero])).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
this : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
rw [← cancel_mono (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n), ← comp_f,
  Iso.hom_inv_id_app, id_f, shiftFunctorZero_inv_app_f]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
this : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)
⊢ 𝟙 (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 0).obj K).X n) = (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n + 0 = n

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
⊢ IsIso (XIsoOfEq K ⋯).hom

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
this : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)
⊢ 𝟙 (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 0).obj K).X n) = (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom

Tactic:
simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans, eqToHom_refl]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n + { as := 0 }.as = n

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n + 0 = n

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
have : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n) := by
  rw [shiftFunctorZero_inv_app_f]
  infer_instance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
this : IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)
⊢ ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K).f n = (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
⊢ IsIso (((shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n)

Tactic:
rw [shiftFunctorZero_inv_app_f]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
⊢ IsIso (XIsoOfEq K ⋯).hom
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
lemma of_yoneda_arrow {Y : C} {η : yoneda.obj Y ⟶ A} {X : C} {s : yoneda.obj X ⟶ A} {f : X ⟶ Y}
    (hf : yoneda.map f ≫ η = s) : MakesOverArrow η s f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
f : X ⟶ Y
hf : yoneda.map f ≫ η = s
⊢ MakesOverArrow η s f

Tactic:
simpa only [yonedaEquiv_yoneda_map f] using of_arrow hf

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Basic.lean
lemma homOfEq_injective {X X' Y Y' : V} (hX : X = X') (hY : Y = Y')
    {f g : X ⟶ Y} (h : Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY) : f = g

Proof state:
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
h : homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯
⊢ f = g

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u_1
inst✝ : Quiver V
X X' Y Y' : V
hX : X = X'
hY : Y = Y'
f g : X ⟶ Y
h : homOfEq f hX hY = homOfEq g hX hY
⊢ f = g

Tactic:
subst hX hY

Result:
V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
h : homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯
⊢ f = g