case refine'_1
A B : GroupCat
f : A ⟶ B
b : ↑B
⊢ b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier → b ∈ {x | ↑h x = ↑g x}

case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ False
A B : GroupCat
f : A ⟶ B
⊢ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier = {x | ↑h x = ↑g x}
refine' Set.ext fun b => ⟨_, fun hb : h b = g b => by_contradiction fun r => _⟩
case refine'_1.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ {x | ↑h x = ↑g x}
case refine'_1
A B : GroupCat
f : A ⟶ B
b : ↑B
⊢ b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier → b ∈ {x | ↑h x = ↑g x}
rintro ⟨a, rfl⟩
case refine'_1.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑h (↑f a) = ↑g (↑f a)
case refine'_1.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑f a ∈ {x | ↑h x = ↑g x}
change h (f a) = g (f a)
case refine'_1.intro.H.fromCoset.mk.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    ↑(↑g (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) })

case refine'_1.intro.H.infinity
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑(↑h (↑f a)) ∞ = ↑(↑g (↑f a)) ∞
case refine'_1.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑h (↑f a) = ↑g (↑f a)
ext ⟨⟨_, ⟨y, rfl⟩⟩⟩
case refine'_1.intro.H.fromCoset.mk.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
case refine'_1.intro.H.fromCoset.mk.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    ↑(↑g (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) })
rw [g_apply_fromCoset]
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }

case neg
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : ¬y ∈ MonoidHom.range f
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
case refine'_1.intro.H.fromCoset.mk.intro
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
by_cases m : y ∈ f.range
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      { val := ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier),
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
change fromCoset _ = fromCoset ⟨f a *l (y *l _), _⟩
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y_1,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      { val := ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier),
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      { val := ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier),
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
simp only [← fromCoset_eq_of_mem_range _ (Subgroup.mul_mem _ ⟨a, rfl⟩ m)]
case pos.e_a.e_val
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier =
    ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
case pos
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ fromCoset
      { val := ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y_1,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      { val := ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier),
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
congr
no goals
case pos.e_a.e_val
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ MonoidHom.range f
⊢ ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier =
    ↑f a *l (y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)
rw [leftCoset_assoc _ (f a) y]
case neg
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : ¬y ∈ MonoidHom.range f
⊢ fromCoset
      { val := ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y_1,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
case neg
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : ¬y ∈ MonoidHom.range f
⊢ ↑(↑h (↑f a))
      (fromCoset
        { val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
          property :=
            (_ :
              ∃ y_1,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                  Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) }) =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
rw [h_apply_fromCoset_nin_range f (f a) ⟨_, rfl⟩ _ m]
no goals
case neg
A B : GroupCat
f : A ⟶ B
a : ↑A
y : ↑B
m : ¬y ∈ MonoidHom.range f
⊢ fromCoset
      { val := ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y_1,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                ↑f a * y *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      {
        val :=
          ↑f a *l
            ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                property :=
                  (_ :
                    ∃ y_1,
                      Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) },
        property :=
          (_ :
            ↑f a *l
                ↑{ val := Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y,
                    property :=
                      (_ :
                        ∃ y_1,
                          Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y_1 =
                            Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y) } ∈
              Set.range (Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier)) }
simp only [leftCoset_assoc]
no goals
case refine'_1.intro.H.infinity
A B : GroupCat
f : A ⟶ B
a : ↑A
⊢ ↑(↑h (↑f a)) ∞ = ↑(↑g (↑f a)) ∞
rw [g_apply_infinity, h_apply_infinity f (f a) ⟨_, rfl⟩]
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
⊢ False
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ False
have eq1 : (h b) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) =
    fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩ := by
  change ((τ).symm.trans (g b)).trans τ _ = _
  dsimp [tau]
  simp [g_apply_infinity f]
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
eq2 :
  ↑(↑g b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
⊢ False
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
⊢ False
have eq2 :
  (g b) (fromCoset ⟨f.range.carrier, ⟨1, one_leftCoset _⟩⟩) =
    fromCoset ⟨b *l f.range.carrier, ⟨b, rfl⟩⟩ := rfl
no goals
case refine'_2
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
eq2 :
  ↑(↑g b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
⊢ False
exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, FunLike.congr_fun hb])
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑((τ.symm.trans (↑g b)).trans τ)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑(↑h b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
change ((τ).symm.trans (g b)).trans τ _ = _
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑(Equiv.swap
          (fromCoset
            { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
              property :=
                (_ :
                  ∃ y,
                    Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                      (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) })
          ∞)
      (↑(↑g b)
        (↑(Equiv.swap
              (fromCoset
                { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
                  property :=
                    (_ :
                      ∃ y,
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                          (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) })
              ∞)
          (fromCoset
            { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
              property :=
                (_ :
                  ∃ y,
                    Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                      (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }))) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑((τ.symm.trans (↑g b)).trans τ)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
dsimp [tau]
no goals
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
⊢ ↑(Equiv.swap
          (fromCoset
            { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
              property :=
                (_ :
                  ∃ y,
                    Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                      (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) })
          ∞)
      (↑(↑g b)
        (↑(Equiv.swap
              (fromCoset
                { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
                  property :=
                    (_ :
                      ∃ y,
                        Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                          (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) })
              ∞)
          (fromCoset
            { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
              property :=
                (_ :
                  ∃ y,
                    Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                      (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }))) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
simp [g_apply_infinity f]
no goals
A B : GroupCat
f : A ⟶ B
b : ↑B
hb : ↑h b = ↑g b
r : ¬b ∈ (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier
eq1 :
  ↑(↑h b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
eq2 :
  ↑(↑g b)
      (fromCoset
        { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
          property :=
            (_ :
              ∃ y,
                Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                  (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) =
    fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
⊢ fromCoset
      { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } =
    fromCoset
      { val := b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier,
        property :=
          (_ :
            ∃ y,
              Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y =
                b *l (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
rw [← eq1, ← eq2, FunLike.congr_fun hb]