awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
⊢ (↑h' : G) • g • B = g • h • B
have rw : (g * h * g⁻¹) • g • B = g • h • B
Tactic: rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_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
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
rw : (g * h * g⁻¹) • g • B = g • h • B
⊢ (↑h' : G) • g • B = g • h • B
have rw₁ : (g * h * g⁻¹ * g) • B = g • h • B
Tactic: rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_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
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
rw : (g * h * g⁻¹) • g • B = g • h • B
rw₁ : (g * h * g⁻¹ * g) • B = g • h • B
⊢ (↑h' : G) • g • B = g • h • B
have rw₂ : (g * h * g⁻¹ * g) • B = (g * h) • B
Tactic: rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_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
H : Subgroup G
hB : IsBlock.{u_1, u_2} (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = (↑h' : G)
rw : (g * h * g⁻¹) • g • B = g • h • B
rw₁ : (g * h * g⁻¹ * g) • B = g • h • B
rw₂ : (g * h * g⁻¹ * g) • B = (g * h) • B
⊢ (↑h' : G) • g • B = g • h • B
have rw₃ : (g * h) • B = (g * h) • B
Tactic: rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock G B
⊢ AddAction.IsBlock G (g +ᵥ B)
have rw : ∀ (hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B), AddAction.IsBlock.{u_3, u_4} (↥⊤) (g +ᵥ B)
Tactic: rw [← AddAction.isBlock_top] at hB ⊢
Cleared hypotheses: hB
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
⊢ AddAction.IsBlock.{u_3, u_4} (↥⊤) (g +ᵥ B)
have rw : AddAction.IsBlock.{u_3, u_4}
  (↥(AddSubgroup.map (G := G)
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      (AddSubgroup.comap (N := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        ⊤)))
  (g +ᵥ B)
Tactic: rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
rw :
  AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.map (G := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (AddSubgroup.comap (N := G)
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          ⊤)))
    (g +ᵥ B)
⊢ AddAction.IsBlock.{u_3, u_4} (↥⊤) (g +ᵥ B)
have rw₁ : G →+ G
Tactic: rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
rw :
  AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.map (G := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (AddSubgroup.comap (N := G)
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          ⊤)))
    (g +ᵥ B)
rw₁ : G →+ G
⊢ AddAction.IsBlock.{u_3, u_4} (↥⊤) (g +ᵥ B)
have rw₂ : Function.Surjective.{u_3 + 1, u_3 + 1} (α := G) (β := G)
  (⇑(AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g))) :
    (a : G) → G)
Tactic: rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_3
inst : AddGroup G
X : Type u_4
inst_1 : AddAction G X
B : Set X
g : G
hB : AddAction.IsBlock.{u_3, u_4} (↥⊤) B
⊢ AddAction.IsBlock.{u_3, u_4}
    (↥(AddSubgroup.map (G := G)
        (AddEquiv.toAddMonoidHom
          ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
        (AddSubgroup.comap (N := G)
          (AddEquiv.toAddMonoidHom
            ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
          ⊤)))
    (g +ᵥ B)
have hB₁ : AddAction.IsBlock.{u_3, u_4}
  (↥(AddSubgroup.comap (N := G)
      (AddEquiv.toAddMonoidHom
        ((Additive.toMul : (a : Additive (AddAut G)) → AddAut G) ((AddAut.conj : (a : G) → Additive (AddAut G)) g)))
      ⊤))
  B
Tactic: apply AddAction.IsBlock.of_addSubgroup_of_conjugate
-- 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
g : G
hB : IsBlock G B
⊢ IsBlock G (g • B)
have rw : ∀ (hB : IsBlock.{u_1, u_2} (↥⊤) B), IsBlock.{u_1, u_2} (↥⊤) (g • B)
Tactic: rw [← isBlock_top] at hB ⊢
Cleared hypotheses: hB
-- 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
g : G
hB : IsBlock.{u_1, u_2} (↥⊤) B
⊢ IsBlock.{u_1, u_2} (↥⊤) (g • B)
have rw : IsBlock.{u_1, u_2}
  (↥(Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G)
      (Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)))
  (g • B)
Tactic: rw [← Subgroup.map_comap_eq_self_of_surjective
          (G := G) (f := MulAut.conj g) (MulAut.conj g).surjective ⊤]
-- 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
g : G
hB : IsBlock.{u_1, u_2} (↥⊤) B
⊢ IsBlock.{u_1, u_2}
    (↥(Subgroup.map (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G)
        (Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)))
    (g • B)
have hB₁ : IsBlock.{u_1, u_2} (↥(Subgroup.comap (↑((MulAut.conj : (a : G) → MulAut G) g : MulAut G) : G →* G) ⊤)) B
Tactic: apply IsBlock.of_subgroup_of_conjugate
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (g : G) ↦ g • B)
have nonempty : ∅ ∉ range fun (g : G) ↦ g • B
Tactic: refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
nonempty : ∅ ∉ range fun (g : G) ↦ g • B
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (g : G) ↦ g • B)
have cover : ∀ (a : X), ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
Tactic: refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
nonempty : ∅ ∉ range fun (g : G) ↦ g • B
cover : ∀ (a : X), ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (g : G) ↦ g • B)
have refine : ∀ ⦃B_1 : Set X⦄, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) B_1 → IsBlock G B_1
Tactic: refine ⟨⟨?nonempty, ?cover⟩, ?mem_blocks⟩
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∅ ∉ range fun (g : G) ↦ g • B
have nonempty : ∀ (x : G), ¬x • B = ∅
Tactic: simp only [Set.mem_range, not_exists]
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
g : G
hg : g • B = ∅
⊢ False
have nonempty : B = ∅
Tactic: apply hBe.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
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
a : X
⊢ ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
have cover : ∀ (b : X) (hb : b ∈ B), ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
Tactic: obtain ⟨b : X, hb : b ∈ B⟩ := hBe
Cleared hypotheses: hBe
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
a b : X
hb : b ∈ B
⊢ ∃! b : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b ∧ a ∈ b
have cover : ∀ (g : G), ∃! b_1 : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1
Tactic: obtain ⟨g, rfl⟩ := exists_smul_eq G b a
Cleared hypotheses: a
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ ∃! b_1 : Set X, Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1
have h : (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) (g • B) ∧
  ∀ (y : Set X),
    (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) y → y = g • B
