harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem isPiSystem_Ioo_rat :
    IsPiSystem (⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo (a : ℝ) (b : ℝ)})

Proof state:
⊢ IsPiSystem (⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b})

Tactic:
convert isPiSystem_Ioo ((↑) : ℚ → ℝ) ((↑) : ℚ → ℝ)

Result:
case h.e'_2

⊢ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} = {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}

Proof state:
case h.e'_2

⊢ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} = {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}

Tactic:
ext x

Result:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} ↔ x ∈ {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}

Proof state:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} ↔ x ∈ {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) :
    x / y ≤ z ↔ x ≤ z * y

Proof state:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ⊤
⊢ x / y ≤ z ↔ x ≤ z * y

Tactic:
rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem idxOf_le_length {a : α} {l : List α} : idxOf a l ≤ length l

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
⊢ (if b = a then 0 else idxOf a l + 1) ≤ l.length + 1

Tactic:
by_cases h : b = a

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : b = a
⊢ (if b = a then 0 else idxOf a l + 1) ≤ l.length + 1

case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : ¬b = a
⊢ (if b = a then 0 else idxOf a l + 1) ≤ l.length + 1

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : ¬b = a
⊢ idxOf a l + 1 ≤ l.length + 1

Tactic:
exact succ_le_succ ih

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : b = a
⊢ 0 ≤ l.length + 1

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
⊢ idxOf a l ≤ l.length

Tactic:
induction' l with b l ih

Result:
case nil
α : Type u
inst✝ : DecidableEq α
a : α
⊢ idxOf a [] ≤ [].length

case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
⊢ idxOf a (b :: l) ≤ (b :: l).length

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
⊢ idxOf a (b :: l) ≤ (b :: l).length

Tactic:
simp only [length, idxOf_cons, cond_eq_if, beq_iff_eq]

Result:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
⊢ (if b = a then 0 else idxOf a l + 1) ≤ l.length + 1

Proof state:
case nil
α : Type u
inst✝ : DecidableEq α
a : α
⊢ idxOf a [] ≤ [].length

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : ¬b = a
⊢ (if b = a then 0 else idxOf a l + 1) ≤ l.length + 1

Tactic:
rw [if_neg h]

Result:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : ¬b = a
⊢ idxOf a l + 1 ≤ l.length + 1

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : b = a
⊢ (if b = a then 0 else idxOf a l + 1) ≤ l.length + 1

