awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
⊢ (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ∩ g • B).Subsingleton
have rw : Set.Subsingleton.{u_4} (α := Y) (Set.image.{u_2, u_4} (α := X) (⇑f : (a : X) → Y) ((⇑f : (a : X) → Y) ⁻¹' (g • B)))
Tactic: rw [← Set.image_preimage_eq_range_inter]
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
⊢ Set.Subsingleton.{u_4} (α := Y) (Set.image.{u_2, u_4} (α := X) (⇑f : (a : X) → Y) ((⇑f : (a : X) → Y) ⁻¹' (g • B)))
have hs : Set.Subsingleton.{u_2} (α := X) ((⇑f : (a : X) → Y) ⁻¹' (g • B))
Tactic: apply Set.Subsingleton.image
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
⊢ Set.Subsingleton.{u_2} (α := X) ((⇑f : (a : X) → Y) ⁻¹' (g • B))
have hs : ¬Eq.{u_2 + 1} (α := Set X) ((⇑f : (a : X) → Y) ⁻¹' (g • B)) Set.univ
Tactic: apply Or.resolve_right (isTrivialBlock_of_isBlock ((hB.translate g).preimage f))
-- 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
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
h : Eq.{u_2 + 1} (α := Set X) ((⇑f : (a : X) → Y) ⁻¹' (g • B)) Set.univ
⊢ False
have h₁ : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
Tactic: simp only [Set.preimage_eq_univ_iff] 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
H : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
⊢ False
have hs : B = Set.univ
Tactic: apply hB_ne_top
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
⊢ B = Set.univ
have hs : Nat.card Y < B.ncard * 2
Tactic: apply hB.eq_univ_of_card_lt
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
⊢ Nat.card Y < B.ncard * 2
have hs : 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard * 2
Tactic: apply lt_of_lt_of_le hf'
-- 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 : Type u_3
Y : Type u_4
inst_2 : Group H
inst_3 : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst_4 : Finite Y
inst_5 : IsPretransitive H Y
inst_6 : IsPreprimitive G X
hf' : Nat.card Y < 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y))
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
hfin : Fintype (↑(Set.range fun (g : H) ↦ g • B) : Type u_4)
g : H
h : Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ g • B
⊢ 2 * Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard * 2
have hs : Set.ncard.{u_4} (α := Y) (Set.range.{u_4, u_2 + 1} (ι := X) (⇑f : (a : X) → Y)) ≤ B.ncard
Tactic: rw [mul_comm, mul_le_mul_iff_left₀ Nat.succ_pos']
-- 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
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ∃ (g : G), a ∈ g • A ∧ b ∉ g • A
have this₁ : ¬∀ (i : G), Membership.mem (γ := Set X) (⋂ (_ : a ∈ i • A), i • A) b
Tactic: rw [Set.mem_iInter] at this
Cleared hypotheses: this
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
⊢ ∃ (g : G), a ∈ g • A ∧ b ∉ g • A
have suffices : b ∉ B
Tactic: suffices b ∉ B by
    rw [Set.mem_iInter] at this
    simpa only [Set.mem_iInter, not_forall, exists_prop] using this
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
this : B = {a}
⊢ b ∉ B
have rw : b ∉ {a}
Tactic: rw [this]
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B
have suffices : B = {a}
Tactic: suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm 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
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}
have inl : ∀ (hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)), B = {a}
Tactic: rcases isTrivialBlock_of_isBlock (G := G) (IsBlock.of_subset a hfA) with hyp | hyp
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
inl : ∀ (hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)), B = {a}
⊢ B = {a}
have inr : ∀ (hyp : Eq.{u_2 + 1} (α := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) Set.univ), B = {a}
Tactic: rcases isTrivialBlock_of_isBlock (G := G) (IsBlock.of_subset a hfA) with hyp | hyp
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)
⊢ B = {a}
have inl : Membership.mem (γ := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) a
Tactic: apply Set.Subsingleton.eq_singleton_of_mem hyp
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : Set.Subsingleton.{u_2} (α := X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A)
⊢ Membership.mem (γ := Set X) (⋂ (k : G), ⋂ (_ : a ∈ k • A), k • A) a
have inl : ∀ (i : G), Membership.mem (γ := Set X) (⋂ (_ : a ∈ i • A), i • A) a
Tactic: rw [Set.mem_iInter]
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
⊢ B = {a}
have inr : 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
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
⊢ False
have inr : A = Set.univ
Tactic: apply hA'
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
this : ∃ (g : G), a ∈ g • A
⊢ A = Set.univ
have obtain : ∀ (g : G) (hg : a ∈ g • A), A = Set.univ
Tactic: obtain ⟨g, hg⟩ := this
Cleared hypotheses: this
-- 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
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
⊢ A = Set.univ
have this : B ⊆ g • A
Tactic: have : B ⊆ g • A := Set.biInter_subset_of_mem hg
-- 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
inst_2 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
this : B ⊆ g • A
⊢ A = Set.univ
have this₁ : A = HSMul.hSMul (β := Set X) g⁻¹ Set.univ
Tactic: rw [hyp, Set.univ_subset_iff, ← eq_inv_smul_iff] at this
Cleared hypotheses: this
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
this : A = HSMul.hSMul (β := Set X) g⁻¹ Set.univ
⊢ A = Set.univ
have rw : HSMul.hSMul (β := Set X) g⁻¹ Set.univ = Set.univ
Tactic: rw [this, Set.smul_set_univ]
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
g : G
hg : a ∈ g • A
this : A = HSMul.hSMul (β := Set X) g⁻¹ Set.univ
rw : HSMul.hSMul (β := Set X) g⁻¹ Set.univ = Set.univ
⊢ A = Set.univ
have rw₁ : Eq.{u_2 + 1} (α := Set X) Set.univ Set.univ
Tactic: rw [this, Set.smul_set_univ]
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
⊢ A = Set.univ
have inr : ∃ (g : G), a ∈ g • A
Tactic: suffices ∃ g : G, a ∈ g • A by
      obtain ⟨g, hg⟩ := this
      have : B ⊆ g • A := Set.biInter_subset_of_mem hg
      rw [hyp, Set.univ_subset_iff, ← eq_inv_smul_iff] at this
      rw [this, Set.smul_set_univ]
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
⊢ ∃ (g : G), a ∈ g • A
have inr : ∀ (x : X) (hx : x ∈ A), ∃ (g : G), a ∈ g • A
Tactic: obtain ⟨x, hx⟩ := hA
Cleared hypotheses: hA
-- 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
⊢ ∃ (g : G), a ∈ g • A
have inr : ∀ (g : G) (hg : g • x = a), ∃ (g : G), a ∈ g • A
Tactic: obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G x 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 : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ (g : G), ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
g : G
hg : g • x = a
w : G
w₁ : X
⊢ ∃ (g : G), a ∈ g • A
have h₁ : x ∈ A ∧ (fun (x : X) ↦ g • x) x = a
Tactic: use g, x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
x x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa : (x * x_1)⁻¹ * x • x_2 ∈ H
Tactic: rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
x x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x * x_1)⁻¹ * x • x_2 ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₁ : (x * x_1)⁻¹ * (x * x_2) ∈ H
Tactic: rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
x x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x * x_1)⁻¹ * x • x_2 ∈ H
rwa₁ : (x * x_1)⁻¹ * (x * x_2) ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₂ : x_1⁻¹ * x⁻¹ * (x * x_2) ∈ H
Tactic: rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
x x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x * x_1)⁻¹ * x • x_2 ∈ H
rwa₁ : (x * x_1)⁻¹ * (x * x_2) ∈ H
rwa₂ : x_1⁻¹ * x⁻¹ * (x * x_2) ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₃ : x_1⁻¹ * (x⁻¹ * (x * x_2)) ∈ H
Tactic: rwa [smul_eq_mul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₃ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₃ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₄ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₃ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₄ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₅ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x * unop (↑b : αᵐᵒᵖ) ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₃ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₄ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₅ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x * unop (↑b : αᵐᵒᵖ) ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₆ : unop (↑b : αᵐᵒᵖ) * ((unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x) ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
b : ↥(Subgroup.op (normalizer (↑H : Set α)))
c x : α
h : c⁻¹ * x ∈ H
rwa : ((↑b : αᵐᵒᵖ) • c)⁻¹ * b • x ∈ H
rwa₁ : ((↑b : αᵐᵒᵖ) • c)⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₂ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (↑b : αᵐᵒᵖ) • x ∈ H
rwa₃ : (c * unop (↑b : αᵐᵒᵖ))⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₄ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * (x * unop (↑b : αᵐᵒᵖ)) ∈ H
rwa₅ : (unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x * unop (↑b : αᵐᵒᵖ) ∈ H
rwa₆ : unop (↑b : αᵐᵒᵖ) * ((unop (↑b : αᵐᵒᵖ))⁻¹ * c⁻¹ * x) ∈ H
⊢ (b • c)⁻¹ * b • x ∈ H
have rwa₇ : unop (↑b : αᵐᵒᵖ) * ((unop (↑b : αᵐᵒᵖ))⁻¹ * (c⁻¹ * x)) ∈ H
Tactic: rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
      mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
hH : H.Normal
x : αᵐᵒᵖ
x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa : (x_1 * unop x)⁻¹ * x • x_2 ∈ H
Tactic: rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
hH : H.Normal
x : αᵐᵒᵖ
x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x_1 * unop x)⁻¹ * x • x_2 ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₁ : (x_1 * unop x)⁻¹ * (x_2 * unop x) ∈ H
Tactic: rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
hH : H.Normal
x : αᵐᵒᵖ
x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x_1 * unop x)⁻¹ * x • x_2 ∈ H
rwa₁ : (x_1 * unop x)⁻¹ * (x_2 * unop x) ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₂ : (unop x)⁻¹ * x_1⁻¹ * (x_2 * unop x) ∈ H
Tactic: rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Quotient (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Group α
inst_1 : Monoid β
inst_2 : MulAction β α
H : Subgroup α
hH : H.Normal
x : αᵐᵒᵖ
x_1 x_2 : α
h : x_1⁻¹ * x_2 ∈ H
rwa : (x_1 * unop x)⁻¹ * x • x_2 ∈ H
rwa₁ : (x_1 * unop x)⁻¹ * (x_2 * unop x) ∈ H
rwa₂ : (unop x)⁻¹ * x_1⁻¹ * (x_2 * unop x) ∈ H
⊢ (x • x_1)⁻¹ * x • x_2 ∈ H
have rwa₃ : (unop x)⁻¹ * (x_1⁻¹ * (x_2 * unop x)) ∈ H
Tactic: rwa [smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, mul_assoc, hH.mem_comm_iff, mul_assoc,
      mul_inv_cancel_right]