-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.KleinFour (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
have :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
neg :
  ∀
    (univ₂ :
      Eq (α := Finset G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
          (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
        univ),
    (e : (a : G₁) → G₂) (x * y) =
      HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have₁ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
neg₁ neg₂ :
  ∀
    (univ₂ :
      Eq (α := Finset G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
          (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
        univ),
    (e : (a : G₁) → G₂) (x * y) =
      HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
neg₃ :
  ∀ (hx : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) 1 : G₂))
    (hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) ((e : (a : G₁) → G₂) 1 : G₂))
    (hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂))
    (univ₂ :
      Eq (α := Finset G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
          (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
        univ),
    (e : (a : G₁) → G₂) (x * y) =
      HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
⊢ (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
have neg₄ : ∀ (hx : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂))
  (hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂))
  (hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂))
  (univ₂ :
    Eq (α := Finset G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
        (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
      univ),
  (e : (a : G₁) → G₂) (x * y) = HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
Tactic: classical
      have univ₂ : {e (x * y), e x, e y, (1 : G₂)} = Finset.univ := by
        simpa [map_univ_equiv e, map_insert, he]
          using congr(Finset.map e.toEmbedding $(eq_finset_univ hx hy hxy))
      rw [← Ne, ← e.injective.ne_iff] at hx hy hxy
      rw [he] at hx hy
      symm
      apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _
      simpa using mul_notMem_of_exponent_two h hx hy hxy
Cleared hypotheses: hx, hy, hxy