internlm/Lean-Github huggingface dataset:
Theorem: MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
Proof state before:
σ : Type u_1
τ : Type ?u.9961
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.9970
n : ℕ
⊢ homogeneousSubmodule σ R n = Finsupp.supported R R {d | degree d = n}
Tactic:
convert weightedHomogeneousSubmodule_eq_finsupp_supported R 1 n
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_eq_zero_iff
Proof state before:
σ : Type u_2
τ : Type ?u.26920
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.26929
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
Tactic:
rw [totalDegree_eq_weightedTotalDegree, weightedTotalDegree_eq_zero_iff _ p]
Proof state after:
σ : Type u_2
τ : Type ?u.26920
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.26929
p : MvPolynomial σ R
⊢ NonTorsionWeight 1
Theorem: MvPolynomial.totalDegree_eq_zero_iff
Proof state before:
σ : Type u_2
τ : Type ?u.26920
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.26929
p : MvPolynomial σ R
⊢ NonTorsionWeight 1
Tactic:
exact unit_weight_is_nonTrivialWeight
Proof state after:
no goals
Theorem: MvPolynomial.isHomogeneous_of_totalDegree_zero_iff
Proof state before:
σ : Type u_2
τ : Type ?u.27316
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.27325
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p.IsHomogeneous 0
Tactic:
rw [totalDegree_eq_weightedTotalDegree,
  ← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsHomogeneous]
