harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.vecMulLinear_transpose [Fintype n] (M : Matrix m n R) :
    Mᵀ.vecMulLinear = M.mulVecLin

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ Mᵀ.vecMulLinear = M.mulVecLin

Tactic:
ext

Result:
case h.h
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
x✝¹ : n → R
x✝ : m
⊢ Mᵀ.vecMulLinear x✝¹ x✝ = M.mulVecLin x✝¹ x✝

Proof state:
case h.h
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
x✝¹ : n → R
x✝ : m
⊢ Mᵀ.vecMulLinear x✝¹ x✝ = M.mulVecLin x✝¹ x✝

Tactic:
simp [vecMul_transpose]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_one : logb b 1 = 0

Proof state:
b : ℝ
⊢ logb b 1 = 0

Tactic:
simp [logb]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsionBySet_iff_is_torsion_by_span :
    IsTorsionBySet R M s ↔ IsTorsionBySet R M (Ideal.span s)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ IsTorsionBySet R M s ↔ IsTorsionBySet R M ↑(Ideal.span s)

Tactic:
simpa only [isTorsionBySet_iff_subset_annihilator] using Ideal.span_le.symm

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
lemma finrank_ker_add_one_of_ne_zero :
    finrank K (LinearMap.ker f) + 1 = finrank K V₁

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
⊢ finrank K ↥(LinearMap.range f) = 1

Tactic:
rw [range_eq_top_of_ne_zero hf, finrank_top, finrank_self]

Result:
no goals

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
⊢ finrank K ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
suffices finrank K (LinearMap.range f) = 1 by
  rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
  f.quotKerEquivRange.finrank_eq, this]

Result:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
⊢ finrank K ↥(LinearMap.range f) = 1

Proof state:
K : Type uK
inst✝³ : Field K
V₁ : Type uV₁
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
this : finrank K ↥(LinearMap.range f) = 1
⊢ finrank K ↥(LinearMap.ker f) + 1 = finrank K V₁

Tactic:
rw [← (LinearMap.ker f).finrank_quotient_add_finrank, add_comm, add_left_inj,
f.quotKerEquivRange.finrank_eq, this]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volume_preserving_negAt [NumberField K] :
    MeasurePreserving (negAt s)

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (↑(neg ℝ).toLinearEquiv).toAddHom.1 volume volume

Tactic:
exact Measure.measurePreserving_neg _

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
⊢ MeasurePreserving (⇑(negAt s)) volume volume

Tactic:
refine MeasurePreserving.prod (volume_preserving_pi fun w ↦ ?_) (MeasurePreserving.id _)

Result:
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
⊢ MeasurePreserving (↑((fun w => if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) w).toLinearEquiv).toAddHom.1
    volume volume

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (↑((fun w => if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) w).toLinearEquiv).toAddHom.1
    volume volume

Tactic:
simp_rw [if_pos hw]

Result:
case pos
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (↑(neg ℝ).toLinearEquiv).toAddHom.1 volume volume

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (↑((fun w => if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) w).toLinearEquiv).toAddHom.1
    volume volume

Tactic:
simp_rw [if_neg hw]

Result:
case neg
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (↑(ContinuousLinearEquiv.refl ℝ ℝ).toLinearEquiv).toAddHom.1 volume volume

Proof state:
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
⊢ MeasurePreserving (↑((fun w => if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) w).toLinearEquiv).toAddHom.1
    volume volume

Tactic:
by_cases hw : w ∈ s

Result:
case pos
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∈ s
⊢ MeasurePreserving (↑((fun w => if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) w).toLinearEquiv).toAddHom.1
    volume volume

case neg
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (↑((fun w => if w ∈ s then neg ℝ else ContinuousLinearEquiv.refl ℝ ℝ) w).toLinearEquiv).toAddHom.1
    volume volume

