α : Type u_1
β : Type ?u.90470
γ : Type ?u.90473
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : x ∈ l₁ * l₂
⊢ x ∈ m₁ * m₂
α : Type u_1
β : Type ?u.90470
γ : Type ?u.90473
l m : Language α
a b x : List α
l₁ l₂ m₁ m₂ : Language α
⊢ l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂
intro h₁ h₂ x hx
α : Type u_1
β : Type ?u.90470
γ : Type ?u.90473
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : ∃ a, a ∈ l₁ ∧ ∃ x_1, x_1 ∈ l₂ ∧ a ++ x_1 = x
⊢ ∃ a, a ∈ m₁ ∧ ∃ x_1, x_1 ∈ m₂ ∧ a ++ x_1 = x
α : Type u_1
β : Type ?u.90470
γ : Type ?u.90473
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : x ∈ l₁ * l₂
⊢ x ∈ m₁ * m₂
simp only [mul_def, exists_and_left, mem_image2, image_prod] at hx⊢
no goals
α : Type u_1
β : Type ?u.90470
γ : Type ?u.90473
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : ∃ a, a ∈ l₁ ∧ ∃ x_1, x_1 ∈ l₂ ∧ a ++ x_1 = x
⊢ ∃ a, a ∈ m₁ ∧ ∃ x_1, x_1 ∈ m₂ ∧ a ++ x_1 = x
tauto