case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L

case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
by_cases h : H.relindex L = 0
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex H (K ⊓ L) * relindex K L ≤ relindex H L * relindex K L
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
rw [← inf_relindex_right, inf_assoc, ← relindex_mul_relindex _ _ L inf_le_right inf_le_right,
  inf_relindex_right, inf_relindex_right]
no goals
case neg
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : ¬relindex H L = 0
⊢ relindex H (K ⊓ L) * relindex K L ≤ relindex H L * relindex K L
exact mul_le_mul_right' (relindex_le_of_le_right inf_le_right h) (K.relindex L)
no goals
case pos
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
h : relindex H L = 0
⊢ relindex (H ⊓ K) L ≤ relindex H L * relindex K L
exact (le_of_eq (relindex_eq_zero_of_le_left inf_le_left h)).trans (zero_le _)