internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsBlock.of_subset
Proof 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⟩)
Proof 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)
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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)
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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'
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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'
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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'
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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']
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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⟩)
Proof state after:
no goals