harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem card_norm_le_eq_card_norm_le_add_one (n : ℕ) [CharZero S] :
    Nat.card {I : Ideal S // absNorm I ≤ n} =
      Nat.card {I : (Ideal S)⁰ // absNorm (I : Ideal S) ≤ n} + 1

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I = ⊥ } = 1

Tactic:
rw [Nat.card_unique]

Result:
no goals

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { x // x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n } + 1

Tactic:
simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } = 1

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Tactic:
have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
  (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
I : Ideal S
⊢ ¬((I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) ∧ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n)

Tactic:
tauto

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem open_source' (he : e ∈ c.atlas) : IsOpen[c.toTopologicalSpace] e.source

Proof state:
case a
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source = ↑e ⁻¹' univ ∩ e.source

Tactic:
simp only [Set.univ_inter, Set.preimage_univ]

Result:
no goals

Proof state:
case a
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen s), {↑e ⁻¹' s ∩ e.source}

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Result:
case a
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ∃ i ∈ c.atlas, ∃ i_1, IsOpen i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source

Proof state:
case a
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ ∃ i ∈ c.atlas, ∃ i_1, IsOpen i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source

Tactic:
refine ⟨e, he, univ, isOpen_univ, ?_⟩

Result:
case a
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source = ↑e ⁻¹' univ ∩ e.source

Proof state:
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ IsOpen e.source

Tactic:
apply TopologicalSpace.GenerateOpen.basic

Result:
case a
H : Type u
M : Type u_2
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : PartialEquiv M H
he : e ∈ c.atlas
⊢ e.source ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen s), {↑e ⁻¹' s ∩ e.source}
-- Mathlib/Topology/Algebra/FilterBasis.lean
theorem mem_nhds_one (B : GroupFilterBasis G) {U : Set G} (hU : U ∈ B) :
    U ∈ @nhds G B.topology 1

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i ∈ B, id i ⊆ U

Tactic:
exact ⟨U, hU, rfl.subset⟩

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ U ∈ 𝓝 1

Tactic:
rw [B.nhds_one_hasBasis.mem_iff]

Result:
G : Type u
inst✝ : Group G
B : GroupFilterBasis G
U : Set G
hU : U ∈ B
⊢ ∃ i ∈ B, id i ⊆ U
-- Mathlib/Topology/Category/TopCat/Opens.lean
lemma map_functorObj {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f)
    (U : Opens X) :
    (Opens.map f).obj (hf.functorObj U) = U

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) = U

Tactic:
apply le_antisymm

Result:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) ≤ U

case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)

Proof state:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
hx : x ∈ ↑U
⊢ x ∈ ↑((Opens.map f).obj (hf.functorObj U))

Tactic:
obtain ⟨U, hU⟩ := U

