awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP :
  Eq.{u_1 + 1} (α := ↥(map (MonoidHom.fst G H) I))
    ((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.fst G H) I))
    (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (map (MonoidHom.fst G H) I) a) g ⋯ :
      ↥(map (MonoidHom.fst G H) I))
hQ :
  Eq.{u_2 + 1} (α := ↥(map (MonoidHom.snd G H) I))
    ((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.snd G H) I))
    (Subtype.mk (p := fun (a : H) ↦ Membership.mem (γ := Subgroup H) (map (MonoidHom.snd G H) I) a) h ⋯ :
      ↥(map (MonoidHom.snd G H) I))
⊢ (g, h) ∈ I
have hP₁ : (↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) sorry)) : G) = g
Tactic: simp only [Subtype.ext_iff] at hP hQ
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP :
  Eq.{u_1 + 1} (α := ↥(map (MonoidHom.fst G H) I))
    ((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.fst G H) I))
    (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (map (MonoidHom.fst G H) I) a) g ⋯ :
      ↥(map (MonoidHom.fst G H) I))
hQ :
  Eq.{u_2 + 1} (α := ↥(map (MonoidHom.snd G H) I))
    ((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.snd G H) I))
    (Subtype.mk (p := fun (a : H) ↦ Membership.mem (γ := Subgroup H) (map (MonoidHom.snd G H) I) a) h ⋯ :
      ↥(map (MonoidHom.snd G H) I))
hP₁ : (↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G) = g
⊢ (g, h) ∈ I
have hQ₁ : (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) sorry)) : H) = h
Tactic: simp only [Subtype.ext_iff] at hP hQ
Cleared hypotheses: hP, hQ
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : (↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G) = g
hQ : (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : H) = h
⊢ (g, h) ∈ I
have h₃ : ((↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) sorry)) : G), h) ∈ I
Tactic: rwa [← hP, ← hQ]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : (↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G) = g
hQ : (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : H) = h
h₃ :
  ((↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G), h) ∈ I
⊢ (g, h) ∈ I
have h₄ : ((↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) sorry)) : G),
    (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) sorry)) : H)) ∈
  I
Tactic: rwa [← hP, ← hQ]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
⊢ MonoidHom.ker
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) ≤
    (P.prod Q).range
have h : MonoidHom.ker
    (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
      (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) =
  (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Tactic: convert! goursatFst_prod_goursatSnd_le (P.prod Q).range
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := MonoidHom.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
⊢ MonoidHom.ker
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) =
    (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
have h : ∀ (g : ↥(map (MonoidHom.fst G H) I)) (h : ↥(map (MonoidHom.snd G H) I)),
  (g, h) ∈
      MonoidHom.ker
        (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
          (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Tactic: ext ⟨g, h⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.1 ∈ orbit M y.1
have rcases : ∀ (g : M), ((fun (m : M) ↦ m • y) g).1 ∈ orbit M y.1
Tactic: rcases h with ⟨g, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.2 ∈ orbit M y.2
have rcases : ∀ (g : M), ((fun (m : M) ↦ m • y) g).2 ∈ orbit M y.2
Tactic: rcases h with ⟨g, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a
have mp : (orbit M a).Subsingleton → ∀ (m : M), m • a = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
a : α
mp : (orbit M a).Subsingleton → ∀ (m : M), m • a = a
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a
have mpr : (∀ (m : M), m • a = a) → (orbit M a).Subsingleton
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a = b
have rw : a - b = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ a - b = 0
have refine : k • (a - b) = 0
Tactic: refine h _ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
⊢ k • (a - b) = 0
have rw : k • a - k • b = 0
Tactic: rw [smul_sub, h', sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
rw : k • a - k • b = 0
⊢ k • (a - b) = 0
have rw₁ : k • b - k • b = 0
Tactic: rw [smul_sub, h', sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
M : Type u_1
G : Type u_2
inst : Monoid M
inst_1 : AddGroup G
inst_2 : DistribMulAction M G
k : M
h : ∀ (x : G), k • x = 0 → x = 0
a b : G
h' : k • a = k • b
rw : k • a - k • b = 0
rw₁ : k • b - k • b = 0
⊢ k • (a - b) = 0
have rw₂ : Eq.{u_2 + 1} (α := G) 0 0
Tactic: rw [smul_sub, h', sub_self]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Subsingleton α
⊢ fixedPoints G α = Set.univ
have a : ∀ (x : α), x ∈ fixedPoints G α
Tactic: apply Set.eq_univ_of_forall
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g h : G
⊢ ∃ (g_1 : G),
    g_1 • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯ =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯
have h₁ : (h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) sorry =
  Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) sorry
Tactic: use h * g⁻¹
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a : α
g h : G
⊢ (h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) ⋯ =
    Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) ⋯
have h₁ : (↑((h * g⁻¹) • Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) g) sorry) : α) =
  (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ orbit G a) ((fun (m : G) ↦ m • a) h) sorry) : α)
Tactic: ext1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
⊢ orbitRel.{u_1, u_2} (↥(H.subgroupOf K)) α = orbitRel.{u_1, u_2} (↥(H ⊓ K)) α
have rw : orbitRel.{u_1, u_2} (↥(H.subgroupOf K)) α = orbitRel.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) α
Tactic: rw [← Subgroup.subgroupOf_map_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
⊢ orbitRel.{u_1, u_2} (↥(H.subgroupOf K)) α = orbitRel.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) α
have a : ∀ (x b : α),
  (orbitRel (↥(H.subgroupOf K)) α : α → α → Prop) x b ↔
    (orbitRel (↥(Subgroup.map K.subtype (H.subgroupOf K))) α : α → α → Prop) x b
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
⊢ x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b ↔ x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
have a : ∀ (h : x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b), x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
a :
  ∀ (h : x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b),
    x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