Tactic:
rw [if_pos h]

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
ih : idxOf a l ≤ l.length
h : b = a
⊢ 0 ≤ l.length + 1
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/-- Two morphisms of sheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `yoneda.obj X ⟶ P` agree. -/
lemma hom_ext_yonedaULift {P Q : Sheaf J (Type (max v v'))} {f g : P ⟶ Q}
    (h : ∀ (X : C) (p : J.yonedaULift.obj X ⟶ P), p ≫ f = p ≫ g) :
    f = g

Proof state:
case h.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (yonedaULift.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.val.obj X
⊢ f.val.app X x = g.val.app X x

Tactic:
simpa only [yonedaULiftEquiv_comp, Equiv.apply_symm_apply]
  using congr_arg (J.yonedaULiftEquiv) (h _ (J.yonedaULiftEquiv.symm x))

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (yonedaULift.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x

Result:
case h.w.h.h
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (yonedaULift.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.val.obj X
⊢ f.val.app X x = g.val.app X x
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type*) [Semiring S] (n k : ℕ) :
    (ascPochhammer S k).eval (n : S) = n.ascFactorial k

Proof state:
S : Type u_1
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval n (ascPochhammer ℕ k)) = ↑(n.ascFactorial k)

Tactic:
rw [ascPochhammer_nat_eq_ascFactorial]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semiring S
n k : ℕ
⊢ eval (↑n) (ascPochhammer S k) = ↑(n.ascFactorial k)

Tactic:
norm_cast

Result:
S : Type u_1
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval n (ascPochhammer ℕ k)) = ↑(n.ascFactorial k)
-- Mathlib/Data/Sym/Basic.lean
theorem mem_fill_iff {a b : α} {i : Fin (n + 1)} {s : Sym α (n - i)} :
    a ∈ Sym.fill b i s ↔ (i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s

Proof state:
α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s

Tactic:
rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem traverse_map {α β γ : Type u} (g : α → β) (f : β → G γ) (x : σ ⊕ α) :
    Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

Proof state:
σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

Tactic:
cases x <;> simp [Sum.traverse, id_map, functor_norm] <;> rfl

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem t2_iff_nhds : T2Space X ↔ ∀ {x y : X}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ ∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y

Tactic:
simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne, not_imp_comm, Pairwise]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem monotone_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    ∀ᵐ a ∂ρ.fst, Monotone fun r ↦ preCDF ρ r a

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst

Tactic:
rw [setLIntegral_preCDF_fst ρ r hs, setLIntegral_preCDF_fst ρ r' hs]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ (ρ.IicSnd ↑r) s ≤ (ρ.IicSnd ↑r') s

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Monotone fun r => preCDF ρ r a

Tactic:
simp_rw [Monotone, ae_all_iff]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ (i i_1 : ℚ), i ≤ i_1 → ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ (i i_1 : ℚ), i ≤ i_1 → ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a

Tactic:
refine fun r r' hrr' ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF
  fun s hs _ ↦ ?_

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
x✝ : ρ.fst s < ⊤
⊢ (ρ.IicSnd ↑r) s ≤ (ρ.IicSnd ↑r') s

Tactic:
exact Measure.IicSnd_mono ρ (mod_cast hrr') s

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_mul_eq_left {f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) :
    (mulSupport f).mulIndicator (f * g) = f

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
⊢ (f * g) x = f x

Tactic:
have : g x = 1 := nmem_mulSupport.1 (disjoint_left.1 h hx)

Result:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ (f * g) x = f x

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport f).mulIndicator (f * g) = f

Tactic:
refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport

Result:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
⊢ (f * g) x = f x

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
⊢ (f * g) x = f x

Tactic:
rw [Pi.mul_apply, this, mul_one]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Pi.lean
@[simp]
lemma piRightHom_mul (x y : A ⊗[R] ∀ i, B i) :
    piRightHom R S A B (x * y) = piRightHom R S A B x * piRightHom R S A B y

Proof state:
case tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * y) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) y

Tactic:
induction y

Result:
case tmul.zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * 0) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) 0

case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)

case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → CommSemiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) x✝
a✝ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * y✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) y✝
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * (x✝ + y✝)) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ + y✝)
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ioc_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
    (∏ k ∈ Ioc a (b + 1), f k) = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Proof state:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a ≤ b
f : ℕ → M
⊢ ∏ k ∈ Ioc a (b + 1), f k = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Tactic:
rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive] lemma CovBySMul.nonneg : CovBySMul M K A B → 0 ≤ K

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B : Set X
⊢ CovBySMul M K A B → 0 ≤ K

Tactic:
rintro ⟨F, hF, -⟩

