-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem _root_.AddAction.IsBlock.of_addSubgroup_of_conjugate
    {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] {B : Set X}
    {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) :
    AddAction.IsBlock (H.map (AddAut.conj g).toMul.toAddMonoidHom) (g +ᵥ B)

Proof state:
case g
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ Disjoint (⟨h, hH⟩ +ᵥ B) B → Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)

Tactic:
exact Set.disjoint_image_of_injective (AddAction.injective g)

Result:
no goals

Proof state:
case f
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ ⟨h, hH⟩ +ᵥ B = B → g +ᵥ h +ᵥ B = g +ᵥ B

Tactic:
intro hB'

Result:
case f
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
hB' : ⟨h, hH⟩ +ᵥ B = B
⊢ g +ᵥ h +ᵥ B = g +ᵥ B

Proof state:
case f
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
hB' : ⟨h, hH⟩ +ᵥ B = B
⊢ g +ᵥ h +ᵥ B = g +ᵥ B

Tactic:
congr

Result:
no goals

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)),
    g_1 +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (g_1 +ᵥ g +ᵥ B) (g +ᵥ B)

Tactic:
intro h'

Result:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)

Tactic:
obtain ⟨h, hH, hh⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h')

Result:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) h = ↑h'
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : ↑h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
exact this

Result:
no goals

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
⊢ AddAction.IsBlock (↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)) (g +ᵥ B)

Tactic:
rw [AddAction.isBlock_iff_vadd_eq_or_disjoint]

Result:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)),
    g_1 +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (g_1 +ᵥ g +ᵥ B) (g +ᵥ B)

Proof state:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) h = ↑h'
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)

Tactic:
simp only [AddEquiv.coe_toAddMonoidHom, AddAut.conj_apply] at hh

Result:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)

Proof state:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
⊢ h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Tactic:
suffices (h' : G) +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by
  exact this

Result:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
⊢ ↑h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ h' +ᵥ g +ᵥ B = g +ᵥ B ∨ Disjoint (h' +ᵥ g +ᵥ B) (g +ᵥ B)

Tactic:
simp only [this]

Result:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ g +ᵥ h +ᵥ B = g +ᵥ B ∨ Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)

Proof state:
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ g +ᵥ h +ᵥ B = g +ᵥ B ∨ Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)

Tactic:
apply (hB.vadd_eq_or_disjoint ⟨h, hH⟩).imp

Result:
case f
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ ⟨h, hH⟩ +ᵥ B = B → g +ᵥ h +ᵥ B = g +ᵥ B

case g
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
this : h' +ᵥ g +ᵥ B = g +ᵥ h +ᵥ B
⊢ Disjoint (⟨h, hH⟩ +ᵥ B) B → Disjoint (g +ᵥ h +ᵥ B) (g +ᵥ B)

Proof state:
case intro.intro
G : Type u_3
inst✝¹ : AddGroup G
X : Type u_4
inst✝ : AddAction G X
B : Set X
H : AddSubgroup G
hB : AddAction.IsBlock (↥H) B
g : G
h' : ↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)
h : G
hH : h ∈ H
hh : g + h + -g = ↑h'
⊢ (g + h + -g + g) +ᵥ B = (g + h) +ᵥ B

Tactic:
simp

Result:
no goals