no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a ⊓ b = a * 1 ⊓ a * (b / a)
rw [mul_one a, div_eq_mul_inv, mul_comm b, mul_inv_cancel_left]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * 1 ⊓ a * (b / a) = a * (1 ⊓ b / a)
rw [← mul_inf 1 (b / a) a]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (1 ⊓ b / a) = a * (b / a ⊓ 1)
rw [inf_comm]
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 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 : α
⊢ a * (b / a ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
rw [div_eq_mul_inv]
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b⁻¹⁻¹ * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 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 : α
⊢ a * (b * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
nth_rw 1 [← inv_inv b]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * (b⁻¹⁻¹ * a⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1)
rw [← mul_inv, mul_comm b⁻¹, ← div_eq_mul_inv]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * ((a / b)⁻¹ ⊓ 1) = a * ((a / b)⁻¹ ⊓ 1⁻¹)
rw [inv_one]
no goals
α : Type u
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a * ((a / b)⁻¹ ⊓ 1⁻¹) = a / (a / b ⊔ 1)
rw [← inv_sup_eq_inv_inf_inv, ← div_eq_mul_inv]