harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_map {Y} [MeasurableSpace Y] {g : X → Y} {f : Y → E} {s : Set Y}
    (hs : MeasurableSet s) (hf : AEStronglyMeasurable f (Measure.map g μ)) (hg : AEMeasurable g μ) :
    ∫ y in s, f y ∂Measure.map g μ = ∫ x in g ⁻¹' s, f (g x) ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst✝ : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g (μ.restrict (g ⁻¹' s)) ≤ Measure.map g μ

Tactic:
exact Measure.map_mono_of_aemeasurable Measure.restrict_le_self hg

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst✝ : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ ∫ (y : Y) in s, f y ∂Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ

Tactic:
rw [Measure.restrict_map_of_aemeasurable hg hs,
  integral_map (hg.mono_measure Measure.restrict_le_self) (hf.mono_measure _)]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure X
Y : Type u_5
inst✝ : MeasurableSpace Y
g : X → Y
f : Y → E
s : Set Y
hs : MeasurableSet s
hf : AEStronglyMeasurable f (Measure.map g μ)
hg : AEMeasurable g μ
⊢ Measure.map g (μ.restrict (g ⁻¹' s)) ≤ Measure.map g μ
-- Mathlib/Analysis/RCLike/Inner.lean
lemma mul_wInner_left (c : 𝕜) (w : ι → ℝ) (f g : ∀ i, E i) :
    c * ⟪f, g⟫_[𝕜, w] = ⟪star c • f, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
c : 𝕜
w : ι → ℝ
f g : (i : ι) → E i
⊢ c * wInner w f g = wInner w (star c • f) g

Tactic:
rw [wInner_smul_left, star_star, smul_eq_mul]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem comp_right_iff {g : α → β} {e : γ ≃ᵐ α} (h : MeasurePreserving e μc μa) :
    MeasurePreserving (g ∘ e) μc μb ↔ MeasurePreserving g μa μb

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
⊢ MeasurePreserving (g ∘ ⇑e) μc μb ↔ MeasurePreserving g μa μb

Tactic:
refine ⟨fun hg => ?_, fun hg => hg.comp h⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
hg : MeasurePreserving (g ∘ ⇑e) μc μb
⊢ MeasurePreserving g μa μb

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
hg : MeasurePreserving (g ∘ ⇑e) μc μb
⊢ MeasurePreserving g μa μb

Tactic:
convert hg.comp (MeasurePreserving.symm e h)

Result:
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
hg : MeasurePreserving (g ∘ ⇑e) μc μb
⊢ g = (g ∘ ⇑e) ∘ ⇑e.symm

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving (⇑e) μc μa
hg : MeasurePreserving (g ∘ ⇑e) μc μb
⊢ g = (g ∘ ⇑e) ∘ ⇑e.symm

Tactic:
simp [Function.comp_assoc g e e.symm]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.integrable_iInf_rat_gt (hf : IsRatCondKernelCDFAux f κ ν)
    [IsFiniteKernel ν] (a : α) (q : ℚ) :
    Integrable (fun t ↦ ⨅ r : Ioi q, f (a, t) r) (ν a)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ⨅ r, f (a, t) ↑r ≤ 1

Tactic:
refine ciInf_le_of_le ?_ ?_ ?_

Result:
case h.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ BddBelow (range fun r => f (a, t) ↑r)

case h.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ↑(Ioi q)

case h.refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r => f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ f (a, t) ↑?h.refine_2 ≤ 1
-- Mathlib/Data/Multiset/Sections.lean
theorem sections_add (s t : Multiset (Multiset α)) :
    Sections (s + t) = (Sections s).bind fun m => (Sections t).map (m + ·) :=
  Multiset.induction_on s (by simp) fun a s ih => by
    simp [ih, bind_assoc, map_bind, bind_map]

Proof state:
α : Type u_1
s✝ t : Multiset (Multiset α)
a : Multiset α
s : Multiset (Multiset α)
ih : (s + t).Sections = s.Sections.bind fun m => map (fun x => m + x) t.Sections
⊢ (a ::ₘ s + t).Sections = (a ::ₘ s).Sections.bind fun m => map (fun x => m + x) t.Sections

Tactic:
simp [ih, bind_assoc, map_bind, bind_map]

Result:
no goals

Proof state:
α : Type u_1
s t : Multiset (Multiset α)
⊢ (0 + t).Sections = (Sections 0).bind fun m => map (fun x => m + x) t.Sections

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem det_fderivPolarCoordSymm (p : ℝ × ℝ) :
    (fderivPolarCoordSymm p).det = p.1

Proof state:
p : ℝ × ℝ
⊢ cos p.2 * (p.1 * cos p.2) + p.1 * sin p.2 * sin p.2 = (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1

Tactic:
ring

Result:
no goals

Proof state:
p : ℝ × ℝ
⊢ (fderivPolarCoordSymm p).det = (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1

Tactic:
unfold fderivPolarCoordSymm

Result:
p : ℝ × ℝ
⊢ (LinearMap.toContinuousLinearMap
        ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
          !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])).det =
    (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1

Proof state:
p : ℝ × ℝ
⊢ (fderivPolarCoordSymm p).det = p.1

Tactic:
conv_rhs => rw [← one_mul p.1, ← cos_sq_add_sin_sq p.2]

Result:
p : ℝ × ℝ
⊢ (fderivPolarCoordSymm p).det = (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1

Proof state:
p : ℝ × ℝ
⊢ (LinearMap.toContinuousLinearMap
        ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ))
          !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])).det =
    (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1

Tactic:
simp only [neg_mul, LinearMap.det_toContinuousLinearMap, LinearMap.det_toLin,
  Matrix.det_fin_two_of, sub_neg_eq_add]

Result:
p : ℝ × ℝ
⊢ cos p.2 * (p.1 * cos p.2) + p.1 * sin p.2 * sin p.2 = (cos p.2 ^ 2 + sin p.2 ^ 2) * p.1
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp) mod_addOrderOf_nsmul]
lemma pow_mod_orderOf (x : G) (n : ℕ) : x ^ (n % orderOf x) = x ^ n :=
  calc
    x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x))

