internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_3
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ 1 = Equiv.Perm.sign y
Tactic:
apply symm
Proof state after:
case h.e'_3.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Equiv.Perm.sign y = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_3.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Equiv.Perm.sign y = 1
Tactic:
convert Equiv.Perm.sign_one
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ y = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ y = 1
Tactic:
rw [← Equiv.Perm.card_support_le_one]
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Equiv.Perm.support y).card ≤ 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ (Equiv.Perm.support y).card ≤ 1
Tactic:
apply le_trans (Finset.card_le_univ _)
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) ≤ 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) ≤ 1
Tactic:
change Fintype.card (MulAction.fixedBy α g) ≤ 1
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(MulAction.fixedBy α g) ≤ 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card ↑(MulAction.fixedBy α g) ≤ 1
Tactic:
rw [OnCycleFactors.Equiv.Perm.card_fixedBy g, tsub_le_iff_left]
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
Tactic:
exact h_fixed
Proof state after:
no goals
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ x ∈ Set.range ⇑(θ g)
Tactic:
rw [← OnCycleFactors.hφ_ker_eq_θ_range, this]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ConjAct.toConjAct x ∈ Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ⊤
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ConjAct.toConjAct x ∈ Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ⊤
Tactic:
simp only [Subgroup.coeSubtype, Subgroup.mem_map, Subgroup.mem_top, true_and]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ∃ x_1, ↑x_1 = ConjAct.toConjAct x
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
this : MonoidHom.ker (φ g) = ⊤
⊢ ∃ x_1, ↑x_1 = ConjAct.toConjAct x
Tactic:
exact ⟨⟨x, hx⟩, rfl⟩
Proof state after:
no goals
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
this : MonoidHom.range (φ g) = ⊥
⊢ y ∈ MonoidHom.ker (φ g)
Tactic:
rw [MonoidHom.mem_ker, ← Subgroup.mem_bot, ← this, MonoidHom.mem_range]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
this : MonoidHom.range (φ g) = ⊥
⊢ ∃ x, (φ g) x = (φ g) y
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
x : ConjAct (Equiv.Perm α)
hx : x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
y : ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
a✝ : y ∈ ⊤
this : MonoidHom.range (φ g) = ⊥
⊢ ∃ x, (φ g) x = (φ g) y
Tactic:
exact ⟨y, rfl⟩
Proof state after:
no goals
Theorem: IsPreprimitive.has_trivial_blocks
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
h : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ Set.Subsingleton B ∨ B = ⊤
Tactic:
apply h.has_trivial_blocks'
Proof state after:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
h : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ IsBlock G B
Theorem: IsPreprimitive.has_trivial_blocks
Proof state before:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
h : IsPreprimitive G X
B : Set X
hB : IsBlock G B
⊢ IsBlock G B
Tactic:
exact hB
Proof state after:
no goals
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ IsPreprimitive G X
Tactic:
have : IsPretransitive G X := by
  apply IsPretransitive.mk
  intro x y
  use Classical.arbitrary G
  rw [eq_iff_true_of_subsingleton]
  trivial
Proof state after:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ IsPreprimitive G X
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ IsPreprimitive G X
Tactic:
apply IsPreprimitive.mk
Proof state after:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
⊢ ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Tactic:
intro B _
Proof state after:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ IsTrivialBlock B
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case has_trivial_blocks'
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ IsTrivialBlock B
Tactic:
left
Proof state after:
case has_trivial_blocks'.h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ Set.Subsingleton B
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case has_trivial_blocks'.h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
this : IsPretransitive G X
B : Set X
a✝ : IsBlock G B
⊢ Set.Subsingleton B
Tactic:
exact Set.subsingleton_of_subsingleton
Proof state after:
no goals
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ IsPretransitive G X
Tactic:
apply IsPretransitive.mk
Proof state after:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ ∀ (x y : X), ∃ g, g • x = y
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
⊢ ∀ (x y : X), ∃ g, g • x = y
Tactic:
intro x y
Proof state after:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case exists_smul_eq
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y
Tactic:
use Classical.arbitrary G
Proof state after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y
Tactic:
rw [eq_iff_true_of_subsingleton]
Proof state after:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True
Theorem: IsPreprimitive.on_subsingleton
Proof state before:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True
Tactic:
trivial
Proof state after:
no goals
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
⊢ IsTrivialBlock B
Tactic:
cases' le_or_lt (Fintype.card B) 1 with h1 h1
Proof state after:
case inl
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ IsTrivialBlock B

