awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
⊢ (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
have pos : x = a → (b ∈ S ↔ x ∈ S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
pos : x = a → (b ∈ S ↔ x ∈ S)
⊢ (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
have pos₁ : ¬x = a → x = b → (a ∈ S ↔ x ∈ S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
α : Type u_1
inst : DecidableEq α
S : Set α
a b : α
h : a ∈ S ↔ b ∈ S
x : α
pos : x = a → (b ∈ S ↔ x ∈ S)
pos₁ : ¬x = a → x = b → (a ∈ S ↔ x ∈ S)
⊢ (if x = a then b else if x = b then a else x) ∈ S ↔ x ∈ S
have neg : ¬x = a → ¬x = b → (x ∈ S ↔ x ∈ S)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s
have mp : H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
mp : H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s
have mpr : (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s ⊆ s
have mp : g • s = s
Tactic: apply Eq.subset
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s = s
have mpr : s ⊆ g • s
Tactic: apply subset_antisymm (hyp g hg)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ x ∈ g • s
have h : g⁻¹ • x ∈ s ∧ (fun (x : α) ↦ g • x) (g⁻¹ • x) = x
Tactic: use g⁻¹ • x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun (x : α) ↦ g • x) (g⁻¹ • x) = x
have h : g⁻¹ • x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
h : g⁻¹ • x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun (x : α) ↦ g • x) (g⁻¹ • x) = x
have h₁ : (fun (x : α) ↦ g • x) (g⁻¹ • x) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s
have h : g⁻¹ • x ∈ g⁻¹ • s
Tactic: apply hyp g⁻¹ (inv_mem hg)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
⊢ Eq.{u_1 + 1} (α := Subgroup Rˣ) (MulAction.stabilizer Rˣ x) ⊥
have rw : LE.le.{u_1} (α := Subgroup Rˣ) (MulAction.stabilizer Rˣ x) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
⊢ Membership.mem (γ := Subgroup Rˣ) (MulAction.stabilizer Rˣ x) g → Membership.mem (γ := Subgroup Rˣ) ⊥ g
have x₁ : ∀ (hg : (↑g : R) • x = x), Membership.mem (γ := Subgroup Rˣ) ⊥ g
Tactic: (hg : g.val • x = x)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
⊢ Membership.mem (γ := Subgroup Rˣ) ⊥ g
have huv : (↑g : R) = (↑1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
⊢ (↑g : R) = (↑1 : R)
have huv : (↑g : R) - (↑1 : R) = 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
⊢ (↑g : R) = (↑1 : R)
have huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
⊢ (↑g : R) = (↑1 : R)
have huv₂ : ((↑g : R) - 1) • x = 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
huv₂ : ((↑g : R) - 1) • x = 0
⊢ (↑g : R) = (↑1 : R)
have huv₃ : (↑g : R) • x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
huv₂ : ((↑g : R) - 1) • x = 0
huv₃ : (↑g : R) • x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
⊢ (↑g : R) = (↑1 : R)
have huv₄ : x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
huv₂ : ((↑g : R) - 1) • x = 0
huv₃ : (↑g : R) • x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
huv₄ : x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
⊢ (↑g : R) = (↑1 : R)
have huv₅ : x - x = 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
x : M
hx : x ≠ 0
g : Rˣ
hg : (↑g : R) • x = x
huv : (↑g : R) - (↑1 : R) = 0
huv₁ : ((↑g : R) - (↑1 : R)) • x = 0
huv₂ : ((↑g : R) - 1) • x = 0
huv₃ : (↑g : R) • x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
huv₄ : x - HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x = 0
huv₅ : x - x = 0
⊢ (↑g : R) = (↑1 : R)
have huv₆ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [← sub_eq_zero, ← smul_eq_zero_iff_left hx, Units.val_one, sub_smul, hg, one_smul, sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
a b : X
⊢ orbit G a = orbit G b ∨ Disjoint (orbit G a) (orbit G b)
have apply : ¬Disjoint (orbit G a) (orbit G b) → orbit G a = orbit G b
Tactic: apply (em (Disjoint (orbit G a) (orbit G b))).symm.imp _ id
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
x y : X
h : Ne.{u_2 + 1} (α := Set X) ((fun (x : X) ↦ orbit G x) x) ((fun (x : X) ↦ orbit G x) y)
⊢ Function.onFun.{u_2 + 1, u_2 + 1, 1} (α := Set X) Disjoint id ((fun (x : X) ↦ orbit G x) x)
    ((fun (x : X) ↦ orbit G x) y)
have contrapose! : ∀ (h : ¬Function.onFun Disjoint id (orbit G x) (orbit G y)), orbit G x = orbit G y
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
⊢ Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit G a)
have h₂ : ∀ (a : X), ∃ (x : Set X), Membership.mem (γ := Set (Set X)) (range fun (x : X) ↦ orbit G x) x ∧ a ∈ x
Tactic: apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
h₂ : ∀ (a : X), ∃ (x : Set X), Membership.mem (γ := Set (Set X)) (range fun (x : X) ↦ orbit G x) x ∧ a ∈ x
⊢ Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit G a)
have h₃ : ∅ ∉ range fun (x : X) ↦ orbit G x
Tactic: apply orbit.pairwiseDisjoint.isPartition_of_exists_of_ne_empty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : IsTrivialBlock B
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
have inl : ∀ (hB : B.Subsingleton), IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
Tactic: obtain hB | hB := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : IsTrivialBlock B
inl : ∀ (hB : B.Subsingleton), IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
have inr : ∀ (hB : B = univ), IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
Tactic: obtain hB | hB := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B.Subsingleton
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
have inl : Set.Subsingleton.{u_6} (α := β) ((⇑f : (a : α) → β) '' B)
Tactic: apply Or.intro_left
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B = univ
⊢ IsTrivialBlock.{u_6} (X := β) ((⇑f : (a : α) → β) '' B)
have inr : Eq.{u_6 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) univ
Tactic: apply Or.intro_right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set α
hB : B = univ
⊢ Eq.{u_6 + 1} (α := Set β) ((⇑f : (a : α) → β) '' B) univ
have inr : Eq.{u_6 + 1} (α := Set β) (Set.image.{u_4, u_6} (α := α) (⇑f : (a : α) → β) univ) univ
Tactic: rw [hB]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsTrivialBlock B
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
have inl : ∀ (hB : B.Subsingleton), IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
Tactic: obtain hB | hB := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : IsTrivialBlock B
inl : ∀ (hB : B.Subsingleton), IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
have inr : ∀ (hB : B = univ), IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
Tactic: obtain hB | hB := hB
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B.Subsingleton
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
have inl : Set.Subsingleton.{u_4} (α := α) ((⇑f : (a : α) → β) ⁻¹' B)
Tactic: apply Or.intro_left
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B = univ
⊢ IsTrivialBlock.{u_4} (X := α) ((⇑f : (a : α) → β) ⁻¹' B)
have inr : Eq.{u_4 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' B) univ
Tactic: apply Or.intro_right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst : Monoid M
inst_1 : MulAction M α
inst_2 : Monoid N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective.{u_4 + 1, u_6 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
B : Set β
hB : B = univ
⊢ Eq.{u_4 + 1} (α := Set α) ((⇑f : (a : α) → β) ⁻¹' B) univ
have inr : Eq.{u_4 + 1} (α := Set α) (Set.preimage.{u_4, u_6} (β := β) (⇑f : (a : α) → β) univ) univ
Tactic: simp only [hB]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B.Subsingleton
⊢ IsTrivialBlock (g • B)
have inl : (g • B).Subsingleton
Tactic: left
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B = univ
⊢ IsTrivialBlock (g • B)
have inr : g • B = univ
Tactic: right
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B = univ
⊢ g • B = univ
have inr : HSMul.hSMul (β := Set α) g univ = univ
Tactic: rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B = univ
inr : HSMul.hSMul (β := Set α) g univ = univ
⊢ g • B = univ
have inr₁ : Eq.{u_4 + 1} (α := Set α) ((fun (x : α) ↦ g • x) '' univ) univ
Tactic: rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
h : B = univ
inr : HSMul.hSMul (β := Set α) g univ = univ
inr₁ : Eq.{u_4 + 1} (α := Set α) ((fun (x : α) ↦ g • x) '' univ) univ
⊢ g • B = univ
have inr₂ : Eq.{u_4 + 1} (α := Set α) univ univ
Tactic: rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
hB : IsTrivialBlock B
g : M
⊢ IsTrivialBlock (g • B)
have inl : ∀ (h : B.Subsingleton), IsTrivialBlock (g • B)
Tactic: cases hB with
  | inl h =>
    left
    exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h
  | inr h =>
    right
    rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
hB : IsTrivialBlock B
g : M
inl : ∀ (h : B.Subsingleton), IsTrivialBlock (g • B)
⊢ IsTrivialBlock (g • B)
have inr : ∀ (h : B = univ), IsTrivialBlock (g • B)
Tactic: cases hB with
  | inl h =>
    left
    exact (Function.Injective.subsingleton_image_iff (MulAction.injective g)).mpr h
  | inr h =>
    right
    rw [h, ← Set.image_smul, Set.image_univ_of_surjective (MulAction.surjective g)]
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) ↔ IsTrivialBlock B
have mp : IsTrivialBlock (g • B) → IsTrivialBlock B
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
mp : IsTrivialBlock (g • B) → IsTrivialBlock B
⊢ IsTrivialBlock (g • B) ↔ IsTrivialBlock B
have mpr : IsTrivialBlock B → IsTrivialBlock (g • B)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
M : Type u_3
α : Type u_4
inst : Group M
inst_1 : MulAction M α
B : Set α
g : M
H : IsTrivialBlock (g • B)
⊢ IsTrivialBlock B
have h : B = g⁻¹ • g • B
Tactic: convert! IsTrivialBlock.smul H g⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
have simp_rw : (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
  ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
Tactic: simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
simp_rw :
  (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
    ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B
have simp_rw₁ : (∀ ⦃g₁ g₂ : G⦄, g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)) ↔
  ∀ ⦃g₁ g₂ : G⦄, ¬Disjoint (g₁ • B) (g₂ • B) → g₁ • B = g₂ • B
Tactic: simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
⊢ g₁ • B = g₂ • B
have by_contra! : ∀ (hg' : g₁ • B ≠ g₂ • B), False
Tactic: by_contra! hg'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
⊢ False
have hB₁ : IsBlock.{u_1, u_2} G (X := X) ∅
Tactic: obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg
Cleared hypotheses: B, hB, hg, hg'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
hB₁ : IsBlock.{u_1, u_2} G (X := X) ∅
⊢ False
have hg₁ : HSMul.hSMul (β := Set X) g₁ ∅ ⊆ HSMul.hSMul (β := Set X) g₂ ∅
Tactic: obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg
Cleared hypotheses: B, hB, hg, hg'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
g₁ g₂ : G
hB : IsBlock G B
hg : g₁ • B ⊆ g₂ • B
hg' : g₁ • B ≠ g₂ • B
hB₁ : IsBlock.{u_1, u_2} G (X := X) ∅
hg₁ : HSMul.hSMul (β := Set X) g₁ ∅ ⊆ HSMul.hSMul (β := Set X) g₂ ∅
⊢ False
have hg'₁ : HSMul.hSMul (β := Set X) g₁ ∅ ≠ HSMul.hSMul (β := Set X) g₂ ∅
Tactic: obtain rfl : B = ∅ := by simpa using (hB hg').eq_bot_of_le hg
Cleared hypotheses: B, hB, hg, hg'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
X : Type u_2
inst : SMul G X
B : Set X
s : Set G
g : G
hB : IsBlock G B
hgs : ¬g • B ⊆ s • B
⊢ Disjoint (g • B) (s • B)
have rw : ∀ (i : G) (j : i ∈ s), Disjoint (g • B) (i • B)
Tactic: rw [← iUnion_smul_set, disjoint_iUnion₂_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
have refine : ∀ (hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) (g₁ g₂ : G) (h : g₁ • B ≠ g₂ • B), Disjoint (g₁ • B) (g₂ • B)
Tactic: refine ⟨fun hB g ↦ by simpa using hB (g₂ := 1), fun hB g₁ g₂ h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : g₁ • B ≠ g₂ • B
⊢ Disjoint (g₁ • B) (g₂ • B)
have simp : ∀ (h : ¬(g₂⁻¹ * g₁) • B = B), Disjoint ((g₂⁻¹ * g₁) • B) B
Tactic: simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
have simp_rw : (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
Tactic: simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B : Set X
simp_rw : (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
⊢ IsBlock G B ↔ ∀ ⦃g : G⦄, (g • B ∩ B).Nonempty → g • B = B
have simp_rw₁ : (∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B) ↔ ∀ ⦃g : G⦄, ¬Disjoint (g • B) B → g • B = B
Tactic: simp_rw [isBlock_iff_disjoint_smul_of_ne, ← not_disjoint_iff_nonempty_inter, not_imp_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
X : Type u_2
inst_1 : MulAction G X
B₁ B₂ : Set X
h₁ : IsBlock G B₁
h₂ : IsBlock G B₂
⊢ IsBlock G (B₁ ∩ B₂)
have simp : ∀ (h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁)
  (h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂) ⦃g₁ g₂ : G⦄,
  (g₁ • B₁ ∩ g₁ • B₂ ∩ (g₂ • B₁ ∩ g₂ • B₂)).Nonempty → g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂
Tactic: simp only [isBlock_iff_smul_eq_smul_of_nonempty, smul_set_inter] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