α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a✝ b : α
f : α → β
a : α
⊢ ↑(Language.map f) (matches' (char a)) = matches' (map f (char a))
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a✝ b : α
f : α → β
a : α
⊢ matches' (map f (char a)) = ↑(Language.map f) (matches' (char a))
rw [eq_comm]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a✝ b : α
f : α → β
a : α
⊢ ↑(Language.map f) (matches' (char a)) = matches' (map f (char a))
exact image_singleton
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ ↑(Language.map f) (matches' R) + ↑(Language.map f) (matches' S) = ↑(Language.map f) (matches' R + matches' S)
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ matches' (map f (R + S)) = ↑(Language.map f) (matches' (R + S))
simp only [matches'_map, map, matches'_add]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ ↑(Language.map f) (matches' R) + ↑(Language.map f) (matches' S) = ↑(Language.map f) (matches' R + matches' S)
rw [map_add]
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ ↑(Language.map f) (matches' R) * ↑(Language.map f) (matches' S) = ↑(Language.map f) (matches' R * matches' S)
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ matches' (map f (R * S)) = ↑(Language.map f) (matches' (R * S))
simp only [matches'_map, map, matches'_mul]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R S : RegularExpression α
⊢ ↑(Language.map f) (matches' R) * ↑(Language.map f) (matches' S) = ↑(Language.map f) (matches' R * matches' S)
rw [map_mul]
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (↑(Language.map f) (matches' R))∗ = ↑(Language.map f) (matches' R)∗
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ matches' (map f (star R)) = ↑(Language.map f) (matches' (star R))
simp_rw [map, matches', matches'_map]
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (⨆ (i : ℕ), ↑(Language.map f) (matches' R) ^ i) = ↑(Language.map f) (⨆ (i : ℕ), matches' R ^ i)
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (↑(Language.map f) (matches' R))∗ = ↑(Language.map f) (matches' R)∗
rw [Language.kstar_eq_iSup_pow, Language.kstar_eq_iSup_pow]
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (⨆ (i : ℕ), ↑(Language.map f) (matches' R ^ i)) = ↑(Language.map f) (⨆ (i : ℕ), matches' R ^ i)
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (⨆ (i : ℕ), ↑(Language.map f) (matches' R) ^ i) = ↑(Language.map f) (⨆ (i : ℕ), matches' R ^ i)
simp_rw [← map_pow]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.138072
dec : DecidableEq α
a b : α
f : α → β
R : RegularExpression α
⊢ (⨆ (i : ℕ), ↑(Language.map f) (matches' R ^ i)) = ↑(Language.map f) (⨆ (i : ℕ), matches' R ^ i)
exact image_iUnion.symm