case inr
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ IsTrivialBlock B
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
case inl
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_left
Proof state after:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Set.Subsingleton B
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Set.Subsingleton B
Tactic:
rw [← Set.subsingleton_coe, ← Fintype.card_le_one_iff_subsingleton]
Proof state after:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Fintype.card ↑B ≤ 1
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
case inl.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : Fintype.card ↑B ≤ 1
⊢ Fintype.card ↑B ≤ 1
Tactic:
exact h1
Proof state after:
no goals
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
case inr
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ IsTrivialBlock B
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ B = ⊤
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ B = ⊤
Tactic:
rw [Set.top_eq_univ, ← set_fintype_card_eq_univ_iff]
Proof state after:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ Fintype.card ↑B = Fintype.card X
Theorem: IsTrivialBlock.of_card_le_2
Proof state before:
case inr.h
G : Type ?u.3301
X : Type u_1
inst✝ : Fintype X
hX : Fintype.card X ≤ 2
B : Set X
h1 : 1 < Fintype.card ↑B
⊢ Fintype.card ↑B = Fintype.card X
Tactic:
exact le_antisymm (set_fintype_card_le_univ B) (le_trans hX h1)
Proof state after:
no goals
Theorem: isTrivialBlock_of_block
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : IsTrivialBlock B
⊢ IsTrivialBlock (g • B)
Tactic:
cases hB with
| inl hB =>
  left
  apply Set.Subsingleton.image hB
| inr hB =>
  apply Or.intro_right
  rw [hB, eq_top_iff]
  intro x _
  rw [Set.mem_smul_set_iff_inv_smul_mem]
  exact Set.mem_univ _
Proof state after:
no goals
Theorem: isTrivialBlock_of_block
Proof state before:
case inl
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : Set.Subsingleton B
⊢ IsTrivialBlock (g • B)
Tactic:
left
Proof state after:
case inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : Set.Subsingleton B
⊢ Set.Subsingleton (g • B)
Theorem: isTrivialBlock_of_block
Proof state before:
case inl.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : Set.Subsingleton B
⊢ Set.Subsingleton (g • B)
Tactic:
apply Set.Subsingleton.image hB
Proof state after:
no goals
Theorem: isTrivialBlock_of_block
Proof state before:
case inr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ IsTrivialBlock (g • B)
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ g • B = ⊤
Theorem: isTrivialBlock_of_block
Proof state before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ g • B = ⊤
Tactic:
rw [hB, eq_top_iff]
Proof state after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ ⊤ ≤ g • ⊤
Theorem: isTrivialBlock_of_block
Proof state before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
⊢ ⊤ ≤ g • ⊤
Tactic:
intro x _
Proof state after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ x ∈ g • ⊤
Theorem: isTrivialBlock_of_block
Proof state before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ x ∈ g • ⊤
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem]
Proof state after:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ g⁻¹ • x ∈ ⊤
Theorem: isTrivialBlock_of_block
Proof state before:
case inr.h
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hB : B = ⊤
x : X
a✝ : x ∈ ⊤
⊢ g⁻¹ • x ∈ ⊤
Tactic:
exact Set.mem_univ _
Proof state after:
no goals
Theorem: isTrivialBlock_of_block_iff
Proof state before:
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock B ↔ IsTrivialBlock (g • B)
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B
Theorem: isTrivialBlock_of_block_iff
Proof state before:
case mp
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B
Tactic:
exact isTrivialBlock_of_block g
Proof state after:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B
Theorem: isTrivialBlock_of_block_iff
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B
Tactic:
intro hgB
Proof state after:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B
Theorem: isTrivialBlock_of_block_iff
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B
Tactic:
rw [← inv_smul_smul g B]
Proof state after:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g⁻¹ • g • B)
Theorem: isTrivialBlock_of_block_iff
Proof state before:
case mpr
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g⁻¹ • g • B)
Tactic:
apply isTrivialBlock_of_block
Proof state after:
case mpr.hB
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B)
Theorem: isTrivialBlock_of_block_iff
Proof state before:
case mpr.hB
G : Type u_2
X : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G X
B : Set X
g : G
hgB : IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B)
Tactic:
exact hgB
Proof state after:
no goals