harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem tendsto_approxOn_range_Lp_eLpNorm [BorelSpace E] {f : β → E} (hp_ne_top : p ≠ ∞)
    {μ : Measure β} (fmeas : Measurable f) [SeparableSpace (range f ∪ {0} : Set E)]
    (hf : eLpNorm f p μ < ∞) :
    Tendsto (fun n => eLpNorm (⇑(approxOn f fmeas (range f ∪ {0}) 0 (by simp) n) - f) p μ)
      atTop (𝓝 0)

Proof state:
case refine_1
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})

Tactic:
filter_upwards with x using subset_closure (by simp)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
q : ℝ
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
⊢ eLpNorm (fun x => f x - 0) p μ < ⊤

Tactic:
simpa using hf

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
x : β
⊢ f x ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
⊢ Tendsto (fun n => eLpNorm (⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) - f) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_approxOn_Lp_eLpNorm fmeas _ hp_ne_top ?_ ?_

Result:
case refine_1
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
⊢ ∀ᵐ (x : β) ∂μ, f x ∈ closure (Set.range f ∪ {0})

case refine_2
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp_ne_top : p ≠ ⊤
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : eLpNorm f p μ < ⊤
⊢ eLpNorm (fun x => f x - 0) p μ < ⊤
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblY_smul (P : Fin 3 → R) (u : R) : W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P

