-- Mathlib/GroupTheory/Transfer.lean
theorem ker_transferSylow_isComplement' : IsComplement' (transferSylow P hP).ker P

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
  (transferSylow_restrict_eq_pow P hP).symm ▸ (P.2.powEquiv' P.not_dvd_index).bijective

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Bijective ⇑((transferSylow P hP).restrict ↑P)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : (transferSylow P hP).ker ⊓ ↑P = ⊥ ∧ ↑(transferSylow P hP).ker * ↑↑P = Set.univ
this : Function.Surjective ⇑(transferSylow P hP)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).restrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
this : Function.Surjective ⇑(transferSylow P hP)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
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

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : (transferSylow P hP).ker ⊓ ↑P = ⊥ ∧ ↑(transferSylow P hP).ker * ↑↑P = Set.univ
this : Function.Surjective ⇑(transferSylow P hP)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).restrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
have := range_eq_top.mp (top_le_iff.mp (hf.2.ge.trans
  (map_le_range (transferSylow P hP) P)))

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).restrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
this : Function.Surjective ⇑(transferSylow P hP)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Bijective ⇑((transferSylow P hP).restrict ↑P)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
rw [Function.Bijective, ← range_eq_top, restrict_range] at hf

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : (↑P).normalizer ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Injective ⇑((transferSylow P hP).restrict ↑P) ∧ map (transferSylow P hP) ↑P = ⊤
⊢ (transferSylow P hP).ker.IsComplement' ↑P