case h.h
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ m₁ = m₂
funext a b
no goals
case h.h
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b
calc
  m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by
    { simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] }
  _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]
no goals
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b
simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]