Tactic:
simp [pow_add, pow_mul, pow_orderOf_eq_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ n

Tactic:
rw [Nat.mod_add_div]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem isMaximal_map_iff_of_bijective : IsMaximal (map f I) ↔ IsMaximal I

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ (map f I).IsMaximal ↔ I.IsMaximal

Tactic:
simpa only [isMaximal_def] using (relIsoOfBijective _ hf).symm.isCoatom_iff _

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Dvr.lean
theorem IsLocalization.isDedekindDomain [IsDedekindDomain A] {M : Submonoid A} (hM : M ≤ A⁰)
    (Aₘ : Type*) [CommRing Aₘ] [IsDomain Aₘ] [Algebra A Aₘ] [IsLocalization M Aₘ] :
    IsDedekindDomain Aₘ

Proof state:
case refine_4.intro.mk
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap Aₘ (FractionRing A)) y = x

Tactic:
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp IsDedekindRing.toIsIntegralClosure hy

Result:
case refine_4.intro.mk.intro
A : Type u_1
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : IsDedekindDomain A
M : Submonoid A
hM : M ≤ A⁰
Aₘ : Type u_2
inst✝³ : CommRing Aₘ
inst✝² : IsDomain Aₘ
inst✝¹ : Algebra A Aₘ
inst✝ : IsLocalization M Aₘ
h : ∀ (y : ↥M), IsUnit ((algebraMap A (FractionRing A)) ↑y)
this✝¹ : Algebra Aₘ (FractionRing A) := (lift h).toAlgebra
this✝ : IsScalarTower A Aₘ (FractionRing A)
this : IsFractionRing Aₘ (FractionRing A)
x : FractionRing A
hx : IsIntegral Aₘ x
y : A
y_mem : y ∈ M
hy : IsIntegral A (⟨y, y_mem⟩ • x)
z : A
hz : (algebraMap A (FractionRing A)) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap Aₘ (FractionRing A)) y = x
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex_subadditive_le [SMul 𝕜 E] {f : E → 𝕜} (hf1 : ∀ x y, f (x + y) ≤ (f x) + (f y))
    (hf2 : ∀ ⦃c⦄ x, 0 ≤ c → f (c • x) ≤ c * f x) (B : 𝕜) :
    Convex 𝕜 { x | f x ≤ B }

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • x + b • y ∈ {x | f x ≤ B}

