Theorem: MulAction.IsBlock.of_subset (Jordan/Blocks.lean)

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
cases' Set.eq_empty_or_nonempty B with hfB_e hfB_ne
State after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
  intro k hk
  exact Set.biInter_subset_of_mem hk
State after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
have hfB' : B'.Finite := by
  obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
  obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a
  apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)
State after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
have hag' : ∀ g : G, a ∈ g • B' → B' = g • B' :=
  by
  intro g hg
  apply symm
  rw [← mem_stabilizer_iff]
  rw [← Subgroup.inv_mem_iff (stabilizer G B')]
  rw [mem_stabilizer_of_finite_iff_smul_le G B' hfB' g⁻¹]
  rw [← Set.subset_set_smul_iff]
  exact hag g hg
State after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
rw [IsBlock.mk_notempty_one]
State after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ ∀ (g : G),
    (g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B ≠ ∅ →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ ∀ (g : G),
    (g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B ≠ ∅ →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
intro g hg
State after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : (g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B ≠ ∅
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : (g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B ≠ ∅
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
rw [← Set.nonempty_iff_ne_empty] at hg
State after:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
obtain ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩ := Set.nonempty_def.mp hg
State after:
case inr.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
have hak : a ∈ k⁻¹ • B' := by
  refine ⟨b, hb, ?_⟩
  simp only [← hk, inv_smul_smul]
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
have hagk : a ∈ (k⁻¹ * g) • B' :=
  by
  rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
  exact hb'
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
have hgkB' : B' = (k⁻¹ * g) • B' := hag' (k⁻¹ * g) hagk
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = (k⁻¹ * g) • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = (k⁻¹ * g) • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
rw [mul_smul] at hgkB'
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : B' = k⁻¹ • B'
hgkB' : B' = k⁻¹ • g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'
State after:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B

State before:
case inr.intro.intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
hagk : a ∈ (k⁻¹ * g) • B'
hkB' : k • B' = B'
hgkB' : k • B' = g • B'
⊢ g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Tactic:
rw [← hgkB', hkB']
State after:
no goals

State before:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
suffices (⋂ (k : G) (_ : a ∈ k • B), k • B) = Set.univ by
  rw [this]; apply top_IsBlock
State after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ ⋂ k, ⋂ (_ : a ∈ k • B), k • B = Set.univ

State before:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ ⋂ k, ⋂ (_ : a ∈ k • B), k • B = Set.univ
Tactic:
simp only [Set.iInter_eq_univ]
State after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ ∀ (i : G), a ∈ i • B → i • B = Set.univ

State before:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ ∀ (i : G), a ∈ i • B → i • B = Set.univ
Tactic:
intro k hk
State after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
k : G
hk : a ∈ k • B
⊢ k • B = Set.univ

State before:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
k : G
hk : a ∈ k • B
⊢ k • B = Set.univ
Tactic:
exfalso
State after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
k : G
hk : a ∈ k • B
⊢ False

State before:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
k : G
hk : a ∈ k • B
⊢ False
Tactic:
rw [hfB_e] at hk
State after:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
k : G
hk : a ∈ k • ∅
⊢ False

State before:
case inl
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
k : G
hk : a ∈ k • ∅
⊢ False
Tactic:
simpa only [Set.smul_set_empty] using hk
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
this : ⋂ k, ⋂ (_ : a ∈ k • B), k • B = Set.univ
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)
Tactic:
rw [this]
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
this : ⋂ k, ⋂ (_ : a ∈ k • B), k • B = Set.univ
⊢ IsBlock G Set.univ

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
this : ⋂ k, ⋂ (_ : a ∈ k • B), k • B = Set.univ
⊢ IsBlock G Set.univ
Tactic:
apply top_IsBlock
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
⊢ ∀ (k : G), a ∈ k • B → B' ≤ k • B
Tactic:
intro k hk
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
k : G
hk : a ∈ k • B
⊢ B' ≤ k • B

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
k : G
hk : a ∈ k • B
⊢ B' ≤ k • B
Tactic:
exact Set.biInter_subset_of_mem hk
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
⊢ Set.Finite B'
Tactic:
obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
State after:
case intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
b : X
hb : b ∈ B
⊢ Set.Finite B'

State before:
case intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
b : X
hb : b ∈ B
⊢ Set.Finite B'
Tactic:
obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a
State after:
case intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
b : X
hb : b ∈ B
k : G
hk : k • b = a
⊢ Set.Finite B'

State before:
case intro.intro
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
b : X
hb : b ∈ B
k : G
hk : k • b = a
⊢ Set.Finite B'
Tactic:
apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
⊢ ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
Tactic:
intro g hg x hx
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ x ∈ g • B'

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ x ∈ g • B'
Tactic:
use g⁻¹ • x
State after:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ g⁻¹ • x ∈ B' ∧ (fun x => g • x) (g⁻¹ • x) = x

State before:
case h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ g⁻¹ • x ∈ B' ∧ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
constructor
State after:
case h.left
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ g⁻¹ • x ∈ B'

case h.right
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ (fun x => g • x) (g⁻¹ • x) = x

State before:
case h.left
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ g⁻¹ • x ∈ B'
Tactic:
apply Set.mem_biInter
State after:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ ∀ x_1 ∈ fun x => (x • B) a, g⁻¹ • x ∈ x_1 • B

State before:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ ∀ x_1 ∈ fun x => (x • B) a, g⁻¹ • x ∈ x_1 • B
Tactic:
intro k
State after:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
⊢ (k ∈ fun x => (x • B) a) → g⁻¹ • x ∈ k • B

State before:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
⊢ (k ∈ fun x => (x • B) a) → g⁻¹ • x ∈ k • B
Tactic:
rintro (hk : a ∈ k • B)
State after:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ g⁻¹ • x ∈ k • B

State before:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ g⁻¹ • x ∈ k • B
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem, smul_smul]
State after:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ (g * k) • B

State before:
case h.left.h
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ (g * k) • B
Tactic:
apply hB'₀
State after:
case h.left.h.x
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ a ∈ (g * k) • B

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'

State before:
case h.left.h.x
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ a ∈ (g * k) • B

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'
Tactic:
rw [← smul_smul, Set.mem_smul_set_iff_inv_smul_mem]
State after:
case h.left.h.x
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ g⁻¹ • a ∈ k • B

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'

State before:
case h.left.h.x
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ g⁻¹ • a ∈ k • B

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'
Tactic:
apply hB'₀ k hk
State after:
case h.left.h.x.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ g⁻¹ • a ∈ B'

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'

State before:
case h.left.h.x.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ g⁻¹ • a ∈ B'

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
State after:
case h.left.h.x.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ a ∈ g • B'

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'

State before:
case h.left.h.x.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ a ∈ g • B'

case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'
Tactic:
exact hg
State after:
case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'

State before:
case h.left.h.a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
k : G
hk : a ∈ k • B
⊢ x ∈ B'
Tactic:
exact hx
State after:
no goals

State before:
case h.right
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
simp only [smul_inv_smul]
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
⊢ ∀ (g : G), a ∈ g • B' → B' = g • B'
Tactic:
intro g hg
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' = g • B'

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' = g • B'
Tactic:
apply symm
State after:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g • B' = B'

State before:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g • B' = B'
Tactic:
rw [← mem_stabilizer_iff]
State after:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g ∈ stabilizer G B'

State before:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g ∈ stabilizer G B'
Tactic:
rw [← Subgroup.inv_mem_iff (stabilizer G B')]
State after:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g⁻¹ ∈ stabilizer G B'

State before:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g⁻¹ ∈ stabilizer G B'
Tactic:
rw [mem_stabilizer_of_finite_iff_smul_le G B' hfB' g⁻¹]
State after:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g⁻¹ • B' ⊆ B'

State before:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ g⁻¹ • B' ⊆ B'
Tactic:
rw [← Set.subset_set_smul_iff]
State after:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'

State before:
case a
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
g : G
hg : a ∈ g • B'
⊢ B' ⊆ g • B'
Tactic:
exact hag g hg
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ a ∈ k⁻¹ • B'
Tactic:
refine ⟨b, hb, ?_⟩
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ (fun x => k⁻¹ • x) b = a

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
⊢ (fun x => k⁻¹ • x) b = a
Tactic:
simp only [← hk, inv_smul_smul]
State after:
no goals

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ a ∈ (k⁻¹ * g) • B'
Tactic:
rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
State after:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ b ∈ g • B'

State before:
G : Type u_2
inst✝² : Group G
X : Type u_1
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
a : X
B : Set X
hfB : Set.Finite B
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_ne : Set.Nonempty B
hB'₀ : ∀ (k : G), a ∈ k • B → B' ≤ k • B
hfB' : Set.Finite B'
hag : ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
g : G
hg : Set.Nonempty ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B)
b : X
hb' : b ∈ g • B'
hb : b ∈ B'
k : G
hk : k • a = b
hak : a ∈ k⁻¹ • B'
⊢ b ∈ g • B'
Tactic:
exact hb'
State after:
no goals