`BookProof.ChapterG.gaugeGroup_fiber_transitive` {X Y : Type*} (π : X → Y) (x₁ x₂ : X) (h : π x₁ = π x₂) : ∃ g ∈ gaugeGroup π, g x₁ = x₂
ProvedBookProof.ChapterG.gaugeGroup_fiber_transitivetheoremstimepiece
Prove the following Lean 4 theorem from ChapterG.
BookProof.ChapterG.gaugeGroup_fiber_transitive {X Y : Type*} (π : X → Y) (x₁ x₂ : X) (h : π x₁ = π x₂) : ∃ g ∈ gaugeGroup π, g x₁ = x₂
Formalization note: Lean 4 identifier BookProof.ChapterG.gaugeGroup_fiber_transitive.
Preamble
-- Generated from ChapterG.lean — theorem BookProof.ChapterG.gaugeGroup_fiber_transitive
import Mathlib
import Definitions.Def_ChapterG
open BookProof.ChapterG
open scoped ComplexConjugate InnerProductSpace Matrix
open MeasureTheory
variable {G : Type*} [Group G] [MeasurableSpace G]
variable {μG : Measure G} [IsProbabilityMeasure μG] [μG.IsMulLeftInvariant]
variable {X : Type*} [MulAction G X]
variable {A : Type*} [Ring A]
variable {α β E : Type*} [MeasurableSpace α] [MeasurableSpace β]
[NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {ν : Measure β}
{p : ENNReal} [Fact (1 ≤ p)]Formal statement
theorem BookProof.ChapterG.gaugeGroup_fiber_transitive {X Y : Type*} (π : X → Y)
(x₁ x₂ : X) (h : π x₁ = π x₂) : ∃ g ∈ gaugeGroup π, g x₁ = x₂ := by sorry