⊢ x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b ↔ x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
have a₁ : ∀ (h : x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b), x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
h : x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
⊢ x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
have a : ∀ (gv : ↥K) (gp : gv ∈ H.subgroupOf K),
  (fun (m : ↥(H.subgroupOf K)) ↦ m • b) (Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K) gv gp) ∈
    orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
Tactic: rcases h with ⟨⟨gv, gp⟩, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : ↥K
gp : gv ∈ H.subgroupOf K
⊢ Subtype.mk (p := fun (x : ↥K) ↦ x ∈ H.subgroupOf K) gv gp • b ∈
    orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
have a : (↑gv : G) ∈ Subgroup.map K.subtype (H.subgroupOf K)
Tactic: refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
x b : α
h : x ∈ orbit.{u_1, u_2} (↥(Subgroup.map K.subtype (H.subgroupOf K))) b
⊢ x ∈ orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
have a : ∀ (gv : G) (gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)),
  (fun (m : ↥(Subgroup.map K.subtype (H.subgroupOf K))) ↦ m • b)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp) ∈
    orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
Tactic: rcases h with ⟨⟨gv, gp⟩, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp • b ∈
    orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
have gp₁ : gv ∈ H ∧ gv ∈ K
Tactic: simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp_1 • b ∈
    orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
have a : gv ∈ K
Tactic: refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
a : gv ∈ K
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ Subgroup.map K.subtype (H.subgroupOf K)) gv gp_1 • b ∈
    orbit.{u_1, u_2} (↥(H.subgroupOf K)) b
have a₁ : Subtype.mk (p := fun (x : G) ↦ x ∈ K) gv sorry ∈ H.subgroupOf K
Tactic: refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
H K : Subgroup G
b : α
gv : G
gp_1 : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ K) gv ⋯ ∈ H.subgroupOf K
have a : gv ∈ H
Tactic: simp only [Subgroup.mem_subgroupOf]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
⊢ IsPretransitive G α ↔ Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)
have refine_1 : IsPretransitive G α → ∀ (a b : orbitRel.Quotient G α), a = b
Tactic: refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
refine_1 : IsPretransitive G α → ∀ (a b : orbitRel.Quotient G α), a = b
⊢ IsPretransitive G α ↔ Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)
have refine_2 : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α) → ∀ (a b : α), ∃ (g : G), g • a = b
Tactic: refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b
have refine_1 : ∀ (x : α), Quot.mk (⇑(orbitRel G α) : α → α → Prop) x = b
Tactic: refine Quot.inductionOn a (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
h : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α)
a b : α
⊢ ∃ (g : G), g • a = b
have h : ⟦b⟧ = ⟦a⟧
Tactic: have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
inst_2 : Nonempty α
⊢ IsPretransitive G α ↔ Nonempty.{max 1 (u_2 + 1)} (Unique (orbitRel.Quotient G α))
have rw : Subsingleton.{u_2 + 1} (orbitRel.Quotient G α) → Nonempty.{u_2 + 1} (orbitRel.Quotient G α)
Tactic: rw [unique_iff_subsingleton_and_nonempty, pretransitive_iff_subsingleton_quotient, iff_self_and]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
x : orbitRel.Quotient G α
⊢ ∀ (x_1 y : (↑x.orbit : Type u_2)), ∃ (g : G), g • x_1 = y
have h : ∀ (a : α) (x y : (↑(orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) : Type u_2)), ∃ (g : G), g • x = y
Tactic: induction x using Quotient.inductionOn'
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a y : α
yh : y ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
z : α
zh : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
⊢ ∃ (g : G),
    g • Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) y yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh
have h : ∀ (yh_1 : (orbitRel G α : α → α → Prop) y a) (z : α)
  (zh : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) (zh_1 : (orbitRel G α : α → α → Prop) z a),
  ∃ (g : G),
    g • Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) y yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh
Tactic: rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh
Cleared hypotheses: z, zh
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MulAction G β
a y : α
yh_1 : y ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
yh : (orbitRel G α : α → α → Prop) y a
z : α
zh_1 : z ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)
zh : (orbitRel G α : α → α → Prop) z a
⊢ ∃ (g : G),
    g • Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) y yh_1 =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh_1
have h : ∀ (g : G) (yh : (fun (m : G) ↦ m • a) g ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)),
  ∃ (g_1 : G),
    g_1 •
        Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a))
          ((fun (m : G) ↦ m • a) g) yh =
      Subtype.mk (p := fun (x : α) ↦ x ∈ orbitRel.Quotient.orbit.{u_1, u_2} (G := G) (Quotient.mk'' a)) z zh_1
Tactic: rcases yh with ⟨g, rfl⟩
Cleared hypotheses: y, yh_1, yh