-- Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic
Goal:
ι : Type u_1
M : Type u_4
s : Finset ι
inst : CommMonoid M
f : ι → M
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
H H₁ :
  ∀ (s : Finset ι)
    (ih :
      ∀ t ⊂ s,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s)
    (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
H₂ :
  ∀
    (ih :
      ∀ t ⊂ ∅,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → Membership.mem (γ := Finset ι) ∅ a → ι)
    (hg₁ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), f a ≠ 1 → g a ha ≠ a)
    (g_mem : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), Membership.mem (γ := Finset ι) ∅ (g a ha))
    (hg₄ : ∀ (a : ι) (ha : Membership.mem (γ := Finset ι) ∅ a), g (g a ha) ⋯ = a),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ ∅, f x) 1
H₃ H₄ :
  ∀ (s : Finset ι)
    (ih :
      ∀ t ⊂ s,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s)
    (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) (x : ι) (hx : x ∈ s), Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
H₅ :
  ∀ (s : Finset ι)
    (ih :
      ∀ t ⊂ s,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s)
    (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) (x : ι) (hx : x ∈ s) (this : {x, g x hx} ⊆ s),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1
H₆ :
  ∀ (s : Finset ι)
    (ih :
      ∀ t ⊂ s,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s)
    (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) (x : ι) (hx : x ∈ s) (this : {x, g x hx} ⊆ s),
    Eq.{u_4 + 1} (α := M) (∏ x ∈ s \ {x, g x hx}, f x) 1
H₇ :
  ∀ (s : Finset ι)
    (ih :
      ∀ t ⊂ s,
        ∀ (g : (a : ι) → a ∈ t → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1)
          (hg₃ : ∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t)
          (hg₄ : ∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a), Eq.{u_4 + 1} (α := M) (∏ x ∈ t, f x) 1)
    (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1)
    (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s)
    (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) (x : ι) (hx : x ∈ s) (this : {x, g x hx} ⊆ s) (a : ι)
    (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ Eq.{u_4 + 1} (α := M) (∏ x ∈ s, f x) 1

Tactic:
classical
  induction s using Finset.strongInduction with | H s ih => ?_
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · simp
  have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]
  suffices h : ∏ x ∈ s \ {x, g x hx}, f x = 1 by
    rw [← prod_sdiff this, h, one_mul]
    cases eq_or_ne (g x hx) x with
    | inl hx' => simpa [hx'] using hg₃ x hx
    | inr hx' => grind
  suffices h₃ : ∀ a (ha : a ∈ s \ {x, g x hx}), g a (sdiff_subset ha) ∈ s \ {x, g x hx} from
    ih (s \ {x, g x hx}) (ssubset_iff.2 ⟨x, by simp [insert_subset_iff, hx]⟩) _
      (by simp [hg₁]) (fun _ _ => hg₃ _ _) h₃ (fun _ _ => hg₄ _ _)
  grind

Premises used: Finset.strongInduction, rfl, Finset.eq_empty_or_nonempty