awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Pointwise (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) = HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
have refine : (⇑f : (a : α) → β) ⁻¹' (σ c • t) ⊆ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
Tactic: refine Subset.antisymm ?_ (smul_preimage_set_subsetₛₗ f c t)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Pointwise (goal)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
⊢ (⇑f : (a : α) → β) ⁻¹' (σ c • t) ⊆ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
have rw : ∀ (x : α),
  Membership.mem (γ := Set α) ((⇑f : (a : α) → β) ⁻¹' (σ c • t)) (c • x) →
    c • x ∈ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
Tactic: rw [subset_def, hc.forall]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Pointwise (hypothesis)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
x : α
y : β
hy : y ∈ t
hxy : Eq.{u_5 + 1} (α := β) ((fun (x : β) ↦ σ c • x) y : β) ((f : (a : α) → β) (c • x) : β)
⊢ c • x ∈ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
have hxy₁ : y = (f : (a : α) → β) x
Tactic: rw [map_smulₛₗ, hc'.eq_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Pointwise (hypothesis)
Goal:
M : Type u_1
N : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
σ : M → N
inst : SMul M α
inst_1 : SMul N β
inst_2 : FunLike F α β
inst_3 : MulActionSemiHomClass F σ α β
f : F
t : Set β
c : M
hc : Surjective (β := α) fun (m : α) ↦ c • m
hc' : Injective (β := β) fun (n : β) ↦ σ c • n
x : α
y : β
hy : y ∈ t
hxy : y = (f : (a : α) → β) x
⊢ c • x ∈ HSMul.hSMul (β := Set α) c ((⇑f : (a : α) → β) ⁻¹' t)
have hy₁ : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
Tactic: subst y
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
x y : X
⊢ ∃ (g : G), g • x = y
have h : Classical.arbitrary G • x = y
Tactic: use Classical.arbitrary G
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y
have h : True
Tactic: rw [eq_iff_true_of_subsingleton]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
inst_1 : Nonempty G
inst_2 : Subsingleton X
B_1 : Set X
B : IsBlock G B_1
⊢ IsTrivialBlock B_1
have h : B_1.Subsingleton
Tactic: left
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
X : Type u_2
inst : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ IsTrivialBlock B
have rw : B.ncard ≤ 1 ∨ B.ncard = Nat.card X
Tactic: rw [IsTrivialBlock, ← B.ncard_le_one_iff_subsingleton, B.eq_univ_iff_ncard]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
X : Type u_2
inst : Finite X
hX : Nat.card X ≤ 2
B : Set X
⊢ B.ncard ≤ 1 ∨ B.ncard = Nat.card X
have this : B.ncard ≤ Nat.card X
Tactic: have := B.ncard_le_card
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
⊢ IsTrivialBlock B
have inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅), IsTrivialBlock.{u_2} (X := X) ∅
Tactic: obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
Cleared hypotheses: B, hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅), IsTrivialBlock.{u_2} (X := X) ∅
⊢ IsTrivialBlock B
have inr : ∀ (b : X) (hb : b ∈ B), IsTrivialBlock B
Tactic: obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B
have inr : ∀ (g : G) (hg : g • b = a), IsTrivialBlock B
Tactic: obtain ⟨g, hg⟩ := exists_smul_eq G b a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
have inr : IsTrivialBlock (g • B)
Tactic: rw [← IsTrivialBlock.smul_iff g]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)
have apply : a ∈ g • B
Tactic: apply H _ (hB.translate g)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ a ∈ g • B
have rw : g • b ∈ g • B
Tactic: rw [← hg]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
a : X
H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
w : X
⊢ g • b ∈ g • B
have h : b ∈ B ∧ (fun (x : X) ↦ g • x) b = g • b
Tactic: use b
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ IsPretransitive G X
have rw : ∀ (x : X), ∃ (g : G), g • a = x
Tactic: rw [isPretransitive_iff_base a]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
⊢ ∀ (x : X), ∃ (g : G), g • a = x
have inl : ∀ (H : (orbit G a).Subsingleton) (x : X), ∃ (g : G), g • a = x
Tactic: rcases H (mem_orbit_self a) (IsBlock.orbit a) with H | H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
inl : ∀ (H : (orbit G a).Subsingleton) (x : X), ∃ (g : G), g • a = x
⊢ ∀ (x : X), ∃ (g : G), g • a = x
have inr : ∀ (H : orbit G a = Set.univ) (x : X), ∃ (g : G), g • a = x
Tactic: rcases H (mem_orbit_self a) (IsBlock.orbit a) with H | H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : (orbit G a).Subsingleton
⊢ ∀ (x : X), ∃ (g : G), g • a = x
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : (orbit G a).Subsingleton
⊢ False
have inl : a ∈ fixedPoints G X
Tactic: apply ha
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : (orbit G a).Subsingleton
⊢ a ∈ fixedPoints G X
have H₁ : orbit G a = {a}
Tactic: rw [Set.subsingleton_iff_singleton (mem_orbit_self a)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = {a}
g : G
⊢ Membership.mem (γ := Set X) {a} (g • a)
have inl : g • a ∈ orbit G a
Tactic: rw [← H]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H_1 : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
H : orbit G a = Set.univ
x : X
⊢ ∃ (g : G), g • a = x
have inr : Membership.mem (γ := Set X) Set.univ x
Tactic: rw [← MulAction.mem_orbit_iff, H]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
⊢ IsTrivialBlock B
have inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅), IsTrivialBlock.{u_2} (X := X) ∅
Tactic: obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
Cleared hypotheses: B, hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
inl : ∀ (hB : IsBlock.{u_1, u_2} G (X := X) ∅), IsTrivialBlock.{u_2} (X := X) ∅
⊢ IsTrivialBlock B
have inr : ∀ (b : X) (hb : b ∈ B), IsTrivialBlock B
Tactic: obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B
have inr : ∀ (g : G) (hg : g • b = a), IsTrivialBlock B
Tactic: obtain ⟨g, hg⟩ := exists_smul_eq G b a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
have inr : IsTrivialBlock (g • B)
Tactic: rw [← IsTrivialBlock.smul_iff g]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
Hnt : fixedPoints G X ≠ ⊤
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
⊢ IsPreprimitive G X
have Hnt₁ : ∃ (a : X), a ∉ fixedPoints G X
Tactic: simp only [Set.top_eq_univ, Set.ne_univ_iff_exists_notMem] at Hnt
Cleared hypotheses: Hnt
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Hnt : ∃ (a : X), a ∉ fixedPoints G X
⊢ IsPreprimitive G X
have obtain : ∀ (w : X) (ha : w ∉ fixedPoints G X), IsPreprimitive G X
Tactic: obtain ⟨_, ha⟩ := Hnt
Cleared hypotheses: Hnt
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst_4 : IsPreprimitive M α
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock B
have rw : IsTrivialBlock.{u_6} (X := β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B))
Tactic: rw [← Set.image_preimage_eq B hf]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
inst_4 : IsPreprimitive M α
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsBlock N B
⊢ IsTrivialBlock.{u_6} (X := β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) ⁻¹' B))
have apply : IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
Tactic: apply IsTrivialBlock.image hf
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ IsPreprimitive M α ↔ IsPreprimitive N β
have mp : IsPreprimitive M α → IsPreprimitive N β
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
mp : IsPreprimitive M α → IsPreprimitive N β
⊢ IsPreprimitive M α ↔ IsPreprimitive N β
have mpr : IsPreprimitive N β → IsPreprimitive M α
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
⊢ IsPreprimitive M α
have this : IsPretransitive M α
Tactic: haveI := (isPretransitive_congr hφ hf).mpr toIsPretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
M : Type u_3
inst : Group M
α : Type u_4
inst_1 : MulAction M α
N : Type u_5
β : Type u_6
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
h : IsPreprimitive N β
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
have rw : IsTrivialBlock.{u_4} (X := α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) ((⇑f : (a : α) → β) '' B))
Tactic: rw [← Set.preimage_image_eq B hf.injective]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
⊢ IsSimpleOrder.{u_4} (BlockMem G a) ↔ IsPreprimitive G X
have mp : IsSimpleOrder.{u_4} (BlockMem G a) → IsPreprimitive G X
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
mp : IsSimpleOrder.{u_4} (BlockMem G a) → IsPreprimitive G X
⊢ IsSimpleOrder.{u_4} (BlockMem G a) ↔ IsPreprimitive G X
have mpr : IsPreprimitive G X → IsSimpleOrder.{u_4} (BlockMem G a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
⊢ IsPreprimitive G X
have mp : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B
Tactic: apply IsPreprimitive.of_isTrivialBlock_base a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ IsTrivialBlock B
have mp : ∀ (hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B sorry) ⊥), IsTrivialBlock B
Tactic: rcases h_bot_or_top ⟨B, haB, hB⟩ with hB' | hB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
mp : ∀ (hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊥), IsTrivialBlock B
⊢ IsTrivialBlock B
have mp₁ : ∀ (hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B sorry) ⊤), IsTrivialBlock B
Tactic: rcases h_bot_or_top ⟨B, haB, hB⟩ with hB' | hB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊥
⊢ IsTrivialBlock B
have hB'₁ : B = (↑⊥ : Set X)
Tactic: simp only [← Subtype.coe_inj] at hB'
Cleared hypotheses: hB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊤
⊢ IsTrivialBlock B
have hB'₁ : B = (↑⊤ : Set X)
Tactic: simp only [← Subtype.coe_inj] at hB'
Cleared hypotheses: hB'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊥ : Set X)
⊢ IsTrivialBlock B
have mp : B.Subsingleton
Tactic: left
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊥ : Set X)
⊢ B.Subsingleton
have mp : Set.Subsingleton.{u_4} (α := X) (↑⊥ : Set X)
Tactic: rw [hB']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊤ : Set X)
⊢ IsTrivialBlock B
have mp : B = Set.univ
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
h : IsSimpleOrder.{u_4} (BlockMem G a)
h_bot_or_top : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤ := ⋯
B : Set X
haB : a ∈ B
hB : IsBlock G B
hB' : B = (↑⊤ : Set X)
⊢ B = Set.univ
have mp : Eq.{u_4 + 1} (α := Set X) (↑⊤ : Set X) Set.univ
Tactic: rw [hB']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
⊢ IsSimpleOrder.{u_4} (BlockMem G a)
have mpr : ∀ (a_1 : BlockMem G a), a_1 = ⊥ ∨ a_1 = ⊤
Tactic: apply IsSimpleOrder.mk
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊥ ∨
    Eq (α := BlockMem G a) (Subtype.mk (p := fun (B : Set X) ↦ a ∈ B ∧ IsBlock G B) B ⋯) ⊤
have mpr : B = (↑⊥ : Set X) ∨ B = (↑⊤ : Set X)
Tactic: simp only [← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (hypothesis)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ B = (↑⊥ : Set X) ∨ B = (↑⊤ : Set X)
have x : IsTrivialBlock B
Tactic: cases hGX'.isTrivialBlock_of_isBlock hB with
    | inl h =>
      simp [BlockMem.coe_bot, h.eq_singleton_of_mem haB]
    | inr h =>
      simp [BlockMem.coe_top, h]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
⊢ IsCoatom (α := Subgroup G) (stabilizer G a) ↔ IsPreprimitive G X
have rw : IsSimpleOrder.{u_3} (↑(Set.Ici (stabilizer G a)) : Type u_3) ↔ IsSimpleOrder.{u_4} (BlockMem G a)
Tactic: rw [← isSimpleOrder_blockMem_iff_isPreprimitive G a, ← Set.isSimpleOrder_Ici_iff_isCoatom]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
⊢ IsSimpleOrder.{u_3} (↑(Set.Ici (stabilizer G a)) : Type u_3) ↔ IsSimpleOrder.{u_4} (BlockMem G a)
have simp : IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔ IsCoatom.{u_4} (α := BlockMem G a) ⊥
Tactic: simp only [isSimpleOrder_iff_isCoatom_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Primitive (goal)
Goal:
G : Type u_3
inst : Group G
X : Type u_4
inst_1 : MulAction G X
inst_2 : IsPretransitive G X
inst_3 : Nontrivial X
a : X
⊢ IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔ IsCoatom.{u_4} (α := BlockMem G a) ⊥
have rw : IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3)) ⊥ ↔
  IsCoatom.{u_3} (α := (↑(Set.Ici (stabilizer G a)) : Type u_3))
    (((block_stabilizerOrderIso G a :
          OrderIso.{u_4, u_3} { B : Set X // a ∈ B ∧ IsBlock G B } (↑(Set.Ici (stabilizer G a)) : Type u_3)) :
        (a_1 : { B : Set X // a ∈ B ∧ IsBlock G B }) → (↑(Set.Ici (stabilizer G a)) : Type u_3))
      ⊥)
Tactic: rw [← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a), OrderIso.map_bot]