Tactic:
simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -((u ^ 4) ^ 3 * W'.negDblY P) - W'.a₁ * ((u ^ 4) ^ 2 * W'.dblX P) * (u ^ 4 * W'.dblZ P) -
      W'.a₃ * (u ^ 4 * W'.dblZ P) ^ 3 =
    (u ^ 4) ^ 3 * (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -((u ^ 4) ^ 3 * W'.negDblY P) - W'.a₁ * ((u ^ 4) ^ 2 * W'.dblX P) * (u ^ 4 * W'.dblZ P) -
      W'.a₃ * (u ^ 4 * W'.dblZ P) ^ 3 =
    (u ^ 4) ^ 3 * (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * W'.dblZ P ^ 3)

Tactic:
ring1

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_succ_comp_X_sub_one (n : ℕ) :
    (descPochhammer R (n + 1)).comp (X - 1) =
      descPochhammer R (n + 1) - (n + (1 : R[X])) • (descPochhammer R n).comp (X - 1)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
this : (descPochhammer ℤ (n + 1)).comp (X - 1) = descPochhammer ℤ (n + 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)
⊢ (descPochhammer R (n + 1)).comp (X - 1) = descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (X - 1)

Tactic:
simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (descPochhammer R (n + 1)).comp (X - 1) = descPochhammer R (n + 1) - (↑n + 1) • (descPochhammer R n).comp (X - 1)

Tactic:
suffices (descPochhammer ℤ (n + 1)).comp (X - 1) =
    descPochhammer ℤ (n + 1) - (n + 1) * (descPochhammer ℤ n).comp (X - 1)
  by simpa [map_comp] using congr_arg (Polynomial.map (Int.castRingHom R)) this

Result:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (descPochhammer ℤ (n + 1)).comp (X - 1) = descPochhammer ℤ (n + 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (descPochhammer ℤ (n + 1)).comp (X - 1) =
    X * (descPochhammer ℤ n).comp (X - 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)

Tactic:
rw [← sub_mul, descPochhammer_succ_right ℤ n, mul_comp, mul_comm, sub_comp, X_comp, natCast_comp]

Result:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (X - 1 - ↑n) * (descPochhammer ℤ n).comp (X - 1) = (X - (↑n + 1)) * (descPochhammer ℤ n).comp (X - 1)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (X - 1 - ↑n) * (descPochhammer ℤ n).comp (X - 1) = (X - (↑n + 1)) * (descPochhammer ℤ n).comp (X - 1)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (descPochhammer ℤ (n + 1)).comp (X - 1) = descPochhammer ℤ (n + 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)

Tactic:
nth_rw 2 [descPochhammer_succ_left]

Result:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (descPochhammer ℤ (n + 1)).comp (X - 1) =
    X * (descPochhammer ℤ n).comp (X - 1) - (↑n + 1) * (descPochhammer ℤ n).comp (X - 1)
-- Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
theorem tmul_one_mul_one_tmul (a₁ : A) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (1 : B) * (1 : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) = (a₁ : A) ᵍ⊗ₜ (b₂ : B)

Proof state:
case h.e'_3.h.e'_17
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
⊢ b₂ = ↑GradedMonoid.GOne.one * b₂

Tactic:
rw [SetLike.coe_gOne, one_mul]

Result:
no goals

Proof state:
case h.e'_3.h.e'_16
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
a₁ : A
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

Tactic:
rw [SetLike.coe_gOne, mul_one]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/LexOrder.lean
theorem lexOrder_def_of_ne_zero {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) :
    ∃ (ne : Set.Nonempty (toLex '' φ.support)),
      lexOrder φ = WithTop.some ((@wellFounded_lt (Lex (σ →₀ ℕ))
        (instLTLex) (Lex.wellFoundedLT)).min (toLex '' φ.support) ne)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ (⇑toLex '' Function.support φ).Nonempty

Tactic:
simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, hφ, not_false_eq_true]

Result:
no goals

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ (if h : φ = 0 then ⊤
    else
      let_fun ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
    ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Tactic:
simp only [dif_neg hφ]

Result:
no goals

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Tactic:
unfold lexOrder

Result:
case h
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ (if h : φ = 0 then ⊤
    else
      let_fun ne := ⋯;
      ↑(⋯.min (⇑toLex '' Function.support φ) ne)) =
    ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Tactic:
suffices ne : Set.Nonempty (toLex '' φ.support) by
  use ne
  unfold lexOrder
  simp only [dif_neg hφ]

Result:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
⊢ (⇑toLex '' Function.support φ).Nonempty

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

Tactic:
use ne

Result:
case h
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
⊢ φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem remainder_lt_aux (p : R[X]) (hq : q ≠ 0) : degree (mod p q) < degree q

Proof state:
R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (q * C q.leadingCoeff⁻¹).degree

Tactic:
exact degree_modByMonic_lt p (monic_mul_leadingCoeff_inv hq)

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < q.degree

Tactic:
rw [← degree_mul_leadingCoeff_inv q hq]

Result:
R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (q * C q.leadingCoeff⁻¹).degree
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem lt_of_lt_of_eq {f g h : CauSeq α abs} (fg : f < g) (gh : g ≈ h) : f < h :=
  show Pos (h - f) by
    convert pos_add_limZero fg (neg_limZero gh) using 1
    simp

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ (h - f).Pos

Tactic:
convert pos_add_limZero fg (neg_limZero gh) using 1

Result:
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)

Proof state:
case h.e'_3
α : Type u_1
inst✝ : LinearOrderedField α
f g h : CauSeq α abs
fg : f < g
gh : g ≈ h
⊢ h - f = g - f + -(g - h)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_transpose [Fintype n] (A : Matrix m n α) (x : n → α) : x ᵥ* Aᵀ = A *ᵥ x

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
⊢ x ᵥ* Aᵀ = A *ᵥ x

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
x✝ : m
⊢ (x ᵥ* Aᵀ) x✝ = (A *ᵥ x) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalCommSemiring α
inst✝ : Fintype n
A : Matrix m n α
x : n → α
x✝ : m
⊢ (x ᵥ* Aᵀ) x✝ = (A *ᵥ x) x✝

Tactic:
apply dotProduct_comm

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem coeff_charpoly_mem_ideal_pow {I : Ideal R} (h : ∀ i j, M i j ∈ I) (k : ℕ) :
    M.charpoly.coeff k ∈ I ^ (Fintype.card n - k)

Proof state:
case h.h
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
⊢ ∀ i ∈ univ, ∀ (k : ℕ), (M.charmatrix (c i) i).coeff k ∈ I ^ (1 - k)

Tactic:
rintro i - (_ | k)

Result:
case h.h.zero
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
⊢ (M.charmatrix (c i) i).coeff 0 ∈ I ^ (1 - 0)

case h.h.succ
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k✝ : ℕ
c : Equiv.Perm n
this : ∑ x : n, 1 = Fintype.card n
i : n
k : ℕ
⊢ (M.charmatrix (c i) i).coeff (k + 1) ∈ I ^ (1 - (k + 1))
-- Mathlib/Data/Setoid/Basic.lean
theorem sSup_eq_eqvGen (S : Set (Setoid α)) :
    sSup S = EqvGen.setoid fun x y => ∃ r : Setoid α, r ∈ S ∧ r x y

Proof state:
α : Type u_1
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} = {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}

Tactic:
ext

Result:
case h
α : Type u_1
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}

