harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Constructible.lean
lemma IsLocallyConstructible.finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X}
    (ht : ∀ i ∈ s, IsLocallyConstructible (t i)) : IsLocallyConstructible (s.inf t)

Proof state:
case empty
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
ht : ∀ i ∈ ∅, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (∅.inf t)

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons i s ih hi =>
  rw [Finset.inf_cons]
  exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp

Result:
no goals

Proof state:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible (t i ⊓ s.inf t)

Tactic:
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht

Result:
no goals

Proof state:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible ((Finset.cons i s ih).inf t)

Tactic:
rw [Finset.inf_cons]

Result:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ IsLocallyConstructible (t i ⊓ s.inf t)
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_mul_left_one_sub_of_lt_order (d : σ →₀ ℕ) (h : degree d < g.order) :
    coeff R d (f * (1 - g)) = coeff R d f

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑d.degree < g.order
⊢ (coeff R d) (f * (1 - g)) = (coeff R d) f

Tactic:
rw [degree_eq_weight_one] at h

Result:
σ : Type u_1
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x => 1) d) < g.order
⊢ (coeff R d) (f * (1 - g)) = (coeff R d) f

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight fun x => 1) d) < g.order
⊢ (coeff R d) (f * (1 - g)) = (coeff R d) f

Tactic:
exact coeff_mul_left_one_sub_of_lt_weightedOrder _ h

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
@[simp]
lemma localized'_top : (⊤ : Submodule R M).localized' S p f = ⊤ :=
  SetLike.ext' (by apply SetLike.ext'_iff.mp <| Submodule.localized₀_top p f)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ↑(localized' S p f ⊤) = ↑⊤

Tactic:
apply SetLike.ext'_iff.mp <| Submodule.localized₀_top p f

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.double_even (a b c : ℕ) (r : ℤ) (ha : a % 4 = 0) (hb : b % 2 = 1)
    (hc : a / 4 = c) (hr : jacobiSymNat c b = r) : jacobiSymNat a b = r

Proof state:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.ofNat_ediv, Nat.cast_ofNat]

Result:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 4) b

Proof state:
a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = jacobiSym (↑a / 4) b

Tactic:
exact (jacobiSym.div_four_left (mod_cast ha) hb).symm

Result:
no goals
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem ODE_solution_unique_of_mem_Icc_right
    (hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t))
    (hf : ContinuousOn f (Icc a b))
    (hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t)
    (hfs : ∀ t ∈ Ico a b, f t ∈ s t)
    (hg : ContinuousOn g (Icc a b))
    (hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t)
    (hgs : ∀ t ∈ Ico a b, g t ∈ s t)
    (ha : f a = g a) :
    EqOn f g (Icc a b) := fun t ht ↦ by
  have := dist_le_of_trajectories_ODE_of_mem hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
  rwa [zero_mul, dist_le_zero] at this

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
⊢ f t = g t

Tactic:
have := dist_le_of_trajectories_ODE_of_mem hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * rexp (↑K * (t - a))
⊢ f t = g t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * rexp (↑K * (t - a))
⊢ f t = g t

