Theorem: Subgroup.pairwiseDisjoint_smul (LeanCamCombi/Kneser/Mathlib.lean)

State before:
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
⊢ (range fun a => a • ↑s).PairwiseDisjoint id
Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ hab
State after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : (fun a => a • ↑s) a ≠ (fun a => a • ↑s) b
⊢ (Disjoint on id) ((fun a => a • ↑s) a) ((fun a => a • ↑s) b)

State before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : (fun a => a • ↑s) a ≠ (fun a => a • ↑s) b
⊢ (Disjoint on id) ((fun a => a • ↑s) a) ((fun a => a • ↑s) b)
Tactic:
simp only [Function.onFun, id_eq, disjoint_left] at hab ⊢
State after:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
⊢ ∀ ⦃a_1 : β⦄, a_1 ∈ a • ↑s → a_1 ∉ b • ↑s

State before:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
⊢ ∀ ⦃a_1 : β⦄, a_1 ∈ a • ↑s → a_1 ∉ b • ↑s
Tactic:
rintro _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False
Tactic:
refine' hab _
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MulAction α β
inst✝ : IsScalarTower α β β
s : Subgroup β
a b : α
hab : a • ↑s ≠ b • ↑s
c : β
hc : c ∈ ↑s
d : β
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ a • ↑s = b • ↑s
Tactic:
rw [← smul_coe hc, ← smul_assoc, ← hcd, smul_assoc, smul_coe hc, smul_coe hd]
State after:
no goals