-- Mathlib/GroupTheory/Perm/Finite.lean
lemma support_closure_subset_union (S : Set (Perm α)) :
    ∀ a ∈ closure S, (a.support : Set α) ⊆ ⋃ b ∈ S, b.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ a ∈ closure S, ↑a.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
apply closure_induction

Result:
case mem
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support

case one
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ↑(support 1) ⊆ ⋃ b ∈ S, ↑b.support

case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Proof state:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
intro a b ha hb hc hd

Result:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support

Proof state:
case mem
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
exact fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl

Result:
no goals

Proof state:
case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
simp only [support_inv, imp_self, implies_true]

Result:
no goals

Proof state:
case one
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ↑(support 1) ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
simp only [support_one, Finset.coe_empty, Set.empty_subset]

Result:
no goals

Proof state:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support ∧ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
exact ⟨hc, hd⟩

Result:
no goals

Proof state:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a.support ⊔ b.support) ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]

Result:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support ∧ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support

Proof state:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a * b).support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_

Result:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a.support ⊔ b.support) ⊆ ⋃ b ∈ S, ↑b.support