harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem functorPullback_pushforward_covering [G.IsCoverDense K] [G.IsLocallyFull K] {X : C}
    (T : K (G.obj X)) : (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X)

Proof state:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
D : Type u_2
inst✝² : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K (G.obj X)

Tactic:
refine K.transitive T.2 _ fun Y iYX hiYX ↦ ?_

Result:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
D : Type u_2
inst✝² : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
⊢ Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)) ∈ K Y

Proof state:
C : Type u_1
inst✝³ : Category.{u_5, u_1} C
D : Type u_2
inst✝² : Category.{u_6, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.functorPullback G ↑T).arrows iVX

Tactic:
simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_empty {c} : (empty c : Raw α β).isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
c : Nat
⊢ (empty c).isEmpty = true

Tactic:
simp_to_raw using Raw₀.isEmpty_empty

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem absConvexHull_nonempty : (absConvexHull 𝕜 s).Nonempty ↔ s.Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ ((absConvexHull 𝕜) s).Nonempty ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne, Ne]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ ¬(absConvexHull 𝕜) s = ∅ ↔ ¬s = ∅

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ ¬(absConvexHull 𝕜) s = ∅ ↔ ¬s = ∅

Tactic:
exact not_congr absConvexHull_eq_empty

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem induction_on' {C : M ∗ N → Prop} (m : M ∗ N)
    (one : C 1)
    (inl_mul : ∀ m x, C x → C (inl m * x))
    (inr_mul : ∀ n x, C x → C (inr n * x)) : C m

Proof state:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
x : FreeMonoid (M ⊕ N)
⊢ C (mk x)

Tactic:
induction x using FreeMonoid.inductionOn' with
| one => exact one
| mul_of x xs ih =>
  cases x with
  | inl m => simpa using inl_mul m _ ih
  | inr n => simpa using inr_mul n _ ih

Result:
no goals

Proof state:
case intro.mul_of.inl
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : C (mk xs)
m : M
⊢ C (mk (of (Sum.inl m) * xs))

Tactic:
simpa using inl_mul m _ ih

Result:
no goals

Proof state:
case intro.one
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
⊢ C (mk 1)

Tactic:
exact one

Result:
no goals

Proof state:
case intro.mul_of
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
x : M ⊕ N
xs : FreeMonoid (M ⊕ N)
ih : C (mk xs)
⊢ C (mk (of x * xs))

Tactic:
cases x with
| inl m => simpa using inl_mul m _ ih
| inr n => simpa using inr_mul n _ ih

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
m : M ∗ N
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
⊢ C m

Tactic:
rcases mk_surjective m with ⟨x, rfl⟩

Result:
case intro
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
x : FreeMonoid (M ⊕ N)
⊢ C (mk x)

Proof state:
case intro.mul_of.inr
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
C : M ∗ N → Prop
one : C 1
inl_mul : ∀ (m : M) (x : M ∗ N), C x → C (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), C x → C (inr n * x)
xs : FreeMonoid (M ⊕ N)
ih : C (mk xs)
n : N
⊢ C (mk (of (Sum.inr n) * xs))

Tactic:
simpa using inr_mul n _ ih

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem ContinuousMul.of_nhds_one {M : Type u} [Monoid M] [TopologicalSpace M]
    (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) <| 𝓝 1)
    (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1))
    (hright : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) : ContinuousMul M :=
  ⟨by
    rw [continuous_iff_continuousAt]
    rintro ⟨x₀, y₀⟩
    have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) =
        ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·)

Proof state:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (uncurry fun x1 x2 => x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)

Tactic:
simp (config := { unfoldPartialApp := true }) only [uncurry]

Result:
M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p => x₀ * p.1 * (p.2 * y₀)) = ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry fun x1 x2 => x1 * x2
key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x
⊢ map (fun a => a.1 * a.2) (𝓝 x₀ ×ˢ 𝓝 y₀) = map (fun p => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1)
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem list_prod_mem_list_prod (t : List ι) (f : ι → Set α) (g : ι → α) (hg : ∀ i ∈ t, g i ∈ f i) :
    (t.map g).prod ∈ (t.map f).prod

Proof state:
case nil
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
hg : ∀ i ∈ [], g i ∈ f i
⊢ (List.map g []).prod ∈ (List.map f []).prod

Tactic:
simp_rw [List.map_nil, List.prod_nil, Set.mem_one]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : List ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ (List.map g t).prod ∈ (List.map f t).prod

Tactic:
induction' t with h tl ih