Proof state:
case neg
K : Type u_1
inst✝¹ : Field K
s : Set { w // w.IsReal }
inst✝ : NumberField K
w : { w // w.IsReal }
hw : w ∉ s
⊢ MeasurePreserving (↑(ContinuousLinearEquiv.refl ℝ ℝ).toLinearEquiv).toAddHom.1 volume volume

Tactic:
exact MeasurePreserving.id _

Result:
no goals
-- Mathlib/CategoryTheory/Extensive.lean
theorem FinitaryPreExtensive.isUniversal_finiteCoproducts [FinitaryPreExtensive C] {ι : Type*}
    [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsUniversalColimit c

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsUniversalColimit c

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsUniversalColimit c

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsUniversalColimit c

Tactic:
apply (IsUniversalColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Proof state:
case intro.intro.hc
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc

Result:
no goals

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsUniversalColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)

Tactic:
apply FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin

Result:
case intro.intro.hc
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
F : Discrete ι ⥤ C
c : Cocone F
hc : IsColimit c
n : ℕ
e : ι ≃ Fin n
⊢ IsColimit (Cocone.whisker (Discrete.equivalence e).symm.functor c)
-- Mathlib/Data/Complex/FiniteDimensional.lean
/-- `C` has an uncountable basis over `ℚ`. -/
@[simp, stacks 09G0]
lemma Complex.rank_rat_complex : Module.rank ℚ ℂ = continuum

Proof state:
⊢ Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ

Tactic:
simpa using aleph0_lt_continuum

Result:
no goals

Proof state:
⊢ Module.rank ℚ ℂ = 𝔠

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans mk_complex

Result:
⊢ Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem Algebra.IsIntegral.tower_bot [Algebra R S] [Algebra R T] [Algebra S T]
    [NoZeroSMulDivisors S T] [Nontrivial T] [IsScalarTower R S T]
    [h : Algebra.IsIntegral R T] : Algebra.IsIntegral R S where
  isIntegral

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : NoZeroSMulDivisors S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ((algebraMap S T).comp (algebraMap R S)).IsIntegral

Tactic:
rw [← IsScalarTower.algebraMap_eq R S T]

Result:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : NoZeroSMulDivisors S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : NoZeroSMulDivisors S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ∀ (x : S), IsIntegral R x

Tactic:
apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T)
  (FaithfulSMul.algebraMap_injective S T)

Result:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : NoZeroSMulDivisors S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ ((algebraMap S T).comp (algebraMap R S)).IsIntegral

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : NoZeroSMulDivisors S T
inst✝¹ : Nontrivial T
inst✝ : IsScalarTower R S T
h : Algebra.IsIntegral R T
⊢ (algebraMap R T).IsIntegral

Tactic:
exact h.isIntegral

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem _root_.Filter.EventuallyEq.restrict {f g : α → δ} {s : Set α} (hfg : f =ᵐ[μ] g) :
    f =ᵐ[μ.restrict s] g

Proof state:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ μ.restrict s ≪ μ

Tactic:
exact Measure.absolutelyContinuous_of_le Measure.restrict_le_self

Result:
no goals

Proof state:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.restrict s)] g

Tactic:
refine hfg.filter_mono ?_

Result:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ ae (μ.restrict s) ≤ ae μ

Proof state:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ ae (μ.restrict s) ≤ ae μ

Tactic:
rw [Measure.ae_le_iff_absolutelyContinuous]

Result:
α : Type u_2
δ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ μ.restrict s ≪ μ
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Ico : (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ico b c = Ioc (a - c) (a - b)
-- Mathlib/MeasureTheory/Function/SpecialFunctions/RCLike.lean
theorem measurable_of_re_im (hre : Measurable fun x => RCLike.re (f x))
    (him : Measurable fun x => RCLike.im (f x)) : Measurable f

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
hre : Measurable fun x => RCLike.re (f x)
him : Measurable fun x => RCLike.im (f x)
⊢ Measurable f

Tactic:
convert Measurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp hre)
    ((RCLike.measurable_ofReal.comp him).mul_const RCLike.I)

Result:
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
hre : Measurable fun x => RCLike.re (f x)
him : Measurable fun x => RCLike.im (f x)
x✝ : α
⊢ f x✝ = (RCLike.ofReal ∘ fun x => RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x => RCLike.im (f x)) x✝ * RCLike.I

Proof state:
case h.e'_5.h
α : Type u_1
𝕜 : Type u_2
inst✝¹ : RCLike 𝕜
inst✝ : MeasurableSpace α
f : α → 𝕜
hre : Measurable fun x => RCLike.re (f x)
him : Measurable fun x => RCLike.im (f x)
x✝ : α
⊢ f x✝ = (RCLike.ofReal ∘ fun x => RCLike.re (f x)) x✝ + (RCLike.ofReal ∘ fun x => RCLike.im (f x)) x✝ * RCLike.I

Tactic:
exact (RCLike.re_add_im _).symm

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem nodup_flatten {L : List (List α)} :
    Nodup (flatten L) ↔ (∀ l ∈ L, Nodup l) ∧ Pairwise Disjoint L

Proof state:
α : Type u
L : List (List α)
⊢ L.flatten.Nodup ↔ (∀ l ∈ L, l.Nodup) ∧ Pairwise Disjoint L

Tactic:
simp only [Nodup, pairwise_flatten, disjoint_left.symm, forall_mem_ne]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem insert'_eq_insertWith [DecidableRel (α := α) (· ≤ ·)] (x : α) :
    ∀ t, insert' x t = insertWith id x t
  | nil => rfl
  | node _ l y r => by
    unfold insert' insertWith; cases cmpLE x y <;> simp [insert'_eq_insertWith]

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ insert' x (node size✝ l y r) = insertWith id x (node size✝ l y r)