Proof state after:
no goals
Theorem: MvPolynomial.IsHomogeneous.totalDegree_eq_weightedTotalDegree
Proof state before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ φ.totalDegree = weightedTotalDegree 1 φ
Tactic:
rw [totalDegree, weightedTotalDegree, weightedDegree]
Proof state after:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ (φ.support.sup fun s => s.sum fun x e => e) = φ.support.sup fun s => (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom s
Theorem: MvPolynomial.IsHomogeneous.totalDegree_eq_weightedTotalDegree
Proof state before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ (φ.support.sup fun s => s.sum fun x e => e) = φ.support.sup fun s => (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom s
Tactic:
apply Finset.sup_congr rfl
Proof state after:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ ∀ a ∈ φ.support, (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a
Theorem: MvPolynomial.IsHomogeneous.totalDegree_eq_weightedTotalDegree
Proof state before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
⊢ ∀ a ∈ φ.support, (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a
Tactic:
intro a _
Proof state after:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
a : σ →₀ ℕ
a✝ : a ∈ φ.support
⊢ (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a
Theorem: MvPolynomial.IsHomogeneous.totalDegree_eq_weightedTotalDegree
Proof state before:
σ : Type u_1
τ : Type ?u.33916
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.33925
φ ψ : MvPolynomial σ R
m n : ℕ
a : σ →₀ ℕ
a✝ : a ∈ φ.support
⊢ (a.sum fun x e => e) = (Finsupp.total σ ℕ ℕ 1).toAddMonoidHom a
Tactic:
simp only [Finsupp.total, Pi.one_apply, LinearMap.toAddMonoidHom_coe, Finsupp.coe_lsum,
  LinearMap.coe_smulRight, LinearMap.id_coe, id_eq, Algebra.id.smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: MvPolynomial.IsHomogeneous.totalDegree
Proof state before:
σ : Type u_1
τ : Type ?u.36379
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.36388
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous n
h : φ ≠ 0
⊢ φ.totalDegree = n
Tactic:
rw [totalDegree_eq_weightedTotalDegree, ← WithBot.coe_eq_coe, ←
  weightedTotalDegree_coe _ φ h, IsWeightedHomogeneous.weighted_total_degree hφ h]
Proof state after:
no goals
Theorem: MvPolynomial.homogeneousComponent_eq_zero
Proof state before:
σ : Type u_1
τ : Type ?u.51956
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.51965
n : ℕ
φ ψ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ (homogeneousComponent n) φ = 0
Tactic:
rw [totalDegree_eq_weightedTotalDegree] at h
Proof state after:
σ : Type u_1
τ : Type ?u.51956
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.51965
n : ℕ
φ ψ : MvPolynomial σ R
h : weightedTotalDegree 1 φ < n
⊢ (homogeneousComponent n) φ = 0
Theorem: MvPolynomial.homogeneousComponent_eq_zero
Proof state before:
σ : Type u_1
τ : Type ?u.51956
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.51965
n : ℕ
φ ψ : MvPolynomial σ R
h : weightedTotalDegree 1 φ < n
⊢ (homogeneousComponent n) φ = 0
Tactic:
exact weightedHomogeneousComponent_eq_zero n φ h
Proof state after:
no goals
Theorem: MvPolynomial.sum_homogeneousComponent
Proof state before:
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ = φ
Tactic:
ext1 d
Proof state after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
Theorem: MvPolynomial.sum_homogeneousComponent
Proof state before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
Tactic:
suffices φ.totalDegree < degree d → 0 = coeff d φ by
  simpa [coeff_sum, coeff_homogeneousComponent]
Proof state after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < degree d → 0 = coeff d φ
Theorem: MvPolynomial.sum_homogeneousComponent
Proof state before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < degree d → 0 = coeff d φ
Tactic:
rw [degree_eq_weightedDegree]
Proof state after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < ∑ i ∈ d.support, d i → 0 = coeff d φ
Theorem: MvPolynomial.sum_homogeneousComponent
Proof state before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < ∑ i ∈ d.support, d i → 0 = coeff d φ
Tactic:
intro h
Proof state after:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
h : φ.totalDegree < ∑ i ∈ d.support, d i
⊢ 0 = coeff d φ
Theorem: MvPolynomial.sum_homogeneousComponent
Proof state before:
case a
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
h : φ.totalDegree < ∑ i ∈ d.support, d i
⊢ 0 = coeff d φ
Tactic:
exact (coeff_eq_zero_of_totalDegree_lt h).symm
Proof state after:
no goals
Theorem: MvPolynomial.sum_homogeneousComponent
Proof state before:
σ : Type u_1
τ : Type ?u.53191
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.53200
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
this : φ.totalDegree < degree d → 0 = coeff d φ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
Tactic:
simpa [coeff_sum, coeff_homogeneousComponent]
Proof state after:
no goals
Theorem: MvPolynomial.decomposition.decompose'_eq
Proof state before:
σ : Type u_1
τ : Type ?u.73574
R : Type u_2
inst✝² : CommSemiring R
S : Type ?u.73583
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq R
⊢ DirectSum.Decomposition.decompose' = fun φ =>
    (DirectSum.mk (fun i => ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑degree) φ.support)) fun m =>
      ⟨(homogeneousComponent ↑m) φ, ⋯⟩
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.mem_toSubset'
Proof state before:
X : Type u_1
s t : Set X
h : s ≤ t
x : ↑t
⊢ x ∈ s.toSubset' t h ↔ ↑x ∈ s
Tactic:
rw [toSubset', Set.range_inclusion, Set.mem_setOf_eq]
Proof state after:
no goals
Theorem: Set.coe_toSubset
Proof state before:
X : Type u_1
s t : Set X
⊢ Subtype.val '' s.toSubset t = s ∩ t
Tactic:
ext
Proof state after:
case h
X : Type u_1
s t : Set X
x✝ : X
⊢ x✝ ∈ Subtype.val '' s.toSubset t ↔ x✝ ∈ s ∩ t
Theorem: Set.coe_toSubset
Proof state before:
case h
X : Type u_1
s t : Set X
x✝ : X
⊢ x✝ ∈ Subtype.val '' s.toSubset t ↔ x✝ ∈ s ∩ t
Tactic:
sorry
Proof state after:
no goals
Theorem: toSubset_iUnion
Proof state before:
X : Type u_1
t : Set X
S : ℕ → Set X
⊢ (⋃ n, S n).toSubset t = ⋃ n, (S n).toSubset t
Tactic:
ext
Proof state after:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ x✝ ∈ (⋃ n, S n).toSubset t ↔ x✝ ∈ ⋃ n, (S n).toSubset t
Theorem: toSubset_iUnion
Proof state before:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ x✝ ∈ (⋃ n, S n).toSubset t ↔ x✝ ∈ ⋃ n, (S n).toSubset t
Tactic:
rw [mem_toSubset]
Proof state after:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ ↑x✝ ∈ ⋃ n, S n ↔ x✝ ∈ ⋃ n, (S n).toSubset t
Theorem: toSubset_iUnion
Proof state before:
case h
X : Type u_1
t : Set X
S : ℕ → Set X
x✝ : ↑t
⊢ ↑x✝ ∈ ⋃ n, S n ↔ x✝ ∈ ⋃ n, (S n).toSubset t
Tactic:
sorry
Proof state after:
no goals
Theorem: toSubset_compact
Proof state before:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hsw : s ⊆ t
hs : IsCompact s
⊢ IsCompact (s.toSubset t)
Tactic:
sorry
Proof state after:
no goals
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ ↑ν (f '' s) = 0
Tactic:
have h₁ : μ = μH[m] := by
  have aux : μH[m] = volume := by
    rw [← Fintype.card_fin m]
    exact hausdorffMeasure_pi_real (ι := Fin m)
  sorry
Proof state after:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
⊢ ↑ν (f '' s) = 0
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
⊢ ↑ν (f '' s) = 0
Tactic:
have h₂ : ν = μH[n] := by sorry
Proof state after:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0
Tactic:
rw [h₁] at h₂s
Proof state after:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
⊢ ↑ν (f '' s) = 0
Tactic:
have : μH[m] (f '' s) = 0 := by
  have scifi : Convex ℝ U := sorry
  apply locally_lipschitz_image_of_null_set_is_null_set_open (of_C1_on_open hU scifi hf) h₁s h₂s
Proof state after:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑ν (f '' s) = 0
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑ν (f '' s) = 0
Tactic:
rw [h₂, ← hd]
Proof state after:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑μH[↑m] (f '' s) = 0
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μH[↑m] s = 0
h₁ : μ = μH[↑m]
h₂ : ν = μH[↑n]
this : ↑μH[↑m] (f '' s) = 0
⊢ ↑μH[↑m] (f '' s) = 0
Tactic:
exact this
Proof state after:
no goals
Theorem: image_null_of_C1_of_null
Proof state before:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
⊢ μ = μH[↑m]
Tactic:
have aux : μH[m] = volume := by
  rw [← Fintype.card_fin m]
  exact hausdorffMeasure_pi_real (ι := Fin m)
Proof state after:
E : Type u_1
inst✝²² : NormedAddCommGroup E
inst✝²¹ : NormedSpace ℝ E
H : Type u_2
inst✝²⁰ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : ChartedSpace H M
inst✝¹⁷ : I.Boundaryless
inst✝¹⁶ : SmoothManifoldWithCorners I M
inst✝¹⁵ : FiniteDimensional ℝ E
inst✝¹⁴ : SecondCountableTopology M
inst✝¹³ : MeasurableSpace E
inst✝¹² : BorelSpace E
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
G : Type u_5
inst✝⁹ : TopologicalSpace G
J : ModelWithCorners ℝ F G
N : Type u_6
inst✝⁸ : TopologicalSpace N
inst✝⁷ : ChartedSpace G N
inst✝⁶ : J.Boundaryless
inst✝⁵ : SmoothManifoldWithCorners J N
inst✝⁴ : FiniteDimensional ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
m n r : ℕ
hm : finrank ℝ E = m
hn : finrank ℝ F = n
hr : r > m - n
f : E → F
U : Set E
hU : IsOpen U
hf : ContDiffOn ℝ 1 f U
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
ν : Measure F
inst✝ : ν.IsAddHaarMeasure
hd : m = n
s : Set E
h₁s : s ⊆ U
h₂s : ↑μ s = 0
aux : μH[↑m] = volume
⊢ μ = μH[↑m]