Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ (Set.range fun a => a • s.mulStab).PairwiseDisjoint id
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (Set.range fun a => a • ∅.mulStab).PairwiseDisjoint id

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ (Set.range fun a => a • s.mulStab).PairwiseDisjoint id

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ (Set.range fun a => a • s.mulStab).PairwiseDisjoint id
Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩
State after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ (fun a => a • s.mulStab) a ≠ (fun a => a • s.mulStab) b →
    (Disjoint on id) ((fun a => a • s.mulStab) a) ((fun a => a • s.mulStab) b)

State before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ (fun a => a • s.mulStab) a ≠ (fun a => a • s.mulStab) b →
    (Disjoint on id) ((fun a => a • s.mulStab) a) ((fun a => a • s.mulStab) b)
Tactic:
simp only [onFun, id_eq]
State after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • s.mulStab ≠ b • s.mulStab → Disjoint (a • s.mulStab) (b • s.mulStab)

State before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • s.mulStab ≠ b • s.mulStab → Disjoint (a • s.mulStab) (b • s.mulStab)
Tactic:
simp_rw [← disjoint_coe, ← coe_injective.ne_iff, coe_smul_finset, coe_mulStab hs]
State after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • ↑(stabilizer α s) ≠ b • ↑(stabilizer α s) → Disjoint (a • ↑(stabilizer α s)) (b • ↑(stabilizer α s))

State before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • ↑(stabilizer α s) ≠ b • ↑(stabilizer α s) → Disjoint (a • ↑(stabilizer α s)) (b • ↑(stabilizer α s))
Tactic:
exact Subgroup.pairwiseDisjoint_smul _ (Set.mem_range_self _) (Set.mem_range_self _)
State after:
no goals

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (Set.range fun a => a • ∅.mulStab).PairwiseDisjoint id
Tactic:
simp
State after:
no goals