Tactic:
unfold insert' insertWith

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (insert' x l).balanceL y r
    | Ordering.eq => node size✝ l y r
    | Ordering.gt => l.balanceR y (insert' x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith id x l).balanceL y r
    | Ordering.eq => node size✝ l (id y) r
    | Ordering.gt => l.balanceR y (insertWith id x r)

Tactic:
cases cmpLE x y <;> simp [insert'_eq_insertWith]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_embedding_eq_zero_iff_lift_lt : #(α ↪ β') = 0 ↔ lift.{u} #β' < lift.{v} #α

Proof state:
α : Type u
β' : Type v
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α

Tactic:
rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem lintegral_map' {β} [MeasurableSpace β] {μ' : Measure β} (f : α →ₛ ℝ≥0∞) (g : β →ₛ ℝ≥0∞)
    (m' : α → β) (eq : ∀ a, f a = g (m' a)) (h : ∀ s, MeasurableSet s → μ' s = μ (m' ⁻¹' s)) :
    f.lintegral μ = g.lintegral μ' :=
  lintegral_eq_of_measure_preimage fun y => by
    simp only [preimage, eq]
    exact (h (g ⁻¹' {y}) (g.measurableSet_preimage _)).symm

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), f a = g (m' a)
h : ∀ (s : Set β), MeasurableSet s → μ' s = μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ μ {x | g (m' x) ∈ {y}} = μ' {x | g x ∈ {y}}

Tactic:
exact (h (g ⁻¹' {y}) (g.measurableSet_preimage _)).symm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), f a = g (m' a)
h : ∀ (s : Set β), MeasurableSet s → μ' s = μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ μ (⇑f ⁻¹' {y}) = μ' (⇑g ⁻¹' {y})

Tactic:
simp only [preimage, eq]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MeasurableSpace β
μ' : Measure β
f : α →ₛ ℝ≥0∞
g : β →ₛ ℝ≥0∞
m' : α → β
eq : ∀ (a : α), f a = g (m' a)
h : ∀ (s : Set β), MeasurableSet s → μ' s = μ (m' ⁻¹' s)
y : ℝ≥0∞
⊢ μ {x | g (m' x) ∈ {y}} = μ' {x | g x ∈ {y}}
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem jordanDecomposition_add_withDensity_mutuallySingular {f : α → ℝ} (hf : Measurable f)
    (htμ : t ⟂ᵥ μ.toENNRealVectorMeasure) :
    (t.toJordanDecomposition.posPart + μ.withDensity fun x : α => ENNReal.ofReal (f x)) ⟂ₘ
      t.toJordanDecomposition.negPart + μ.withDensity fun x : α => ENNReal.ofReal (-f x)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)

Tactic:
exact
  ((JordanDecomposition.mutuallySingular _).add_right
        (htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
    ((htμ.2.symm.mono_ac (withDensity_absolutelyContinuous _ _) (refl _)).add_right
      (withDensity_ofReal_mutuallySingular hf))

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)

Tactic:
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
  VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem hasSum_prod_mFourierCoeff (f g : L²(UnitAddTorus d)) :
    HasSum (fun i ↦ conj (mFourierCoeff f i) * (mFourierCoeff g i)) (∫ t, conj (f t) * g t)

Proof state:
d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
n : d → ℤ
⊢ (starRingEnd ℂ) (mFourierCoeff (↑↑f) n) * mFourierCoeff (↑↑g) n =
    inner f (mFourierBasis n) * inner (mFourierBasis n) g

Tactic:
simp only [← mFourierBasis_repr, HilbertBasis.repr_apply_apply, inner_conj_symm]

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
⊢ HasSum (fun i => (starRingEnd ℂ) (mFourierCoeff (↑↑f) i) * mFourierCoeff (↑↑g) i)
    (∫ (t : UnitAddTorus d), (starRingEnd ℂ) (↑↑f t) * ↑↑g t)

Tactic:
refine HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)

Result:
d : Type u_1
inst✝ : Fintype d
f g : ↥(Lp ℂ 2 volume)
n : d → ℤ
⊢ (starRingEnd ℂ) (mFourierCoeff (↑↑f) n) * mFourierCoeff (↑↑g) n =
    inner f (mFourierBasis n) * inner (mFourierBasis n) g
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffineLift_add (P Q : W.Point) :
    (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩

Result:
case mk.mk.mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
point✝¹ : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
point✝ : PointClass F
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (mk hP + mk hQ).toAffineLift = (mk hP).toAffineLift + (mk hQ).toAffineLift

Proof state:
case mk.mk.mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
point✝¹ : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
point✝ : PointClass F
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (mk hP + mk hQ).toAffineLift = (mk hP).toAffineLift + (mk hQ).toAffineLift

Tactic:
exact toAffine_add hP hQ

Result:
no goals
-- Mathlib/Analysis/Oscillation.lean
theorem eq_zero_iff_continuousAt [TopologicalSpace E] (f : E → F) (x : E) :
    oscillation f x = 0 ↔ ContinuousAt f x

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
⊢ oscillation f x = 0 ↔ ContinuousAt f x

Tactic:
rw [← oscillationWithin_univ_eq_oscillation, ← continuousWithinAt_univ f x]

Result:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
⊢ oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
x : E
⊢ oscillationWithin f univ x = 0 ↔ ContinuousWithinAt f univ x

Tactic:
exact OscillationWithin.eq_zero_iff_continuousWithinAt f (mem_univ x)

Result:
no goals