Proof state:
case h
α : Type u_1
S : Set (Setoid α)
x✝ : Setoid α
⊢ x✝ ∈ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} ↔
    x✝ ∈ {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}

Tactic:
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩

Result:
no goals

Proof state:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = EqvGen.setoid fun x y => ∃ r ∈ S, r x y

Tactic:
rw [eqvGen_eq]

Result:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}

Proof state:
α : Type u_1
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}

Tactic:
simp only [upperBounds, le_def, and_imp, exists_imp]

Result:
α : Type u_1
S : Set (Setoid α)
⊢ {x | ∀ ⦃a : Setoid α⦄, a ∈ S → ∀ {x_1 y : α}, a x_1 y → x x_1 y} = {s | ∀ ⦃x y : α⦄, ∀ x_1 ∈ S, x_1 x y → s x y}

Proof state:
α : Type u_1
S : Set (Setoid α)
⊢ sSup S = sInf {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}

Tactic:
apply congr_arg sInf

Result:
α : Type u_1
S : Set (Setoid α)
⊢ upperBounds S = {s | ∀ ⦃x y : α⦄, (∃ r ∈ S, r x y) → s x y}
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_disjUnion (h) :
    ∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x1 x2 => x1 * x2) (1 * 1) (fun x => f x) (s₁.disjUnion s₂ h)

Tactic:
rw [one_mul]

Result:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x1 x2 => x1 * x2) 1 (fun x => f x) (s₁.disjUnion s₂ h)

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Tactic:
refine Eq.trans ?_ (fold_disjUnion h)

Result:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x1 x2 => x1 * x2) (1 * 1) (fun x => f x) (s₁.disjUnion s₂ h)

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝ : CommMonoid β
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁.disjUnion s₂ h, f x = fold (fun x1 x2 => x1 * x2) 1 (fun x => f x) (s₁.disjUnion s₂ h)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_toReal_eq_two_mul_add_two_pi {θ : Angle} :
    ((2 : ℕ) • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Proof state:
θ : Angle
h : -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π
⊢ θ.toReal ≤ -π / 2

Tactic:
linarith

Result:
no goals

Proof state:
θ : Angle
⊢ (2 • θ).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
nth_rw 1 [← coe_toReal θ]

Result:
θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Proof state:
θ : Angle
h : θ.toReal ≤ -π / 2
⊢ -3 * π < 2 * θ.toReal

Tactic:
linarith [pi_pos, neg_pi_lt_toReal θ]

Result:
no goals

Proof state:
θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2

Tactic:
refine
  ⟨fun h => by linarith, fun h =>
    ⟨by linarith [pi_pos, neg_pi_lt_toReal θ], (le_div_iff₀' (zero_lt_two' ℝ)).1 h⟩⟩

Result:
no goals

Proof state:
θ : Angle
⊢ (2 • ↑θ.toReal).toReal = 2 * θ.toReal + 2 * π ↔ θ.toReal ≤ -π / 2