Result:
case intro.intro
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B : Set X
F : Finset M
hF : ↑(#F) ≤ K
⊢ 0 ≤ K

Proof state:
case intro.intro
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B : Set X
F : Finset M
hF : ↑(#F) ≤ K
⊢ 0 ≤ K

Tactic:
exact (#F).cast_nonneg.trans hF

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndependent_iff'ₛ :
    LinearIndependent R v ↔
      ∀ s : Finset ι, ∀ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i :=
  linearIndependent_iffₛ.trans
    ⟨fun hv s f g eq i his ↦ by
      have h :=
        hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
          simpa only [map_sum, Finsupp.linearCombination_single] using eq
      have (f : ι → R) : f i = (∑ j ∈ s, Finsupp.single j (f j)) i :=
        calc
          f i = (Finsupp.lapply i : (ι →₀ R) →ₗ[R] R) (Finsupp.single i (f i))

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.lapply i) (Finsupp.single j (f j)) = 0

Tactic:
rw [Finsupp.lapply_apply, Finsupp.single_eq_of_ne hji]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
⊢ f i = g i

Tactic:
have h :=
  hv (∑ i ∈ s, Finsupp.single i (f i)) (∑ i ∈ s, Finsupp.single i (g i)) <| by
    simpa only [map_sum, Finsupp.linearCombination_single] using eq

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f i) = ∑ i ∈ s, Finsupp.single i (g i)
⊢ f i = g i
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem mem_nonZeroDivisors_of_leadingCoeff {p : R[X]} (h : p.leadingCoeff ∈ R⁰) : p ∈ R[X]⁰

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
⊢ p ∈ R[X]⁰

Tactic:
refine mem_nonZeroDivisors_iff.2 fun x hx ↦ leadingCoeff_eq_zero.1 ?_

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
x : R[X]
hx : x * p = 0
⊢ x.leadingCoeff = 0

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
x : R[X]
hx : x * p = 0
hx' : ¬x.leadingCoeff * p.leadingCoeff = 0
⊢ False

Tactic:
simp only [← leadingCoeff_mul' hx', hx, leadingCoeff_zero, not_true] at hx'

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
x : R[X]
hx : x * p = 0
⊢ x.leadingCoeff = 0

Tactic:
by_contra hx'

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
x : R[X]
hx : x * p = 0
hx' : ¬x.leadingCoeff = 0
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
x : R[X]
hx : x * p = 0
hx' : ¬x.leadingCoeff = 0
⊢ False

Tactic:
rw [← mul_right_mem_nonZeroDivisors_eq_zero_iff h] at hx'

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
h : p.leadingCoeff ∈ R⁰
x : R[X]
hx : x * p = 0
hx' : ¬x.leadingCoeff * p.leadingCoeff = 0
⊢ False
-- Mathlib/Analysis/Analytic/Composition.lean
theorem removeZero_applyComposition (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (c : Composition n) : p.removeZero.applyComposition c = p.applyComposition c

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
v : Fin n → E
i : Fin c.length
⊢ p.removeZero.applyComposition c v i = p.applyComposition c v i

Tactic:
simp [applyComposition, zero_lt_one.trans_le (c.one_le_blocksFun i), removeZero_of_pos]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
⊢ p.removeZero.applyComposition c = p.applyComposition c

Tactic:
ext v i

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
v : Fin n → E
i : Fin c.length
⊢ p.removeZero.applyComposition c v i = p.applyComposition c v i
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Iic (y : ℝ) : Real.toEReal ⁻¹' Iic y = Iic y

Proof state:
y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iic ↑↑y = Iic y

Tactic:
refine preimage_comp.trans ?_

Result:
y : ℝ
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Iic ↑↑y) = Iic y

Proof state:
y : ℝ
⊢ Real.toEReal ⁻¹' Iic ↑y = Iic y

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Iic (WithBot.some (WithTop.some y))) = _

Result:
y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iic ↑↑y = Iic y

Proof state:
y : ℝ
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Iic ↑↑y) = Iic y

Tactic:
simp only [WithBot.preimage_coe_Iic, WithTop.preimage_coe_Iic]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_odd_mul_cos_pow (m n : ℕ) :
    (∫ x in a..b, sin x ^ (2 * m + 1) * cos x ^ n) = ∫ u in cos b..cos a, u^n * (↑1 - u ^ 2) ^ m :=
  have hc : Continuous fun u : ℝ => u ^ n * (↑1 - u ^ 2) ^ m

Proof state:
case h.e'_4.h.h.e'_5.h.e'_5.h.e'_5
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝

Tactic:
rw [← sq, ← sq, sin_sq]

Result:
no goals

Proof state:
a b : ℝ
m n : ℕ
⊢ Continuous fun u => u ^ n * (1 - u ^ 2) ^ m

Tactic:
fun_prop

Result:
no goals

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in a..b, sin x ^ (2 * m + 1) * cos x ^ n = -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n

Tactic:
rw [integral_symm]

Result:
no goals