Result:
case a.mk
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
U : Set ↑X
hU : IsOpen U
hx : x ∈ ↑{ carrier := U, is_open' := hU }
⊢ x ∈ ↑((Opens.map f).obj (hf.functorObj { carrier := U, is_open' := hU }))

Proof state:
case a.mk
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
U : Set ↑X
hU : IsOpen U
hx : x ∈ ↑{ carrier := U, is_open' := hU }
⊢ x ∈ ↑((Opens.map f).obj (hf.functorObj { carrier := U, is_open' := hU }))

Tactic:
obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU

Result:
case a.mk.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
hx : x ∈ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
⊢ x ∈ ↑((Opens.map f).obj (hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }))

Proof state:
case a.intro.intro.intro.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
s : Opens ↑Y
hx : (ConcreteCategory.hom f) x ∈ s
⊢ x ∈ ↑((Opens.map f).obj s)

Tactic:
exact hx

Result:
no goals

Proof state:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ U ≤ (Opens.map f).obj (hf.functorObj U)

Tactic:
intros x hx

Result:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
hx : x ∈ ↑U
⊢ x ∈ ↑((Opens.map f).obj (hf.functorObj U))

Proof state:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
⊢ (Opens.map f).obj (hf.functorObj U) ≤ U

Tactic:
rintro x ⟨_, ⟨s, rfl⟩, _, ⟨rfl : _ = U, rfl⟩, hx : f x ∈ s⟩

Result:
case a.intro.intro.intro.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
s : Opens ↑Y
hx : (ConcreteCategory.hom f) x ∈ s
⊢ x ∈ ↑((Opens.map f).obj s)

Proof state:
case a.mk.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
hx : x ∈ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
⊢ x ∈ ↑((Opens.map f).obj (hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }))

Tactic:
exact Opens.mem_sSup.mpr ⟨⟨_, ht⟩, rfl, hx⟩

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- The cardinality of the fiber is preserved under isomorphisms. -/
lemma card_fiber_eq_of_iso {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X) = Nat.card (F.obj Y)

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
i : X ≅ Y
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier

Tactic:
have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)

Result:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
i : X ≅ Y
e : (F.obj X).carrier ≃ (F.obj Y).carrier
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
X Y : C
i : X ≅ Y
e : (F.obj X).carrier ≃ (F.obj Y).carrier
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier

Tactic:
exact Nat.card_eq_of_bijective e (Equiv.bijective e)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_C_mul : (C a * p).eval x = a * p.eval x

Proof state:
case h_add
R : Type u
a : R
inst✝ : Semiring R
p✝ : R[X]
x : R
p q : R[X]
ph : eval x (C a * p) = a * eval x p
qh : eval x (C a * q) = a * eval x q
⊢ eval x (C a * (p + q)) = a * eval x (p + q)

Tactic:
simp only [mul_add, eval_add, ph, qh]

Result:
no goals

Proof state:
case h_monomial
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
b : R
⊢ eval x (C a * (monomial n) b) = a * eval x ((monomial n) b)

Tactic:
simp only [mul_assoc, C_mul_monomial, eval_monomial]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
x : R
⊢ eval x (C a * p) = a * eval x p

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [mul_add, eval_add, ph, qh]
| h_monomial n b =>
  simp only [mul_assoc, C_mul_monomial, eval_monomial]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem iInf_rat_gt_eq (f : StieltjesFunction) (x : ℝ) :
    ⨅ r : { r' : ℚ // x < r' }, f r = f x

Proof state:
f : StieltjesFunction
x : ℝ
⊢ ⨅ r, ↑f ↑↑r = ↑f x

Tactic:
rw [← iInf_Ioi_eq f x]

Result:
f : StieltjesFunction
x : ℝ
⊢ ⨅ r, ↑f ↑↑r = ⨅ r, ↑f ↑r

Proof state:
f : StieltjesFunction
x y : ℝ
⊢ y ∈ ↑f '' Ioi x → ↑f x ≤ y

Tactic:
rintro ⟨y, hy_mem, rfl⟩

Result:
case intro.intro
f : StieltjesFunction
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f y

Proof state:
case intro.intro
f : StieltjesFunction
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f y

Tactic:
exact f.mono (le_of_lt hy_mem)

Result:
no goals

Proof state:
f : StieltjesFunction
x : ℝ
⊢ BddBelow (↑f '' Ioi x)

Tactic:
refine ⟨f x, fun y => ?_⟩

Result:
f : StieltjesFunction
x y : ℝ
⊢ y ∈ ↑f '' Ioi x → ↑f x ≤ y

Proof state:
f : StieltjesFunction
x : ℝ
⊢ ⨅ r, ↑f ↑↑r = ⨅ r, ↑f ↑r

Tactic:
refine (Real.iInf_Ioi_eq_iInf_rat_gt _ ?_ f.mono).symm

Result:
f : StieltjesFunction
x : ℝ
⊢ BddBelow (↑f '' Ioi x)
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_vandermonde_ne_zero_iff [IsDomain R] {n : ℕ} {v : Fin n → R} :
    det (vandermonde v) ≠ 0 ↔ Function.Injective v

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det ≠ 0 ↔ ∀ ⦃a₁ a₂ : Fin n⦄, v a₁ = v a₂ → a₁ = a₂

Tactic:
simp only [det_vandermonde_eq_zero_iff, Ne, not_exists, not_and, Classical.not_not]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det ≠ 0 ↔ Function.Injective v

Tactic:
unfold Function.Injective

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det ≠ 0 ↔ ∀ ⦃a₁ a₂ : Fin n⦄, v a₁ = v a₂ → a₁ = a₂
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem mem_comp_of_mem_ball {V W : Set (β × β)} {x y z : β} (hV : SymmetricRel V)
    (hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ V ○ W

Proof state:
β : Type ub
V W : Set (β × β)
x y z : β
hV : SymmetricRel V
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W

Tactic:
exact ⟨z, hx, hy⟩

Result:
no goals

Proof state:
β : Type ub
V W : Set (β × β)
x y z : β
hV : SymmetricRel V
hx : x ∈ ball z V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W

Tactic:
rw [mem_ball_symmetry hV] at hx

Result:
β : Type ub
V W : Set (β × β)
x y z : β
hV : SymmetricRel V
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean
lemma toPresheaf_map_sheafificationHomEquiv
    {P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
    (f : (sheafification α).obj P ⟶ F) :
    (toPresheaf R₀).map (sheafificationHomEquiv α f) =
      (sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf
        ((SheafOfModules.toSheaf _).obj F) ((SheafOfModules.toSheaf _).map f)

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ (toPresheaf R₀).map ((sheafificationHomEquiv α) f) =
    ((sheafificationAdjunction J AddCommGrp).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F))
      ((SheafOfModules.toSheaf R).map f)

Tactic:
rw [toPresheaf_map_sheafificationHomEquiv_def, Adjunction.homEquiv_unit]

Result:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ CategoryTheory.toSheafify J P.presheaf ≫ (toPresheaf R.val).map f.val =
    (sheafificationAdjunction J AddCommGrp).unit.app P.presheaf ≫
      (sheafToPresheaf J AddCommGrp).map ((SheafOfModules.toSheaf R).map f)

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.val
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrp
inst✝ : HasWeakSheafify J AddCommGrp
P : PresheafOfModules R₀
F : SheafOfModules R
f : (sheafification α).obj P ⟶ F
⊢ CategoryTheory.toSheafify J P.presheaf ≫ (toPresheaf R.val).map f.val =
    (sheafificationAdjunction J AddCommGrp).unit.app P.presheaf ≫
      (sheafToPresheaf J AddCommGrp).map ((SheafOfModules.toSheaf R).map f)

Tactic:
dsimp

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma lintegral_toKernel_mem [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν)
    (a : α) {s : Set (β × ℝ)} (hs : MeasurableSet s) :
    ∫⁻ b, hf.toKernel f (a, b) {y | (b, y) ∈ s} ∂(ν a) = κ a s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a✝, b)) {y | (b, y) ∈ f' i} ∂ν a✝ = (κ a✝) (f' i)
a : β
⊢ {x | (a, x) ∈ ⋃ i, f' i} = ⋃ i, {x | (a, x) ∈ f' i}

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a✝ : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq : ∀ (i : ℕ), ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a✝, b)) {y | (b, y) ∈ f' i} ∂ν a✝ = (κ a✝) (f' i)
a : β
x : ℝ
⊢ x ∈ {x | (a, x) ∈ ⋃ i, f' i} ↔ x ∈ ⋃ i, {x | (a, x) ∈ f' i}

Proof state:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_prod_eq_snd : ∀ a ∈ t₁, {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) {y | (b, y) ∈ (fun x1 x2 => x1 ×ˢ x2) t₁ t₂} ∂ν a =
    (κ a) ((fun x1 x2 => x1 ×ˢ x2) t₁ t₂)

Tactic:
rw [← lintegral_add_compl _ ht₁]

Result:
case basic.intro.intro.intro.intro
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_prod_eq_snd : ∀ a ∈ t₁, {x | (a, x) ∈ t₁ ×ˢ t₂} = t₂
⊢ ∫⁻ (x : β) in t₁, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ (fun x1 x2 => x1 ×ˢ x2) t₁ t₂} ∂ν a +
      ∫⁻ (x : β) in t₁ᶜ, ((IsCondKernelCDF.toKernel f hf) (a, x)) {y | (x, y) ∈ (fun x1 x2 => x1 ×ˢ x2) t₁ t₂} ∂ν a =
    (κ a) ((fun x1 x2 => x1 ×ˢ x2) t₁ t₂)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_val_natCast {n x y : Nat} (h : y = x % (n + 1)):
    @Nat.cast Int instNatCastInt (@Fin.val (n + 1) (OfNat.ofNat x)) = OfNat.ofNat y

Proof state:
n x y : Nat
h : y = x % (n + 1)
⊢ ↑↑(OfNat.ofNat x) = OfNat.ofNat (x % (n + 1))

Tactic:
rfl

Result:
no goals

Proof state:
n x y : Nat
h : y = x % (n + 1)
⊢ ↑↑(OfNat.ofNat x) = OfNat.ofNat y

Tactic:
rw [h]

Result:
n x y : Nat
h : y = x % (n + 1)
⊢ ↑↑(OfNat.ofNat x) = OfNat.ofNat (x % (n + 1))
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem centroid_eq_of_inj_on_of_image_eq {p : ι → P}
    (hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j) {p₂ : ι₂ → P}
    (hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j) (he : p '' ↑s = p₂ '' ↑s₂) :
    s.centroid k p = s₂.centroid k p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' ↑s = p₂ '' ↑s₂
⊢ centroid k s p = centroid k s₂ p₂

Tactic:
rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' ↑s = p₂ '' ↑s₂
⊢ centroid k s p = centroid k s₂ p₂

Tactic:
classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
    s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_def (f : Π₀ i, β i) : f.filter p = mk (f.support.filter p) fun i => f i.1

Proof state:
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
⊢ filter p f = mk (Finset.filter p f.support) fun i => f ↑i

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
⊢ (filter p f) i = (mk (Finset.filter p f.support) fun i => f ↑i) i

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
⊢ (filter p f) i = (mk (Finset.filter p f.support) fun i => f ↑i) i

Tactic:
by_cases h1 : p i <;> by_cases h2 : f i ≠ 0 <;> simp at h2 <;> simp [h1, h2]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem to_rightInverse (hf : AntilipschitzWith K f) {g : β → α} (hg : Function.RightInverse g f) :
    LipschitzWith K g

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

Tactic:
have := hf (g x) (g y)

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

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

Tactic:
rwa [hg x, hg y] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
⊢ LipschitzWith K g

Tactic:
intro x y

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) ≤ ↑K * edist x y
-- Mathlib/Topology/Order.lean
theorem preimage_nhds_coinduced [TopologicalSpace α] {π : α → β} {s : Set β} {a : α}
    (hs : s ∈ @nhds β (TopologicalSpace.coinduced π ‹_›) (π a)) : π ⁻¹' s ∈ 𝓝 a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
V : Set β
hVs : V ⊆ s
V_op : IsOpen V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
letI := TopologicalSpace.coinduced π ‹_›

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
⊢ π ⁻¹' s ∈ 𝓝 a

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
V : Set β
hVs : V ⊆ s
V_op : IsOpen V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a

Tactic:
exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩

Result:
no goals