Tactic:
rw [← coe_nsmul, two_nsmul, ← two_mul, toReal_coe_eq_self_add_two_pi_iff, Set.mem_Ioc]

Result:
θ : Angle
⊢ -3 * π < 2 * θ.toReal ∧ 2 * θ.toReal ≤ -π ↔ θ.toReal ≤ -π / 2
-- Mathlib/Data/Set/Prod.lean
theorem range_const_eq_diagonal {α β : Type*} [hβ : Nonempty β] :
    range (const α) = {f : α → β | ∀ x y, f x = f y}

Proof state:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
⊢ ∃ a, const α a = f

Tactic:
rcases isEmpty_or_nonempty α with h|⟨⟨a⟩⟩

Result:
case inl
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
h : IsEmpty α
⊢ ∃ a, const α a = f

case inr.intro
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f

Proof state:
α : Type u_1
β : Type u_2
hβ : Nonempty β
⊢ range (const α) = {f | ∀ (x y : α), f x = f y}

Tactic:
refine (range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
⊢ ∃ a, const α a = f

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
a : α
⊢ ∃ a, const α a = f

Tactic:
exact ⟨f a, funext fun x ↦ hf _ _⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
hβ : Nonempty β
f : α → β
hf : f ∈ {f | ∀ (x y : α), f x = f y}
h : IsEmpty α
⊢ ∃ a, const α a = f

Tactic:
exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩

Result:
no goals
-- Mathlib/Probability/Kernel/Proper.lean
lemma IsProper.setLIntegral_eq_comp (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧) {μ : Measure[𝓧] X}
    (hA : MeasurableSet[𝓧] A) (hB : MeasurableSet[𝓑] B) :
    ∫⁻ a in B, π a A ∂μ = (π ∘ₘ μ) (A ∩ B)

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = ∫⁻ (a : X), (π a) (A ∩ B) ∂μ

Tactic:
simp only [hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, ← indicator_mul_const, Pi.one_apply, one_mul]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = ∫⁻ (a : X), B.indicator (fun x => (π a) A) a ∂μ

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = (⇑π ∘ₘ μ) (A ∩ B)

Tactic:
rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl)]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = ∫⁻ (a : X), (π a) (A ∩ B) ∂μ

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ MeasurableSet (A ∩ B)

Tactic:
measurability

Result:
no goals

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = ∫⁻ (a : X), B.indicator (fun x => (π a) A) a ∂μ

Tactic:
rw [← lintegral_indicator (h𝓑𝓧 _ hB)]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X), B.indicator (fun a => (π a) A) a ∂μ = ∫⁻ (a : X), B.indicator (fun x => (π a) A) a ∂μ

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X), B.indicator (fun a => (π a) A) a ∂μ = ∫⁻ (a : X), B.indicator (fun x => (π a) A) a ∂μ

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/PathCategory/Basic.lean
theorem lift_toPath {C} [Category C] (φ : V ⥤q C) {X Y : V} (f : X ⟶ Y) :
    (lift φ).map f.toPath = φ.map f

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f

Tactic:
simp

Result:
no goals

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map f.toPath = φ.map f

Tactic:
dsimp [Quiver.Hom.toPath, lift]

Result:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem invOf_fromBlocks_zero₂₁_eq (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α)
    [Invertible A] [Invertible D] [Invertible (fromBlocks A B 0 D)] :
    ⅟ (fromBlocks A B 0 D) = fromBlocks (⅟ A) (-(⅟ A * B * ⅟ D)) 0 (⅟ D)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D

Tactic:
convert (rfl : ⅟ (fromBlocks A B 0 D) = _)

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D

Tactic:
letI := fromBlocksZero₂₁Invertible A B D

Result:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A B 0 D)
this : Invertible (fromBlocks A B 0 D) := A.fromBlocksZero₂₁Invertible B D
⊢ ⅟(fromBlocks A B 0 D) = fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D