Result:
case nil
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
hg : ∀ i ∈ [], g i ∈ f i
⊢ (List.map g []).prod ∈ (List.map f []).prod

case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : (∀ i ∈ tl, g i ∈ f i) → (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ (List.map g (h :: tl)).prod ∈ (List.map f (h :: tl)).prod

Proof state:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : (∀ i ∈ tl, g i ∈ f i) → (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod

Tactic:
exact mul_mem_mul (hg h <| List.mem_cons_self _ _)
  (ih fun i hi ↦ hg i <| List.mem_cons_of_mem _ hi)

Result:
no goals

Proof state:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : (∀ i ∈ tl, g i ∈ f i) → (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ (List.map g (h :: tl)).prod ∈ (List.map f (h :: tl)).prod

Tactic:
simp_rw [List.map_cons, List.prod_cons]

Result:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
h : ι
tl : List ι
ih : (∀ i ∈ tl, g i ∈ f i) → (List.map g tl).prod ∈ (List.map f tl).prod
hg : ∀ i ∈ h :: tl, g i ∈ f i
⊢ g h * (List.map g tl).prod ∈ f h * (List.map f tl).prod
-- Mathlib/Algebra/QuaternionBasis.lean
theorem k_mul_i : q.k * q.i = -c₁ • q.j

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.i = -c₁ • q.j

Tactic:
rw [← i_mul_j, mul_assoc, j_mul_i, mul_sub, i_mul_k, neg_smul, mul_smul_comm, i_mul_j]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • q.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • q.k - (c₁ • q.j + c₂ • q.k) = -(c₁ • q.j)

Tactic:
linear_combination (norm := module)

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem mem_kernMap_iff_compl {s : Set β} : s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ

Proof state:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ

Tactic:
rw [kernImage_compl, compl_eq_comm, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ x, xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
refine exists_congr (fun x ↦ and_congr_right fun _ ↦ ?_)

Result:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ kernImage m xᶜ = s ↔ m '' x = sᶜ

Proof state:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ s ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ

Tactic:
rw [mem_kernMap, compl_surjective.exists]

Result:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ (∃ x, xᶜ ∈ f ∧ kernImage m xᶜ = s) ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
-- Mathlib/Algebra/Ring/Invertible.lean
theorem Ring.inverse_add_inverse [Semiring α] {a b : α} (h : IsUnit a ↔ IsUnit b) :
    Ring.inverse a + Ring.inverse b = Ring.inverse a * (a + b) * Ring.inverse b

Proof state:
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
by_cases ha : IsUnit a

Result:
case pos
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

case neg
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Proof state:
case neg
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
have hb := h.not.mp ha

Result:
case neg
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Proof state:
case pos.intro.intro
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
simp_rw [inverse_invertible, invOf_add_invOf]

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
have hb := h.mp ha

Result:
case pos
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Proof state:
case pos
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
obtain ⟨ia⟩ := ha.nonempty_invertible

Result:
case pos.intro
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Proof state:
case pos.intro
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
obtain ⟨ib⟩ := hb.nonempty_invertible

Result:
case pos.intro.intro
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Proof state:
case neg
α : Type u
inst✝ : Semiring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ inverse a + inverse b = inverse a * (a + b) * inverse b

Tactic:
simp [inverse_non_unit, ha, hb]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Layercake.lean
theorem Integrable.integral_eq_integral_meas_lt
    (f_intble : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
    ∫ ω, f ω ∂μ = ∫ t in Set.Ioi 0, ENNReal.toReal (μ {a : α | t < f a})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal

Tactic:
have lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞ := Integrable.lintegral_lt_top f_intble

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤
⊢ ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem zero_shiftRight : ∀ n, 0 >>> n = 0
  | 0 => by simp [shiftRight]
  | n + 1 => by simp [shiftRight, zero_shiftRight n, shiftRight_succ]

Proof state:
⊢ 0 >>> 0 = 0

Tactic:
simp [shiftRight]

Result:
no goals

Proof state:
n : Nat
⊢ 0 >>> (n + 1) = 0

Tactic:
simp [shiftRight, zero_shiftRight n, shiftRight_succ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem mul_adjMatrix_apply [NonAssocSemiring α] (M : Matrix V V α) (v w : V) :
    (M * G.adjMatrix α) v w = ∑ u ∈ G.neighborFinset w, M v u

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (M * adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v u

Tactic:
simp [mul_apply, neighborFinset_eq_filter, sum_filter, adj_comm]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_natDegree (n : ℕ) [NoZeroDivisors R] [Nontrivial R] :
    (descPochhammer R n).natDegree = n

Proof state:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n✝ : ℕ
hn : (descPochhammer R (n✝ + 1)).natDegree = n✝ + 1
this : (X - ↑(n✝ + 1)).natDegree = 1
⊢ descPochhammer R (n✝ + 1) ≠ 0

Tactic:
refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Result:
no goals

Proof state:
case zero
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hn : (descPochhammer R 0).natDegree = 0
this : (X - ↑0).natDegree = 1
⊢ descPochhammer R 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case zero
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (descPochhammer R 0).natDegree = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
n : ℕ
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (descPochhammer R n).natDegree = n

Tactic:
induction' n with n hn

Result:
case zero
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (descPochhammer R 0).natDegree = 0

case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Proof state:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Tactic:
have : natDegree (X - (n : R[X])) = 1 := natDegree_X_sub_C (n : R)

Result:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Proof state:
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ descPochhammer R n ≠ 0

Tactic:
cases n

Result:
case zero
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
hn : (descPochhammer R 0).natDegree = 0
this : (X - ↑0).natDegree = 1
⊢ descPochhammer R 0 ≠ 0

case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n✝ : ℕ
hn : (descPochhammer R (n✝ + 1)).natDegree = n✝ + 1
this : (X - ↑(n✝ + 1)).natDegree = 1
⊢ descPochhammer R (n✝ + 1) ≠ 0

Proof state:
case succ
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ (descPochhammer R (n + 1)).natDegree = n + 1

Tactic:
rw [descPochhammer_succ_right,
    natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]

Result:
R : Type u
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
n : ℕ
hn : (descPochhammer R n).natDegree = n
this : (X - ↑n).natDegree = 1
⊢ descPochhammer R n ≠ 0
-- Mathlib/Data/List/Basic.lean
theorem mem_getLast?_cons {x y : α} : ∀ {l : List α}, x ∈ l.getLast? → x ∈ (y :: l).getLast?
  | [], _ => by contradiction
  | _ :: _, h => h

Proof state:
α : Type u
x y : α
x✝ : x ∈ [].getLast?
⊢ x ∈ [y].getLast?

Tactic:
contradiction

Result:
no goals
-- Mathlib/Analysis/NormedSpace/FunctionSeries.lean
theorem continuousOn_tsum [TopologicalSpace β] {f : α → β → F} {s : Set β}
    (hf : ∀ i, ContinuousOn (f i) s) (hu : Summable u) (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) :
    ContinuousOn (fun x => ∑' n, f n x) s

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) s

Tactic:
classical
  refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Eventually.of_forall ?_)
  intro t
  exact continuousOn_finset_sum _ fun i _ => hf i

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn (fun x => ∑ n ∈ t, f n x) s

Tactic:
exact continuousOn_finset_sum _ fun i _ => hf i

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ∀ (x : Finset α), ContinuousOn (fun x_1 => ∑ n ∈ x, f n x_1) s

Tactic:
intro t

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
t : Finset α
⊢ ContinuousOn (fun x => ∑ n ∈ t, f n x) s

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) s

Tactic:
refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Eventually.of_forall ?_)

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ∀ (x : Finset α), ContinuousOn (fun x_1 => ∑ n ∈ x, f n x_1) s
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_succ' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) :
    X.σ i ≫ X.δ j = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ X.σ i ≫ X.δ j = 𝟙 (X _⦋n⦌)

Tactic:
subst H

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.succ = 𝟙 (X _⦋n⦌)

Tactic:
rw [δ_comp_σ_succ]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem Right.one_le_pow_of_le (hx : 1 ≤ x) : ∀ {n : ℕ}, 1 ≤ x ^ n
  | 0 => (pow_zero _).ge
  | n + 1 => by
    rw [pow_succ]
    exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x

Tactic:
exact Right.one_le_mul (Right.one_le_pow_of_le hx) hx

Result:
no goals

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ (n + 1)

Tactic:
rw [pow_succ]

Result:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulRightMono M
x : M
hx : 1 ≤ x
n : ℕ
⊢ 1 ≤ x ^ n * x
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma lintegral_tilted (f : α → ℝ) (g : α → ℝ≥0∞) :
    ∫⁻ x, g x ∂(μ.tilted f)
      = ∫⁻ x, ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ) * (g x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
⊢ ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
rw [← setLIntegral_univ, setLIntegral_tilted' f g MeasurableSet.univ, setLIntegral_univ]

Result:
no goals