Tactic: use g • B
-- 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
hGX : IsPretransitive G X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
⊢ (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) (g • B) ∧
    ∀ (y : Set X),
      (fun (b_1 : Set X) ↦ Membership.mem (γ := Set (Set X)) (range fun (g : G) ↦ g • B) b_1 ∧ g • b ∈ b_1) y →
        y = g • B
have h : ∀ (a : G), g • b ∈ a • B → a • B = g • B
Tactic: simp only [Set.smul_mem_smul_set_iff, hb, Set.mem_range,
      exists_apply_eq_apply, and_imp, forall_exists_index,
      forall_apply_eq_imp_iff, true_and]
-- 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
N : Subgroup G
nN : N.Normal
a : X
g : G
⊢ g • orbit.{u_1, u_2} (↥N) a = orbit.{u_1, u_2} (↥N) (g • a)
have simp : Eq.{u_2 + 1} (α := Set X) (range fun (i : ↥N) ↦ g • i • a) (range fun (m : ↥N) ↦ m • g • a)
Tactic: simp only [orbit, Set.smul_set_range]
-- 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
N : Subgroup G
nN : N.Normal
a : X
g : G
⊢ Eq.{u_2 + 1} (α := Set X) (range fun (i : ↥N) ↦ g • i • a) (range fun (m : ↥N) ↦ m • g • a)
have h : ∀ (x : X),
  Membership.mem (γ := Set X) (range fun (i : ↥N) ↦ g • i • a) x ↔
    Membership.mem (γ := Set X) (range fun (m : ↥N) ↦ m • g • a) x
Tactic: ext
-- 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
N : Subgroup G
nN : N.Normal
a : X
g : G
x : X
⊢ (∃ (y : ↥N), g • y • a = x) ↔ ∃ (y : ↥N), y • g • a = x
have h : (∃ (y : ↥N), g • y • a = x) → ∃ (y : ↥N), y • g • a = x
Tactic: constructor
-- 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
N : Subgroup G
nN : N.Normal
a : X
g : G
x : X
h : (∃ (y : ↥N), g • y • a = x) → ∃ (y : ↥N), y • g • a = x
⊢ (∃ (y : ↥N), g • y • a = x) ↔ ∃ (y : ↥N), y • g • a = x
have h₁ : (∃ (y : ↥N), y • g • a = x) → ∃ (y : ↥N), g • y • a = x
Tactic: constructor
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ (y : ↥N), y • g • a = g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • a
have h : Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g * k * g⁻¹) sorry • g • a = g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • a
Tactic: use ⟨g * k * g⁻¹, nN.conj_mem k hk g⟩
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g * k * g⁻¹) ⋯ • g • a = g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • a
have h : (g * k * g⁻¹) • g • a = g • k • a
Tactic: simp only [Subgroup.mk_smul]
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ (g * k * g⁻¹) • g • a = g • k • a
have h : (g * k * g⁻¹ * g) • a = g • k • a
Tactic: rw [smul_smul, inv_mul_cancel_right, ← smul_smul]
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : (g * k * g⁻¹ * g) • a = g • k • a
⊢ (g * k * g⁻¹) • g • a = g • k • a
have h₁ : (g * k) • a = g • k • a
Tactic: rw [smul_smul, inv_mul_cancel_right, ← smul_smul]
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
h : (g * k * g⁻¹ * g) • a = g • k • a
h₁ : (g * k) • a = g • k • a
⊢ (g * k * g⁻¹) • g • a = g • k • a
have h₂ : g • k • a = g • k • a
Tactic: rw [smul_smul, inv_mul_cancel_right, ← smul_smul]
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ ∃ (y : ↥N), g • y • a = Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • g • a
have h : g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g⁻¹ * k * g) sorry • a = Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • g • a
Tactic: use ⟨g⁻¹ * k * g, nN.conj_mem' k hk g⟩
-- 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
N : Subgroup G
nN : N.Normal
a : X
g k : G
hk : k ∈ N
⊢ g • Subtype.mk (p := fun (x : G) ↦ x ∈ N) (g⁻¹ * k * g) ⋯ • a = Subtype.mk (p := fun (x : G) ↦ x ∈ N) k hk • g • a
have h : g • (g⁻¹ * k * g) • a = k • g • a
Tactic: simp only [Subgroup.mk_smul]
-- 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
N : Subgroup G
inst_2 : N.Normal
a : X
⊢ IsBlock G (orbit.{u_1, u_2} (↥N) a)
have rw : ∀ (g : G),
  g • orbit.{u_1, u_2} (↥N) a = orbit.{u_1, u_2} (↥N) a ∨
    Disjoint (g • orbit.{u_1, u_2} (↥N) a) (orbit.{u_1, u_2} (↥N) a)
