internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ g⁻¹ • x ∈ g⁻¹ • B
Tactic:
rw [Set.smul_mem_smul_set_iff]
Proof state after:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ B
Theorem: MulAction.IsBlock_of_invariant
Proof state before:
case h.a.a
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hfB : IsInvariantBlock G B
g : G
x : X
hx : x ∈ B
⊢ x ∈ B
Tactic:
exact hx
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_orbit
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
⊢ IsBlock G (orbit G a)
Tactic:
apply IsBlock_of_fixed
Proof state after:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
⊢ IsFixedBlock G (orbit G a)
Theorem: MulAction.IsBlock_of_orbit
Proof state before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
⊢ IsFixedBlock G (orbit G a)
Tactic:
intro g
Proof state after:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
g : G
⊢ g • orbit G a = orbit G a
Theorem: MulAction.IsBlock_of_orbit
Proof state before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
g : G
⊢ g • orbit G a = orbit G a
Tactic:
apply smul_orbit
Proof state after:
no goals
Theorem: MulAction.top_IsBlock
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsBlock G ⊤
Tactic:
apply IsBlock_of_fixed
Proof state after:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsFixedBlock G ⊤
Theorem: MulAction.top_IsBlock
Proof state before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ IsFixedBlock G ⊤
Tactic:
intro g
Proof state after:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
g : G
⊢ g • ⊤ = ⊤
Theorem: MulAction.top_IsBlock
Proof state before:
case hfB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
g : G
⊢ g • ⊤ = ⊤
Tactic:
simp only [Set.top_eq_univ, Set.smul_set_univ]
Proof state after:
no goals
Theorem: MulAction.Subgroup.IsBlock
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
⊢ MulAction.IsBlock (↥H) B
Tactic:
rw [IsBlock.def_one]
Proof state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
⊢ ∀ (g : ↥H), g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.Subgroup.IsBlock
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
⊢ ∀ (g : ↥H), g • B = B ∨ Disjoint (g • B) B
Tactic:
rintro ⟨g, _⟩
Proof state after:
case mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
g : G
property✝ : g ∈ H
⊢ { val := g, property := property✝ } • B = B ∨ Disjoint ({ val := g, property := property✝ } • B) B
Theorem: MulAction.Subgroup.IsBlock
Proof state before:
case mk
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
B : Set X
hfB : MulAction.IsBlock G B
g : G
property✝ : g ∈ H
⊢ { val := g, property := property✝ } • B = B ∨ Disjoint ({ val := g, property := property✝ } • B) B
Tactic:
simpa only using IsBlock.def_one.mp hfB g
Proof state after:
no goals
Theorem: MulAction.IsBlock_preimage
Proof state before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
⊢ IsBlock H (⇑j ⁻¹' B)
Tactic:
rw [IsBlock.def_one]
Proof state after:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
⊢ ∀ (g : H), g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Theorem: MulAction.IsBlock_preimage
Proof state before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
⊢ ∀ (g : H), g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
intro g
Proof state after:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Theorem: MulAction.IsBlock_preimage
Proof state before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
cases' IsBlock.def_one.mp hB (φ g) with heq hdis
Proof state after:
case inl
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)

