internlm/Lean-Github huggingface dataset:
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
hfB' : Set.Finite B'
⊢ ∀ (g : G), a ∈ g • B' → B' ≤ g • B'
Tactic:
intro g hg x hx
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
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'
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
hfB' : Set.Finite B'
g : G
hg : a ∈ g • B'
x : X
hx : x ∈ B'
⊢ x ∈ g • B'
Tactic:
use g⁻¹ • x
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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)
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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
Theorem: MulAction.IsBlock.of_subset
Proof 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'₀
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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
Proof state after:
no goals
Theorem: MulAction.IsBlock.of_subset
Proof 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]
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
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
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
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'
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
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
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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')]
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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⁻¹]
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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]
Proof 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'
Theorem: MulAction.IsBlock.of_subset
Proof 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
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
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, ?_⟩
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
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
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
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]
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
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]
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
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'
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
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'
Proof state after:
no goals
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
⊢ commutator M ≤ N
Tactic:
have is_transN := is_qprim.pretransitive_of_normal nN hNX
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
⊢ commutator M ≤ N
Theorem: commutator_le_iwasawa
Proof state before:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
⊢ commutator M ≤ N
Tactic:
have ntα : Nontrivial α := isnontrivial_of_nontrivial_action hNX
Proof state after:
M : Type u_2
inst✝¹ : Group M
α : Type u_1
inst✝ : MulAction M α
is_qprim : IsQuasipreprimitive M α
IwaS : IwasawaStructure M α
N : Subgroup M
nN : Subgroup.Normal N
hNX : MulAction.fixedPoints (↥N) α ≠ ⊤
is_transN : MulAction.IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N