-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem pairwise_aedisjoint_of_aedisjoint_forall_ne_one {G α : Type*} [Group G] [MulAction G α]
    {_ : MeasurableSpace α} {μ : Measure α} {s : Set α}
    (h_ae_disjoint : ∀ g ≠ (1 : G), AEDisjoint μ (g • s) s)
    (h_qmp : ∀ g : G, QuasiMeasurePreserving (g • ·) μ μ) :
    Pairwise (AEDisjoint μ on fun g : G => g • s)

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ g ≠ 1

Tactic:
rw [Ne, inv_mul_eq_one]

Result:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g₂ = g₁

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun x => g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
⊢ (AEDisjoint μ on fun g => g • s) g₁ g₂

Tactic:
change μ (g₁ • s ∩ g₂ • s) = 0

Result:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun x => g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
⊢ μ (g₁ • s ∩ g₂ • s) = 0

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (fun x => g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s

Tactic:
rw [preimage_eq_iff_eq_image (MulAction.bijective g₂⁻¹), image_smul, smul_set_inter, smul_smul,
  smul_smul, inv_mul_cancel, one_smul]

Result:
no goals

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ ¬g₂ = g₁

Tactic:
exact hg.symm

Result:
no goals

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ (AEDisjoint μ on fun g => g • s) g₁ g₂

Tactic:
replace hg : g ≠ 1 := by
  rw [Ne, inv_mul_eq_one]
  exact hg.symm

Result:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ (AEDisjoint μ on fun g => g • s) g₁ g₂

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
⊢ Pairwise (AEDisjoint μ on fun g => g • s)

Tactic:
intro g₁ g₂ hg

Result:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
⊢ (AEDisjoint μ on fun g => g • s) g₁ g₂

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
⊢ (AEDisjoint μ on fun g => g • s) g₁ g₂

Tactic:
let g := g₂⁻¹ * g₁

Result:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
hg : g₁ ≠ g₂
g : G := g₂⁻¹ * g₁
⊢ (AEDisjoint μ on fun g => g • s) g₁ g₂

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x => g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
this : (fun x => g₂⁻¹ • x) ⁻¹' (g • s ∩ s) = g₁ • s ∩ g₂ • s
⊢ μ (g₁ • s ∩ g₂ • s) = 0

Tactic:
exact this ▸ (h_qmp g₂⁻¹).preimage_null (h_ae_disjoint g hg)

Result:
no goals