case refine'_1
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) ≤ c * a ⊓ c * b

case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) = c * a ⊓ c * b
refine' le_antisymm _ _
case refine'_1
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a ⊓ b ≤ a ∧ a ⊓ b ≤ b

case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
case refine'_1
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * (a ⊓ b) ≤ c * a ⊓ c * b

case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
rw [le_inf_iff, mul_le_mul_iff_left, mul_le_mul_iff_left]
case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
case refine'_1
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ a ⊓ b ≤ a ∧ a ⊓ b ≤ b

case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
simp
case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * a ∧ c * a ⊓ c * b ≤ c * b
case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * (a ⊓ b)
rw [← mul_le_mul_iff_left c⁻¹, ← mul_assoc, inv_mul_self, one_mul, le_inf_iff,
  inv_mul_le_iff_le_mul, inv_mul_le_iff_le_mul]
no goals
case refine'_2
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
⊢ c * a ⊓ c * b ≤ c * a ∧ c * a ⊓ c * b ≤ c * b
simp