Proof state:
case e_f
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (fun x => (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n) = fun x => cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x

Tactic:
ext

Result:
case e_f.h
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ (1 - cos x✝ ^ 2) ^ m * -sin x✝ * cos x✝ ^ n = cos x✝ ^ n * (1 - cos x✝ ^ 2) ^ m * -sin x✝

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x

Tactic:
congr

Result:
case e_f
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ (fun x => (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n) = fun x => cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n

Tactic:
congr! 5

Result:
case h.e'_4.h.h.e'_5.h.e'_5.h.e'_5
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ sin x✝ * sin x✝ = 1 - cos x✝ * cos x✝

Proof state:
case e_f.h
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
x✝ : ℝ
⊢ (1 - cos x✝ ^ 2) ^ m * -sin x✝ * cos x✝ ^ n = cos x✝ ^ n * (1 - cos x✝ ^ 2) ^ m * -sin x✝

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n = ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n

Tactic:
simp only [_root_.pow_succ, pow_mul, _root_.pow_zero, one_mul, mul_neg, neg_mul,
  integral_neg, neg_inj]

Result:
a b : ℝ
m n : ℕ
hc : Continuous fun u => u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in b..a, (sin x * sin x) ^ m * sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, (1 - cos x * cos x) ^ m * sin x * cos x ^ n
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integral_gaussian (b : ℝ) : ∫ x : ℝ, exp (-b * x ^ 2) = √(π / b)

Proof state:
b : ℝ
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

Tactic:
rcases le_or_lt b 0 with (hb | hb)

Result:
case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

Proof state:
case inl
b : ℝ
hb : b ≤ 0
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

Tactic:
rw [integral_undef, sqrt_eq_zero_of_nonpos]

Result:
case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x => rexp (-b * x ^ 2)) volume

Proof state:
case inl
b : ℝ
hb : b ≤ 0
⊢ ¬Integrable (fun x => rexp (-b * x ^ 2)) volume

Tactic:
simpa only [not_lt, integrable_exp_neg_mul_sq_iff] using hb

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
⊢ 0 < (↑b).re

Tactic:
rwa [ofReal_re]

Result:
no goals

Proof state:
case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = √(π / b) ^ 2

Tactic:
rw [← ofReal_inj, ofReal_pow, ← coe_algebraMap, RCLike.algebraMap_eq_ofReal, ← integral_ofReal,
  sq_sqrt (div_pos pi_pos hb).le, ← RCLike.algebraMap_eq_ofReal, coe_algebraMap, ofReal_div]

Result:
case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), ↑(rexp (-b * x ^ 2))) ^ 2 = ↑π / ↑b

Proof state:
case inr
b : ℝ
hb : 0 < b
⊢ ∫ (x : ℝ), rexp (-b * x ^ 2) = √(π / b)

Tactic:
refine (sq_eq_sq₀ (by positivity) (by positivity)).1 ?_

Result:
case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), rexp (-b * x ^ 2)) ^ 2 = √(π / b) ^ 2

Proof state:
case inl
b : ℝ
hb : b ≤ 0
⊢ π / b ≤ 0

Tactic:
exact div_nonpos_of_nonneg_of_nonpos pi_pos.le hb

Result:
no goals

Proof state:
case inr
b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ), ↑(rexp (-b * x ^ 2))) ^ 2 = ↑π / ↑b

Tactic:
convert integral_gaussian_sq_complex (by rwa [ofReal_re] : 0 < (b : ℂ).re) with _ x

Result:
case h.e'_2.h.e'_5.h.e'_7.h
b : ℝ
hb : 0 < b
x : ℝ
⊢ ↑(rexp (-b * x ^ 2)) = cexp (-↑b * ↑x ^ 2)

Proof state:
case h.e'_2.h.e'_5.h.e'_7.h
b : ℝ
hb : 0 < b
x : ℝ
⊢ ↑(rexp (-b * x ^ 2)) = cexp (-↑b * ↑x ^ 2)

Tactic:
rw [ofReal_exp, ofReal_mul, ofReal_pow, ofReal_neg]

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
⊢ 0 ≤ √(π / b)

Tactic:
positivity

Result:
no goals

Proof state:
b : ℝ
hb : 0 < b
⊢ 0 ≤ ∫ (x : ℝ), rexp (-b * x ^ 2)

Tactic:
positivity

Result:
no goals