G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : { x // x ∈ H₁ } × { x // x ∈ H₂ }
hxy : (fun g => ↑g.fst * ↑g.snd) x = (fun g => ↑g.fst * ↑g.snd) y
⊢ x = y
G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
⊢ Injective fun g => ↑g.fst * ↑g.snd
intro x y hxy
G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : { x // x ∈ H₁ } × { x // x ∈ H₂ }
hxy✝ : (↑y.fst)⁻¹ * ↑x.fst * ↑x.snd = ↑y.snd
hxy : (↑y.fst)⁻¹ * ↑x.fst * (↑x.snd * (↑y.snd)⁻¹) = 1
⊢ x = y
G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : { x // x ∈ H₁ } × { x // x ∈ H₂ }
hxy : (fun g => ↑g.fst * ↑g.snd) x = (fun g => ↑g.fst * ↑g.snd) y
⊢ x = y
rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : { x // x ∈ H₁ } × { x // x ∈ H₂ }
hxy✝ : (↑y.fst)⁻¹ * ↑x.fst * ↑x.snd = ↑y.snd
hxy : ↑(y.fst⁻¹ * x.fst) = 1 ∧ ↑(x.snd * y.snd⁻¹) = 1
⊢ x = y
G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : { x // x ∈ H₁ } × { x // x ∈ H₂ }
hxy✝ : (↑y.fst)⁻¹ * ↑x.fst * ↑x.snd = ↑y.snd
hxy : (↑y.fst)⁻¹ * ↑x.fst * (↑x.snd * (↑y.snd)⁻¹) = 1
⊢ x = y
replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
no goals
G : Type u_1
G' : Type ?u.729648
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.729657
inst✝¹ : AddGroup A
N : Type ?u.729663
inst✝ : Group N
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : { x // x ∈ H₁ } × { x // x ∈ H₂ }
hxy✝ : (↑y.fst)⁻¹ * ↑x.fst * ↑x.snd = ↑y.snd
hxy : ↑(y.fst⁻¹ * x.fst) = 1 ∧ ↑(x.snd * y.snd⁻¹) = 1
⊢ x = y
rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ←
  Subtype.ext_iff, eq_comm, ← Prod.ext_iff] at hxy