internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : Equiv.Perm.cycleType ↑k = 0
⊢ False
Tactic:
apply hk'
Proof state after:
case intro.intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : Equiv.Perm.cycleType ↑k = 0
⊢ k = 1
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : Equiv.Perm.cycleType ↑k = 0
⊢ k = 1
Tactic:
rw [Equiv.Perm.cycleType_eq_zero] at hk2
Proof state after:
case intro.intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : ↑k = 1
⊢ k = 1
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : ↑k = 1
⊢ k = 1
Tactic:
simp only [← Subtype.coe_inj, hk2, Subgroup.coe_one]
Proof state after:
no goals
Theorem: alternatingGroup.V4_eq_commutator
Proof state before:
case intro.intro.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Normal (V4 α)
comm_le : commutator ↥(alternatingGroup α) ≤ V4 α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
k : ↥(alternatingGroup α)
hk : k ∈ commutator ↥(alternatingGroup α)
hk' : k ≠ 1
hk2 : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
exact hk2
Proof state after:
no goals
Theorem: MulAction.IsBlock.def
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)

case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → IsBlock G B
Theorem: MulAction.IsBlock.def
Proof state before:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro hB g g'
Proof state after:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def
Proof state before:
case mp
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
by_cases h : g • B = g' • B
Proof state after:
case pos
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)