Tactic: rw [isBlock_iff_smul_eq_or_disjoint]
-- 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
N : Subgroup G
inst_2 : N.Normal
a : X
g : G
⊢ g • orbit.{u_1, u_2} (↥N) a = orbit.{u_1, u_2} (↥N) a ∨
    Disjoint (g • orbit.{u_1, u_2} (↥N) a) (orbit.{u_1, u_2} (↥N) a)
have rw : orbit.{u_1, u_2} (↥N) (g • a) = orbit.{u_1, u_2} (↥N) a ∨
  Disjoint (orbit.{u_1, u_2} (↥N) (g • a)) (orbit.{u_1, u_2} (↥N) a)
Tactic: rw [smul_orbit_eq_orbit_smul]
-- 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
N : Subgroup G
inst_2 : N.Normal
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)
have left : Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)
Tactic: constructor
-- 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
N : Subgroup G
inst_2 : N.Normal
left : Setoid.IsPartition.{u_2} (α := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)
⊢ IsBlockSystem.{u_1, u_2} G (X := X) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a)
have right : ∀ ⦃B : Set X⦄, Membership.mem (γ := Set (Set X)) (range fun (a : X) ↦ orbit.{u_1, u_2} (↥N) a) B → IsBlock G B
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
⊢ IsBlock G (↑s : Set H)
have simp : ∀ ⦃g₁ g₂ : G⦄, g₁ • (↑s : Set H) ≠ g₂ • (↑s : Set H) → ∀ ⦃a : H⦄, a ∈ g₁ • (↑s : Set H) → a ∉ g₂ • (↑s : Set H)
Tactic: simp only [IsBlock, disjoint_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
⊢ False
have refine : a • (↑s : Set H) = b • (↑s : Set H)
Tactic: refine hab ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
Tactic: rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₁ : (a • c) • (↑s : Set H) = b • c • (↑s : Set H)
Tactic: rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
rw₁ : (a • c) • (↑s : Set H) = b • c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₂ : (b • d) • (↑s : Set H) = b • c • (↑s : Set H)
Tactic: rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
rw₁ : (a • c) • (↑s : Set H) = b • c • (↑s : Set H)
rw₂ : (b • d) • (↑s : Set H) = b • c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₃ : b • d • (↑s : Set H) = b • c • (↑s : Set H)
Tactic: rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
rw₁ : (a • c) • (↑s : Set H) = b • c • (↑s : Set H)
rw₂ : (b • d) • (↑s : Set H) = b • c • (↑s : Set H)
rw₃ : b • d • (↑s : Set H) = b • c • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₄ : b • d • (↑s : Set H) = b • (↑s : Set H)
Tactic: rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G H H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
rw : a • c • (↑s : Set H) = b • c • (↑s : Set H)
rw₁ : (a • c) • (↑s : Set H) = b • c • (↑s : Set H)
rw₂ : (b • d) • (↑s : Set H) = b • c • (↑s : Set H)
rw₃ : b • d • (↑s : Set H) = b • c • (↑s : Set H)
rw₄ : b • d • (↑s : Set H) = b • (↑s : Set H)
⊢ a • (↑s : Set H) = b • (↑s : Set H)
have rw₅ : b • (↑s : Set H) = b • (↑s : Set H)
Tactic: rw [← smul_coe_set hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe_set hc, smul_coe_set hd]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
⊢ IsBlock G (↑s : Set H)
have simp : ∀ ⦃g₁ g₂ : G⦄, g₁ • (↑s : Set H) ≠ g₂ • (↑s : Set H) → ∀ ⦃a : H⦄, a ∈ g₁ • (↑s : Set H) → a ∉ g₂ • (↑s : Set H)
Tactic: simp only [IsBlock, disjoint_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Blocks (goal)
Goal:
G : Type u_1
inst : Group G
S : Type u_3
H : Type u_4
inst_1 : Group H
inst_2 : SetLike S H
inst_3 : SubgroupClass S H
s : S
inst_4 : MulAction G H
inst_5 : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • (↑s : Set H) ≠ b • (↑s : Set H)
c : H
hc : c ∈ (↑s : Set H)
d : H
hd : d ∈ (↑s : Set H)
hcd : b • d = a • c
⊢ False
have refine : a • (↑s : Set H) = b • (↑s : Set H)
Tactic: refine hab ?_