-- Mathlib/GroupTheory/Perm/Finite.lean
lemma disjoint_support_closure_of_disjoint_support {S T : Set (Perm α)}
    (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) :
    ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
⊢ _root_.Disjoint a.support b.support

Tactic:
have key1 := support_closure_subset_union S a ha

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ _root_.Disjoint a.support b.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
have key := Set.disjoint_of_subset key1 key2

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : _root_.Disjoint (⋃ b ∈ S, ↑b.support) (⋃ b ∈ T, ↑b.support) → _root_.Disjoint ↑a.support ↑b.support
⊢ _root_.Disjoint a.support b.support

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

Tactic:
have key2 := support_closure_subset_union T b hb

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
⊢ _root_.Disjoint a.support b.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : (∀ i ∈ S, ∀ i_2 ∈ T, _root_.Disjoint i.support i_2.support) → _root_.Disjoint a.support b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
exact key h

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Tactic:
intro a ha b hb

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
⊢ _root_.Disjoint a.support b.support

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : _root_.Disjoint (⋃ b ∈ S, ↑b.support) (⋃ b ∈ T, ↑b.support) → _root_.Disjoint ↑a.support ↑b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
simp_rw [Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.disjoint_coe] at key

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : a ∈ closure S
b : Perm α
hb : b ∈ closure T
key1 : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
key2 : ↑b.support ⊆ ⋃ b ∈ T, ↑b.support
key : (∀ i ∈ S, ∀ i_2 ∈ T, _root_.Disjoint i.support i_2.support) → _root_.Disjoint a.support b.support
⊢ _root_.Disjoint a.support b.support