G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Bijective ↑(restrict (transferSylow P hP) ↑P)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
  (transferSylow_restrict_eq_pow P hP).symm ▸
    (P.2.powEquiv'
        (not_dvd_index_sylow P
          (mt index_eq_zero_of_relindex_eq_zero index_ne_zero_of_finite))).bijective
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Bijective ↑(restrict (transferSylow P hP) ↑P)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
rw [Function.Bijective, ← range_top_iff_surjective, restrict_range] at hf
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
have := range_top_iff_surjective.mp (top_le_iff.mp (hf.2.ge.trans
  (map_le_range (transferSylow P hP) P)))
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf✝ : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ ker (transferSylow P hP) ⊔ ↑P = ⊤
hf : ker (transferSylow P hP) ⊓ ↑P = ⊥ ∧ ↑(ker (transferSylow P hP)) * ↑↑P = Set.univ
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff,
  normal_mul, ← ker_eq_bot_iff, ← (map_injective (P : Subgroup G).subtype_injective).eq_iff,
  ker_restrict, subgroupOf_map_subtype, Subgroup.map_bot, coe_top] at hf
no goals
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
A : Type ?u.1410107
inst✝³ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : FiniteIndex ↑P
hf✝ : Function.Injective ↑(restrict (transferSylow P hP) ↑P) ∧ ker (transferSylow P hP) ⊔ ↑P = ⊤
hf : ker (transferSylow P hP) ⊓ ↑P = ⊥ ∧ ↑(ker (transferSylow P hP)) * ↑↑P = Set.univ
this : Function.Surjective ↑(transferSylow P hP)
⊢ IsComplement' (ker (transferSylow P hP)) ↑P
exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2