awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b_1 : B
a : A
ha :
  Membership.mem (γ := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b_1 ((φ : (a : A) → B) a : B))) a
b : A
hb :
  Membership.mem (γ := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b_1 ((φ : (a : A) → B) a : B))) b
⊢ Eq.{u_3 + 1} (α := C) ((ψ : (a : B) → C) (HMul.hMul (β := B) b_1 ((φ : (a : A) → B) a : B)) : C)
    ((ψ : (a : B) → C) (HMul.hMul (β := B) b_1 ((φ : (a : A) → B) b : B)) : C)

Tactic:
simp [H.mulExact.apply_apply_eq_one]

Premises used: TopologicalGroup.IsSES.mulExact, Function.MulExact.apply_apply_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b_1 : B
a : A
ha :
  Membership.mem (γ := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b_1 ((φ : (a : A) → B) a : B))) a
b : A
hb :
  Membership.mem (γ := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b_1 ((φ : (a : A) → B) a : B))) b
⊢ a = b

Tactic:
simpa [H.isClosedEmbedding.injective.eq_iff] using hc (hf3 (subset_tsupport _ ha))
      (hf3 (subset_tsupport _ hb)) (by simp [H.mulExact.apply_apply_eq_one])

Premises used: subset_tsupport, Function.Injective.eq_iff, TopologicalGroup.IsSES.isClosedEmbedding, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
⊢ Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))

Tactic:
have key : (Function.support fun a ↦ f (b * φ a)).Subsingleton := by
    intro a ha b hb
    simpa [H.isClosedEmbedding.injective.eq_iff] using hc (hf3 (subset_tsupport _ ha))
      (hf3 (subset_tsupport _ hb)) (by simp [H.mulExact.apply_apply_eq_one])
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h_2 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
key :
  Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))
h :
  Eq.{u_1 + 1} (α := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))) ∅
⊢ ∫ (x : A) in
      Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)),
      (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) x : B)) ∂μA ≤
    ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
key :
  Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))
a : A
ha :
  Eq (α := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))) {a}
inr : LE.le (α := ℝ) ((f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)) : ℝ) (1 : ℝ)
inr₁ : 0 < ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})
⊢ ∫ (x : A) in
      Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)),
      (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) x : B)) ∂μA ≤
    ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})

Tactic:
rw [ha, integral_singleton, real_def, haar_singleton, smul_eq_mul, mul_le_iff_le_one_right]

Premises used: MeasureTheory.Measure.haar_singleton, MeasureTheory.Measure.real_def, MeasureTheory.integral_singleton, smul_eq_mul, mul_le_iff_le_one_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
key :
  Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))
a : A
ha :
  Eq (α := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))) {a}
⊢ LE.le (α := ℝ) ((f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)) : ℝ) (1 : ℝ)

Tactic:
(hf4 _).2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
key :
  Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))
a : A
ha :
  Eq (α := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))) {a}
⊢ LE.le (α := ℝ) ((f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)) : ℝ) (1 : ℝ)

Tactic:
exact (hf4 _).2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
key :
  Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))
a : A
ha :
  Eq (α := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))) {a}
⊢ 0 < ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})

Tactic:
ENNReal.toReal_pos ho.ne' ht.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Extension
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Group A
inst_1 : Group B
inst_2 : Group C
inst_3 : TopologicalSpace A
inst_4 : TopologicalSpace B
inst_5 : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst_6 : IsTopologicalGroup A
inst_7 : IsTopologicalGroup B
inst_8 : MeasurableSpace A
inst_9 : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst_10 : IsTopologicalGroup C
inst_11 : LocallyCompactSpace B
inst_12 : MeasurableSpace C
inst_13 : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst_14 : T2Space B
inst_15 : MeasurableSpace B
inst_16 : BorelSpace B
U : Set B
hU : IsOpen U
inst_17 : DiscreteTopology A
h_1 :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ((H.inducedMeasure μA μC : Measure B) : (a : Set B) → ENNReal) U
ho : LT.lt (α := ENNReal) (0 : ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal)
ht : LT.lt (α := ENNReal) ((μA : (a : Set A) → ENNReal) {1} : ENNReal) (⊤ : ENNReal)
K : Set B
hKU : K ⊆ U
hK : IsCompact K
f : C(B, ℝ)
hf1 : Set.EqOn (β := ℝ) (⇑f : (a : B) → ℝ) 1 K
hf2 : IsCompact (X := B) (tsupport (α := ℝ) (⇑f : (a : B) → ℝ))
hf3 : tsupport (α := ℝ) (⇑f : (a : B) → ℝ) ⊆ U
hf4 : ∀ (x : B), Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1) ((f : (a : B) → ℝ) x : ℝ)
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) ((μC : (a : Set C) → ENNReal) Set.univ : ENNReal)
      ((μA : (a : Set A) → ENNReal) {1} : ENNReal) <
    ENNReal.ofReal
      (∫ (c : C),
        ((((H.pushforward μA :
                    LinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) (CompactlySupportedContinuousMap B ℝ)
                      (CompactlySupportedContinuousMap C ℝ)) :
                  (a : CompactlySupportedContinuousMap B ℝ) → CompactlySupportedContinuousMap C ℝ)
                { toContinuousMap := f, hasCompactSupport' := hf2 } :
              CompactlySupportedContinuousMap C ℝ) :
            (a : C) → ℝ)
          c ∂μC)
hc : Set.InjOn.{u_2, u_3} (β := C) (⇑ψ : (a : B) → C) U
b : B
key :
  Set.Subsingleton.{u_1} (α := A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B)))
a : A
ha :
  Eq (α := Set A)
    (Function.support (M := ℝ) fun (a : A) ↦ (f : (a : B) → ℝ) (HMul.hMul (β := B) b ((φ : (a : A) → B) a : B))) {a}
⊢ 0 < ENNReal.toReal ((μA : (a : Set A) → ENNReal) {1})

Tactic:
exact ENNReal.toReal_pos ho.ne' ht.ne

Premises used: ENNReal.toReal_pos, LT.lt.ne', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
⊢ Eq (α := (a : E) → F) (⇑f.toMeasurableEquiv : (a : E) → F) (⇑f : (a : E) → F)

Tactic:
rfl

Premises used: rfl