Tactic:
calc
  _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
  _ ≤ a • B + b • B :=
      add_le_add (smul_le_smul_of_nonneg_left hx ha) (smul_le_smul_of_nonneg_left hy hb)
  _ ≤ B := by rw [← add_smul, hs, one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • B + b • B ≤ B

Tactic:
rw [← add_smul, hs, one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ ∀ ⦃x : E⦄, x ∈ {x | f x ≤ B} → ∀ ⦃y : E⦄, y ∈ {x | f x ≤ B} → [x-[𝕜]y] ⊆ {x | f x ≤ B}

Tactic:
rintro x hx y hy z ⟨a, b, ha, hb, hs, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : x ∈ {x | f x ≤ B}
y : E
hy : y ∈ {x | f x ≤ B}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • x + b • y ∈ {x | f x ≤ B}

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ Convex 𝕜 {x | f x ≤ B}

Tactic:
rw [convex_iff_segment_subset]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedRing 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ ∀ ⦃x : E⦄, x ∈ {x | f x ≤ B} → ∀ ⦃y : E⦄, y ∈ {x | f x ≤ B} → [x-[𝕜]y] ⊆ {x | f x ≤ B}
-- Mathlib/Algebra/BigOperators/Finsupp.lean
@[to_additive]
lemma prod_mul_eq_prod_mul_of_exists [Zero M] [CommMonoid N]
    {f : α →₀ M} {g : α → M → N} {n₁ n₂ : N}
    (a : α) (ha : a ∈ f.support)
    (h : g a (f a) * n₁ = g a (f a) * n₂) :
    f.prod g * n₁ = f.prod g * n₂

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a (f a) * n₁ = g a (f a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
classical
exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : Zero M
inst✝ : CommMonoid N
f : α →₀ M
g : α → M → N
n₁ n₂ : N
a : α
ha : a ∈ f.support
h : g a (f a) * n₁ = g a (f a) * n₂
⊢ f.prod g * n₁ = f.prod g * n₂

Tactic:
exact Finset.prod_mul_eq_prod_mul_of_exists a ha h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem exists_circumsphere_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P}
    (h : ps ⊆ s) [Nonempty s] {n : ℕ} [FiniteDimensional ℝ s.direction]
    (hd : finrank ℝ s.direction = n) (hc : Cospherical ps) :
    ∃ c : Sphere P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumsphere = c

Proof state:
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc✝ : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
c : P
hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
exact ⟨⟨c, r⟩, fun sx hsx => Sphere.ext (hc sx hsx) (hr sx hsx)⟩

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
obtain ⟨r, hr⟩ := exists_circumradius_eq_of_cospherical_subset h hd hc

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
obtain ⟨c, hc⟩ := exists_circumcenter_eq_of_cospherical_subset h hd hc

Result:
case intro.intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc✝ : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
c : P
hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
-- Mathlib/RingTheory/Binomial.lean
theorem descPochhammer_eq_factorial_smul_choose [NatPowAssoc R] (r : R) (n : ℕ) :
    (descPochhammer ℤ n).smeval r = n.factorial • choose r n

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
h : (1 - ↑n).smeval r = 1 - ↑n
⊢ (ascPochhammer ℤ n).smeval (r + (1 - ↑n).smeval r) = (ascPochhammer ℕ n).smeval (r - ↑n + 1)

Tactic:
rw [h, ascPochhammer_smeval_cast, add_comm_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (descPochhammer ℤ n).smeval r = n.factorial • choose r n

Tactic:
rw [choose, factorial_nsmul_multichoose_eq_ascPochhammer, descPochhammer_eq_ascPochhammer,
  smeval_comp, add_comm_sub, smeval_add, smeval_X, npow_one]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ n).smeval (r + (1 - ↑n).smeval r) = (ascPochhammer ℕ n).smeval (r - ↑n + 1)

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (1 - ↑n).smeval r = 1 - ↑n

Tactic:
rw [← C_eq_natCast, ← C_1, ← C_sub, smeval_C]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (1 - ↑n) • r ^ 0 = 1 - ↑n

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (1 - ↑n) • r ^ 0 = 1 - ↑n

Tactic:
simp only [npow_zero, zsmul_one, Int.cast_sub, Int.cast_one, Int.cast_natCast]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ (ascPochhammer ℤ n).smeval (r + (1 - ↑n).smeval r) = (ascPochhammer ℕ n).smeval (r - ↑n + 1)

Tactic:
have h : smeval (1 - n : Polynomial ℤ) r = 1 - n := by
  rw [← C_eq_natCast, ← C_1, ← C_sub, smeval_C]
  simp only [npow_zero, zsmul_one, Int.cast_sub, Int.cast_one, Int.cast_natCast]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
h : (1 - ↑n).smeval r = 1 - ↑n
⊢ (ascPochhammer ℤ n).smeval (r + (1 - ↑n).smeval r) = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem lt_rank_iff {o : Ordinal} : o < rank x ↔ ∃ y ∈ x, o ≤ rank y

Proof state:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
rw [← not_iff_not, not_lt, rank_le_iff]

Result:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ (∀ ⦃y : ZFSet.{u}⦄, y ∈ x → y.rank < o) ↔ ¬∃ y ∈ x, o ≤ y.rank

Proof state:
x : ZFSet.{u}
o : Ordinal.{u}
⊢ (∀ ⦃y : ZFSet.{u}⦄, y ∈ x → y.rank < o) ↔ ¬∃ y ∈ x, o ≤ y.rank

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
@[simp]
lemma powersetCard_nonempty : (powersetCard n s).Nonempty ↔ n ≤ s.card

Proof state:
α : Type u_1
n : ℕ
s : Finset α
⊢ (powersetCard n s).Nonempty ↔ n ≤ #s

Tactic:
aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
@[simp] lemma coeff_natTrailingDegree_eq_zero : coeff p p.natTrailingDegree = 0 ↔ p = 0

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ False

Tactic:
obtain ⟨n, hpn, hn⟩ := by simpa using min_mem_image_coe <| support_nonempty.2 hp

Result:
case mp.intro.intro
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : ↑n = p.support.min
⊢ False

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
⊢ p = 0

Tactic:
by_contra hp

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ False

Proof state:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 → p = 0

Tactic:
rintro h

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
⊢ p = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ ?m.5933

Tactic:
simpa using min_mem_image_coe <| support_nonempty.2 hp

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : ↑n = p.support.min
⊢ False

Tactic:
obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm

Result:
case mp.intro.intro
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
hpn : ¬p.coeff p.natTrailingDegree = 0
hn : ↑p.natTrailingDegree = p.support.min
⊢ False

Proof state:
case mp.intro.intro
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
hpn : ¬p.coeff p.natTrailingDegree = 0
hn : ↑p.natTrailingDegree = p.support.min
⊢ False

Tactic:
exact hpn h

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 ↔ p = 0

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 → p = 0

case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Tactic:
rintro rfl

Result:
case mpr
R : Type u
inst✝ : Semiring R
⊢ coeff 0 (natTrailingDegree 0) = 0

Proof state:
case mpr
R : Type u
inst✝ : Semiring R
⊢ coeff 0 (natTrailingDegree 0) = 0

Tactic:
simp

Result:
no goals