case inr
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Theorem: MulAction.IsBlock_preimage
Proof state before:
case inl
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
apply Or.intro_left
Proof state after:
case inl.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B
Theorem: MulAction.IsBlock_preimage
Proof state before:
case inl.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
heq : φ g • B = B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B
Tactic:
rw [← Set.preimage_smul_setₑ, heq]
Proof state after:
no goals
Theorem: MulAction.IsBlock_preimage
Proof state before:
case inr
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ g • ⇑j ⁻¹' B = ⇑j ⁻¹' B ∨ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Theorem: MulAction.IsBlock_preimage
Proof state before:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (g • ⇑j ⁻¹' B) (⇑j ⁻¹' B)
Tactic:
rw [← Set.preimage_smul_setₑ]
Proof state after:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (⇑j ⁻¹' (φ g • B)) (⇑j ⁻¹' B)
Theorem: MulAction.IsBlock_preimage
Proof state before:
case inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (⇑j ⁻¹' (φ g • B)) (⇑j ⁻¹' B)
Tactic:
apply Disjoint.preimage
Proof state after:
case inr.h.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (φ g • B) B
Theorem: MulAction.IsBlock_preimage
Proof state before:
case inr.h.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : H → G
j : Y →ₑ[φ] X
B : Set X
hB : IsBlock G B
g : H
hdis : Disjoint (φ g • B) B
⊢ Disjoint (φ g • B) B
Tactic:
exact hdis
Proof state after:
no goals
Theorem: MulAction.IsBlock_image
Proof state before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
⊢ IsBlock H (⇑j '' B)
Tactic:
rw [IsBlock.def]
Proof state after:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
⊢ ∀ (g g' : H), g • ⇑j '' B = g' • ⇑j '' B ∨ Disjoint (g • ⇑j '' B) (g' • ⇑j '' B)
Theorem: MulAction.IsBlock_image
Proof state before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
⊢ ∀ (g g' : H), g • ⇑j '' B = g' • ⇑j '' B ∨ Disjoint (g • ⇑j '' B) (g' • ⇑j '' B)
Tactic:
intro h h'
Proof state after:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h h' : H
⊢ h • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (h • ⇑j '' B) (h' • ⇑j '' B)
Theorem: MulAction.IsBlock_image
Proof state before:
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h h' : H
⊢ h • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (h • ⇑j '' B) (h' • ⇑j '' B)
Tactic:
obtain ⟨g, rfl⟩ := hφ h
Proof state after:
case intro
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h' : H
g : G
⊢ φ g • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (h' • ⇑j '' B)
Theorem: MulAction.IsBlock_image
Proof state before:
case intro
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
h' : H
g : G
⊢ φ g • ⇑j '' B = h' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (h' • ⇑j '' B)
Tactic:
obtain ⟨g', rfl⟩ := hφ h'
Proof state after:
case intro.intro
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ φ g • ⇑j '' B = φ g' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (φ g' • ⇑j '' B)
Theorem: MulAction.IsBlock_image
Proof state before:
case intro.intro
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ φ g • ⇑j '' B = φ g' • ⇑j '' B ∨ Disjoint (φ g • ⇑j '' B) (φ g' • ⇑j '' B)
Tactic:
simp only [← Set.image_smul_setₑ]
Proof state after:
case intro.intro
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Theorem: MulAction.IsBlock_image
Proof state before:
case intro.intro
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
cases' IsBlock.def.mp hB g g' with h h
Proof state after:
case intro.intro.inl
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))

case intro.intro.inr
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Theorem: MulAction.IsBlock_image
Proof state before:
case intro.intro.inl
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
apply Or.intro_left
Proof state after:
case intro.intro.inl.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B)
Theorem: MulAction.IsBlock_image
Proof state before:
case intro.intro.inl.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MulAction.IsBlock_image
Proof state before:
case intro.intro.inr
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ ⇑j '' (g • B) = ⇑j '' (g' • B) ∨ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
apply Or.intro_right
Proof state after:
case intro.intro.inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Theorem: MulAction.IsBlock_image
Proof state before:
case intro.intro.inr.h
G : Type u_4
inst✝³ : Group G
X : Type u_3
inst✝² : MulAction G X
H : Type u_1
Y : Type u_2
inst✝¹ : Group H
inst✝ : MulAction H Y
φ : G → H
j : X →ₑ[φ] Y
hφ : Function.Surjective φ
hj : Function.Injective ⇑j
B : Set X
hB : IsBlock G B
g g' : G
h : Disjoint (g • B) (g' • B)
⊢ Disjoint (⇑j '' (g • B)) (⇑j '' (g' • B))
Tactic:
exact Set.disjoint_image_of_injective hj h
Proof state after:
no goals
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
⊢ g • Subtype.val '' B = Subtype.val '' (g • B)
Tactic:
ext
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B ↔ x✝ ∈ Subtype.val '' (g • B)
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B ↔ x✝ ∈ Subtype.val '' (g • B)
Tactic:
constructor
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B → x✝ ∈ Subtype.val '' (g • B)

case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ Subtype.val '' (g • B) → x✝ ∈ g • Subtype.val '' B
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ g • Subtype.val '' B → x✝ ∈ Subtype.val '' (g • B)
Tactic:
intro hx
Proof state after:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ g • Subtype.val '' B
⊢ x✝ ∈ Subtype.val '' (g • B)
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mp
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ g • Subtype.val '' B
⊢ x✝ ∈ Subtype.val '' (g • B)
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
Proof state after:
case h.mp.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : X
hy : y ∈ Subtype.val '' B
⊢ (fun x => g • x) y ∈ Subtype.val '' (g • B)
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mp.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : X
hy : y ∈ Subtype.val '' B
⊢ (fun x => g • x) y ∈ Subtype.val '' (g • B)
Tactic:
obtain ⟨z, hz, rfl⟩ := hy
Proof state after:
case h.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z ∈ Subtype.val '' (g • B)
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z ∈ Subtype.val '' (g • B)
Tactic:
use g • z
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B ∧ ↑(g • z) = (fun x => g • x) ↑z
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B ∧ ↑(g • z) = (fun x => g • x) ↑z
Tactic:
constructor
Proof state after:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • z ∈ g • B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z
Tactic:
exact ⟨z, hz, rfl⟩
Proof state after:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑(g • z) = (fun x => g • x) ↑z
Tactic:
rw [SubMulAction.val_smul_of_tower]
Proof state after:
no goals
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
⊢ x✝ ∈ Subtype.val '' (g • B) → x✝ ∈ g • Subtype.val '' B
Tactic:
intro hx
Proof state after:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ Subtype.val '' (g • B)
⊢ x✝ ∈ g • Subtype.val '' B
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
x✝ : X
hx : x✝ ∈ Subtype.val '' (g • B)
⊢ x✝ ∈ g • Subtype.val '' B
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
Proof state after:
case h.mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : ↥C
hy : y ∈ g • B
⊢ ↑y ∈ g • Subtype.val '' B
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
y : ↥C
hy : y ∈ g • B
⊢ ↑y ∈ g • Subtype.val '' B
Tactic:
obtain ⟨z, hz, rfl⟩ := hy
Proof state after:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑((fun x => g • x) z) ∈ g • Subtype.val '' B
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑((fun x => g • x) z) ∈ g • Subtype.val '' B
Tactic:
rw [SubMulAction.val_smul_of_tower]
Proof state after:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • ↑z ∈ g • Subtype.val '' B
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ g • ↑z ∈ g • Subtype.val '' B
Tactic:
use ↑z
Proof state after:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B ∧ (fun x => g • x) ↑z = g • ↑z
Theorem: MulAction.SubMulAction.smul_coe_eq_coe_smul
Proof state before:
case h
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B ∧ (fun x => g • x) ↑z = g • ↑z
Tactic:
constructor
Proof state after:
case h.left
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ ↑z ∈ Subtype.val '' B

case h.right
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g : G
z : ↥C
hz : z ∈ B
⊢ (fun x => g • x) ↑z = g • ↑z