case neg
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def
Proof state before:
case pos
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
refine' Or.intro_left _ h
Proof state after:
no goals
Theorem: MulAction.IsBlock.def
Proof state before:
case neg
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_right
Proof state after:
case neg.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def
Proof state before:
case neg.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : IsBlock G B
g g' : G
h : ¬g • B = g' • B
⊢ Disjoint (g • B) (g' • B)
Tactic:
exact hB (Set.mem_range_self g) (Set.mem_range_self g') h
Proof state after:
no goals
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → IsBlock G B
Tactic:
intro hB
Proof state after:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ IsBlock G B
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ IsBlock G B
Tactic:
unfold IsBlock
Proof state after:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ Set.PairwiseDisjoint (Set.range fun g => g • B) id
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
⊢ Set.PairwiseDisjoint (Set.range fun g => g • B) id
Tactic:
intro C hC C' hC'
Proof state after:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C : Set X
hC : C ∈ Set.range fun g => g • B
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
⊢ C ≠ C' → (Disjoint on id) C C'
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C : Set X
hC : C ∈ Set.range fun g => g • B
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
⊢ C ≠ C' → (Disjoint on id) C C'
Tactic:
obtain ⟨g, rfl⟩ := hC
Proof state after:
case mpr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
g : G
⊢ (fun g => g • B) g ≠ C' → (Disjoint on id) ((fun g => g • B) g) C'
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
C' : Set X
hC' : C' ∈ Set.range fun g => g • B
g : G
⊢ (fun g => g • B) g ≠ C' → (Disjoint on id) ((fun g => g • B) g) C'
Tactic:
obtain ⟨g', rfl⟩ := hC'
Proof state after:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
⊢ (fun g => g • B) g ≠ (fun g => g • B) g' → (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
⊢ (fun g => g • B) g ≠ (fun g => g • B) g' → (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
intro hgg'
Proof state after:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr.intro.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
cases hB g g' with
| inl h => exfalso; exact hgg' h
| inr h => exact h
Proof state after:
no goals
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr.intro.intro.inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : g • B = g' • B
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
exfalso
Proof state after:
case mpr.intro.intro.inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : g • B = g' • B
⊢ False
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr.intro.intro.inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : g • B = g' • B
⊢ False
Tactic:
exact hgg' h
Proof state after:
no goals
Theorem: MulAction.IsBlock.def
Proof state before:
case mpr.intro.intro.inr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g g' : G
hgg' : (fun g => g • B) g ≠ (fun g => g • B) g'
h : Disjoint (g • B) (g' • B)
⊢ (Disjoint on id) ((fun g => g • B) g) ((fun g => g • B) g')
Tactic:
exact h
Proof state after:
no goals
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ (g g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Tactic:
rw [IsBlock.def]
Proof state after:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Tactic:
apply forall_congr'
Proof state after:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ ∀ (a : G), (∀ (g' : G), a • B = g' • B ∨ Disjoint (a • B) (g' • B)) ↔ ∀ (g' : G), a • B ∩ g' • B ≠ ∅ → a • B = g' • B
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
⊢ ∀ (a : G), (∀ (g' : G), a • B = g' • B ∨ Disjoint (a • B) (g' • B)) ↔ ∀ (g' : G), a • B ∩ g' • B ≠ ∅ → a • B = g' • B
Tactic:
intro g
Proof state after:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g : G
⊢ (∀ (g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g : G
⊢ (∀ (g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g' : G), g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Tactic:
apply forall_congr'
Proof state after:
case h.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g : G
⊢ ∀ (a : G), g • B = a • B ∨ Disjoint (g • B) (a • B) ↔ g • B ∩ a • B ≠ ∅ → g • B = a • B
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
case h.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g : G
⊢ ∀ (a : G), g • B = a • B ∨ Disjoint (g • B) (a • B) ↔ g • B ∩ a • B ≠ ∅ → g • B = a • B
Tactic:
intro g'
Proof state after:
case h.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B) ↔ g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
case h.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B) ↔ g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Tactic:
rw [Set.disjoint_iff_inter_eq_empty]
Proof state after:
case h.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g g' : G
⊢ g • B = g' • B ∨ g • B ∩ g' • B = ∅ ↔ g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Theorem: MulAction.IsBlock.mk_notempty
Proof state before:
case h.h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
g g' : G
⊢ g • B = g' • B ∨ g • B ∩ g' • B = ∅ ↔ g • B ∩ g' • B ≠ ∅ → g • B = g' • B
Tactic:
exact or_iff_not_imp_right
Proof state after:
no goals
Theorem: MulAction.IsBlock_of_fixed
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ IsBlock G B
Tactic:
rw [IsBlock.def]
Proof state after:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock_of_fixed
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro g g'
Proof state after:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock_of_fixed
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_left
Proof state after:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
g g' : G
⊢ g • B = g' • B
Theorem: MulAction.IsBlock_of_fixed
Proof state before:
case h
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
g g' : G
⊢ g • B = g' • B
Tactic:
rw [hfB g, hfB g']
Proof state after:
no goals
Theorem: MulAction.bot_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ IsBlock G ⊥
Tactic:
rw [IsBlock.def]
Proof state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ ∀ (g g' : G), g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)
Theorem: MulAction.bot_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ ∀ (g g' : G), g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)
Tactic:
intro g g'
Proof state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)
Theorem: MulAction.bot_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥ ∨ Disjoint (g • ⊥) (g' • ⊥)
Tactic:
apply Or.intro_left
Proof state after:
case h
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥
Theorem: MulAction.bot_IsBlock
Proof state before:
case h
G : Type u_1
X : Type u_2
inst✝ : SMul G X
g g' : G
⊢ g • ⊥ = g' • ⊥
Tactic:
simp only [Set.bot_eq_empty, Set.smul_set_empty]
Proof state after:
no goals
Theorem: MulAction.singleton_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
⊢ IsBlock G {a}
Tactic:
rw [IsBlock.def]
Proof state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
⊢ ∀ (g g' : G), g • {a} = g' • {a} ∨ Disjoint (g • {a}) (g' • {a})
Theorem: MulAction.singleton_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
⊢ ∀ (g g' : G), g • {a} = g' • {a} ∨ Disjoint (g • {a}) (g' • {a})
Tactic:
intro g g'
Proof state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • {a} = g' • {a} ∨ Disjoint (g • {a}) (g' • {a})
Theorem: MulAction.singleton_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • {a} = g' • {a} ∨ Disjoint (g • {a}) (g' • {a})
Tactic:
simp only [Set.smul_set_singleton, Set.singleton_eq_singleton_iff, Set.disjoint_singleton, Ne.def]
Proof state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • a = g' • a ∨ ¬g • a = g' • a
Theorem: MulAction.singleton_IsBlock
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
g g' : G
⊢ g • a = g' • a ∨ ¬g • a = g' • a
Tactic:
apply em
Proof state after:
no goals
Theorem: MulAction.subsingleton_IsBlock
Proof state before:
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
⊢ IsBlock G B
Tactic:
cases Set.Subsingleton.eq_empty_or_singleton hB with
| inl h => rw [h]; apply bot_IsBlock
| inr h => obtain ⟨a, ha⟩ := h; rw [ha]; apply singleton_IsBlock
Proof state after:
no goals
Theorem: MulAction.subsingleton_IsBlock
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : B = ∅
⊢ IsBlock G B
Tactic:
rw [h]
Proof state after:
case inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : B = ∅
⊢ IsBlock G ∅
Theorem: MulAction.subsingleton_IsBlock
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : B = ∅
⊢ IsBlock G ∅
Tactic:
apply bot_IsBlock
Proof state after:
no goals
Theorem: MulAction.subsingleton_IsBlock
Proof state before:
case inr
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
h : ∃ x, B = {x}
⊢ IsBlock G B
Tactic:
obtain ⟨a, ha⟩ := h
Proof state after:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G B
Theorem: MulAction.subsingleton_IsBlock
Proof state before:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G B
Tactic:
rw [ha]
Proof state after:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G {a}
Theorem: MulAction.subsingleton_IsBlock
Proof state before:
case inr.intro
G : Type u_2
X : Type u_1
inst✝ : SMul G X
B : Set X
hB : Set.Subsingleton B
a : X
ha : B = {a}
⊢ IsBlock G {a}
Tactic:
apply singleton_IsBlock
Proof state after:
no goals
Theorem: MulAction.IsBlock.def_one
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
rw [IsBlock.def]
Proof state after:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.def_one
Proof state before:
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) ↔ ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B

case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), g • B = B ∨ Disjoint (g • B) B) → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)) → ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
Tactic:
intro hB g
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
g : G
⊢ g • B = B ∨ Disjoint (g • B) B
Tactic:
simpa only [one_smul] using hB g 1
Proof state after:
no goals
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
⊢ (∀ (g : G), g • B = B ∨ Disjoint (g • B) B) → ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro hB
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
⊢ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
⊢ ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
intro g g'
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
cases hB (g'⁻¹ * g) with
| inl h =>
  apply Or.intro_left
  rw [← inv_inv g', eq_inv_smul_iff, smul_smul]
  exact h
| inr h =>
  apply Or.intro_right
  rw [Set.disjoint_iff] at h ⊢
  rintro x ⟨hx, hx'⟩
  simp only [Set.mem_empty_iff_false]
  suffices g'⁻¹ • x ∈ (g'⁻¹ * g) • B ⊓ B by
    apply h this
  simp only [Set.inf_eq_inter, Set.mem_inter_iff]
  simp only [← Set.mem_smul_set_iff_inv_smul_mem]
  rw [← smul_smul]; rw [smul_inv_smul]
  exact ⟨hx, hx'⟩
Proof state after:
no goals
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inl
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B = B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_left
Proof state after:
case mpr.inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B = B
⊢ g • B = g' • B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B = B
⊢ g • B = g' • B
Tactic:
rw [← inv_inv g', eq_inv_smul_iff, smul_smul]
Proof state after:
case mpr.inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B = B
⊢ (g'⁻¹ * g) • B = B
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inl.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B = B
⊢ (g'⁻¹ * g) • B = B
Tactic:
exact h
Proof state after:
no goals
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : Disjoint ((g'⁻¹ * g) • B) B
⊢ g • B = g' • B ∨ Disjoint (g • B) (g' • B)
Tactic:
apply Or.intro_right
Proof state after:
case mpr.inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : Disjoint ((g'⁻¹ * g) • B) B
⊢ Disjoint (g • B) (g' • B)
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : Disjoint ((g'⁻¹ * g) • B) B
⊢ Disjoint (g • B) (g' • B)
Tactic:
rw [Set.disjoint_iff] at h ⊢
Proof state after:
case mpr.inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
⊢ g • B ∩ g' • B ⊆ ∅
Theorem: MulAction.IsBlock.def_one
Proof state before:
case mpr.inr.h
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
⊢ g • B ∩ g' • B ⊆ ∅
Tactic:
rintro x ⟨hx, hx'⟩
Proof state after:
case mpr.inr.h.intro
G : Type u_2
inst✝¹ : Group G
X : Type u_1
inst✝ : MulAction G X
B : Set X
hB : ∀ (g : G), g • B = B ∨ Disjoint (g • B) B
g g' : G
h : (g'⁻¹ * g) • B ∩ B ⊆ ∅
x : X
hx : x ∈ g • B
hx' : x ∈ g' • B
⊢ x ∈ ∅