Tactic:
rwa [zero_mul, dist_le_zero] at this

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_isProbabilityMeasure {s : Set Ω} (hs : s.Finite) (hs' : s.Nonempty) :
    IsProbabilityMeasure (uniformOn s)

Proof state:
case hs
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ ⊤

Tactic:
exact (Measure.count_apply_lt_top.2 hs).ne

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ IsProbabilityMeasure (uniformOn s)

Tactic:
apply cond_isProbabilityMeasure_of_finite

Result:
case hcs
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ 0

case hs
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ ⊤

Proof state:
case hcs
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ 0

Tactic:
rwa [Measure.count_ne_zero_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem sinh_arsinh (x : ℝ) : sinh (arsinh x) = x

Proof state:
x : ℝ
⊢ sinh (arsinh x) = x

Tactic:
rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]

Result:
x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x

Proof state:
x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x

Tactic:
field_simp

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem rank_eq_one_of_commute_of_flat_of_self_of_inj (H : A.LinearDisjoint A) [Module.Flat R A]
    (hc : ∀ (a b : A), Commute a.1 b.1)
    (hinj : Function.Injective (algebraMap R S)) : Module.rank R A = 1

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Module.Flat R ↥A
hc : ∀ (a b : ↥A), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥A = 1

Tactic:
rw [← inf_of_le_left (le_refl A)] at hc ⊢

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Module.Flat R ↥A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥(A ⊓ A) = 1

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
A : Subalgebra R S
H : A.LinearDisjoint A
inst✝ : Module.Flat R ↥A
hc : ∀ (a b : ↥(A ⊓ A)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
⊢ Module.rank R ↥(A ⊓ A) = 1

Tactic:
exact H.rank_inf_eq_one_of_commute_of_flat_left_of_inj hc hinj

Result:
no goals
-- Mathlib/Topology/Algebra/UniformConvergence.lean
theorem UniformOnFun.hasBasis_nhds_one_of_basis (𝔖 : Set <| Set α) (h𝔖₁ : 𝔖.Nonempty)
    (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {b : ι → Set G}
    (h : (𝓝 1 : Filter G).HasBasis p b) :
    (𝓝 1 : Filter (α →ᵤ[𝔖] G)).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
      { f : α →ᵤ[𝔖] G | ∀ x ∈ Si.1, toFun 𝔖 f x ∈ b Si.2 }

Proof state:
case h.e'_5.h.h.e'_2.h.a
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : Set α × ι
x✝ : α →ᵤ[𝔖] G
⊢ (∀ x ∈ x✝¹.1, (toFun 𝔖) x✝ x ∈ b x✝¹.2) ↔ (x✝, 1) ∈ UniformOnFun.gen 𝔖 x✝¹.1 {x | x.1 / x.2 ∈ b x✝¹.2}

Tactic:
simp [UniformOnFun.gen]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
⊢ (𝓝 1).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (toFun 𝔖) f x ∈ b Si.2}

Tactic:
convert UniformOnFun.hasBasis_nhds_of_basis α _ 𝔖 (1 : α →ᵤ[𝔖] G) h𝔖₁ h𝔖₂ <|
  h.uniformity_of_nhds_one_swapped

Result:
case h.e'_5.h.h.e'_2.h.a
α : Type u_1
G : Type u_2
ι : Type u_3
inst✝² : Group G
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
𝔖 : Set (Set α)
h𝔖₁ : 𝔖.Nonempty
h𝔖₂ : DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖
p : ι → Prop
b : ι → Set G
h : (𝓝 1).HasBasis p b
x✝¹ : Set α × ι
x✝ : α →ᵤ[𝔖] G
⊢ (∀ x ∈ x✝¹.1, (toFun 𝔖) x✝ x ∈ b x✝¹.2) ↔ (x✝, 1) ∈ UniformOnFun.gen 𝔖 x✝¹.1 {x | x.1 / x.2 ∈ b x✝¹.2}
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem lift_fieldRange (hg : Injective g) :
    (lift hg : K →+* L).fieldRange = Subfield.closure g.range :=
  ringHom_fieldRange_eq_of_comp_eq (by ext; simp)

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
g : A →+* L
hg : Injective ⇑g
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
ext

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
g : A →+* L
hg : Injective ⇑g
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝

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
g : A →+* L
hg : Injective ⇑g
x✝ : A
⊢ ((lift hg).comp (algebraMap A K)) x✝ = g x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_comm (hr : Symmetric r) (s t : Finset α) :
    edgeDensity r s t = edgeDensity r t s

Proof state:
α : Type u_4
r : α → α → Prop
inst✝ : DecidableRel r
hr : Symmetric r
s t : Finset α
⊢ edgeDensity r s t = edgeDensity r t s

Tactic:
rw [edgeDensity, mul_comm, card_interedges_comm hr, edgeDensity]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
theorem orbitRel.Quotient.orbit_eq_orbit_out (x : orbitRel.Quotient G α)
    {φ : orbitRel.Quotient G α → α} (hφ : letI := orbitRel G α; RightInverse φ Quotient.mk') :
    orbitRel.Quotient.orbit x = MulAction.orbit G (φ x)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ x.orbit = MulAction.orbit G (φ x)

Tactic:
conv_lhs => rw [← hφ x]

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ orbit (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
φ : Quotient G α → α
hφ : RightInverse φ Quotient.mk'
⊢ orbit (Quotient.mk' (φ x)) = MulAction.orbit G (φ x)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_const [CompleteSpace E] (c : E) : ∫ _ in a..b, c = (b - a) • c

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
c : E
⊢ ∫ (x : ℝ) in a..b, c = (b - a) • c

Tactic:
simp only [integral_const', Real.volume_Ioc, ENNReal.toReal_ofReal', ← neg_sub b,
  max_zero_sub_eq_self]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem QuotientAddGroup.norm_eq_infDist {S : AddSubgroup M} (x : M ⧸ S) :
    ‖x‖ = infDist 0 { m : M | (m : M ⧸ S) = x }

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
⊢ ‖x‖ = infDist 0 {m | ↑m = x}

Tactic:
simp only [AddSubgroup.quotient_norm_eq, infDist_eq_iInf, sInf_image', dist_zero_left]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_div_of_nonpos_of_le (hc : c ≤ 0) (h : b ≤ a) : a / c ≤ b / c

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a / c ≤ b / c

Tactic:
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a * (1 / c) ≤ b * (1 / c)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c ≤ 0
h : b ≤ a
⊢ a * (1 / c) ≤ b * (1 / c)

Tactic:
exact mul_le_mul_of_nonpos_right h (one_div_nonpos.2 hc)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_zpow {n : ℤ} (h : 0 ≤ n ∨ n ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
    ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1)

Proof state:
a b : ℝ
n : ℤ
h : -1 < ↑n ∨ ↑n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
exact mod_cast integral_rpow h

Result:
no goals

Proof state:
a b : ℝ
n : ℤ
h : 0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)

Tactic:
replace h : -1 < (n : ℝ) ∨ (n : ℝ) ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]] := mod_cast h

Result:
a b : ℝ
n : ℤ
h : -1 < ↑n ∨ ↑n ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_cancel_right (m : M) (s₁ s₂ : S) : mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₁)

Tactic:
rw [LocalizedModule.mk_cancel_common_right]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) =
    (fromLocalizedModule S f) (LocalizedModule.mk m s₁)
-- Mathlib/Data/Seq/Computation.lean
theorem exists_of_mem_map {f : α → β} {b : β} {s : Computation α} (h : b ∈ map f s) :
    ∃ a, a ∈ s ∧ f a = b

Proof state:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
rw [← bind_pure] at h

Result:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b

Proof state:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
let ⟨a, as, fb⟩ := exists_of_mem_bind h

Result:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
a : α
as : a ∈ s
fb : b ∈ (pure ∘ f) a
⊢ ∃ a, a ∈ s ∧ f a = b

Proof state:
α : Type u
β : Type v
f : α → β
b : β
s : Computation α
h : b ∈ s.bind (pure ∘ f)
a : α
as : a ∈ s
fb : b ∈ (pure ∘ f) a
⊢ ∃ a, a ∈ s ∧ f a = b

Tactic:
exact ⟨a, as, mem_unique (ret_mem _) fb⟩

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem add_one_le_ceil_iff : z + 1 ≤ ⌈a⌉ ↔ (z : α) < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z + 1 ≤ ⌈a⌉ ↔ ↑z < a

Tactic:
rw [← lt_ceil, add_one_le_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integrable_kernel_prod_mk_left (a : α) {s : Set (β × γ)} (hs : MeasurableSet s)
    (h2s : (κ ⊗ₖ η) a s ≠ ∞) : Integrable (fun b => (η (a, b) (Prod.mk b ⁻¹' s)).toReal) (κ a)

Proof state:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
⊢ AEStronglyMeasurable (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)

Tactic:
exact (measurable_kernel_prod_mk_left' hs a).ennreal_toReal.aestronglyMeasurable

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
⊢ Integrable (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)

Tactic:
constructor

Result:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
⊢ AEStronglyMeasurable (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)

case right
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
⊢ HasFiniteIntegral (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)

Proof state:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
⊢ HasFiniteIntegral (fun b => ((η (a, b)) (Prod.mk b ⁻¹' s)).toReal) (κ a)

Tactic:
exact hasFiniteIntegral_prod_mk_left a h2s

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem radical_of_prime {a : M} (ha : Prime a) : radical a = normalize a

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ {normalize a}.toFinset.prod id = normalize a

Tactic:
simp only [Multiset.toFinset_singleton, id, Finset.prod_singleton]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ (normalizedFactors a).toFinset.prod id = normalize a

Tactic:
rw [normalizedFactors_irreducible ha.irreducible]

Result:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ {normalize a}.toFinset.prod id = normalize a

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ radical a = normalize a

Tactic:
rw [radical, primeFactors]

Result:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
⊢ (normalizedFactors a).toFinset.prod id = normalize a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_pos_iff {a : α} {l : List α} : 0 < count a l ↔ a ∈ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ 0 < count a l ↔ a ∈ l

Tactic:
simp only [count, countP_pos_iff, beq_iff_eq, exists_eq_right]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ici_eq_cons_Ioi (a : α) : Ici a = (Ioi a).cons a not_mem_Ioi_self

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) ⋯

Tactic:
classical rw [cons_eq_insert, Ioi_insert]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) ⋯

Tactic:
rw [cons_eq_insert, Ioi_insert]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLE_comp_ofLE {B : C} (X Y Z : Subobject B) (h₁ : X ≤ Y) (h₂ : Y ≤ Z) :
    ofLE X Y h₁ ≫ ofLE Y Z h₂ = ofLE X Z (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ underlying.map (h₁.hom ≫ h₂.hom) = underlying.map ⋯.hom

Tactic:
congr 1

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ X.ofLE Y h₁ ≫ Y.ofLE Z h₂ = X.ofLE Z ⋯

Tactic:
simp only [ofLE, ← Functor.map_comp underlying]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y Z : Subobject B
h₁ : X ≤ Y
h₂ : Y ≤ Z
⊢ underlying.map (h₁.hom ≫ h₂.hom) = underlying.map ⋯.hom