Theorem: LO.FirstOrder.Rew.map_inj (Logic/FirstOrder/Basic/Syntax/Rew.lean)

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x : Fin n₁
t : Semiterm L ξ₁ n₁
⊢ (map b e) #x = (map b e) t → #x = t
Tactic:
cases t <;> simp[Rew.func]
State after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
⊢ b x = b a✝ → x = a✝

State before:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
⊢ b x = b a✝ → x = a✝
Tactic:
intro h
State after:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
h : b x = b a✝
⊢ x = a✝

State before:
case bvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : Fin n₁
h : b x = b a✝
⊢ x = a✝
Tactic:
exact hb h
State after:
no goals

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x : ξ₁
t : Semiterm L ξ₁ n₁
⊢ (map b e) &x = (map b e) t → &x = t
Tactic:
cases t <;> simp[Rew.func]
State after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
⊢ e x = e a✝ → x = a✝

State before:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
⊢ e x = e a✝ → x = a✝
Tactic:
intro h
State after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
h : e x = e a✝
⊢ x = a✝

State before:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
x a✝ : ξ₁
h : e x = e a✝
⊢ x = a✝
Tactic:
exact he h
State after:
no goals

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
t : Semiterm L ξ₁ n₁
⊢ (map b e) (func f v) = (map b e) t → func f v = t
Tactic:
cases t <;> simp[*, Rew.func]
State after:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
⊢ k = arity✝ →
    HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = arity✝ ∧ HEq f a✝¹ ∧ HEq v a✝

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
⊢ k = arity✝ →
    HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = arity✝ ∧ HEq f a✝¹ ∧ HEq v a✝
Tactic:
case func =>
  rintro rfl; simp; rintro rfl h; simp
  funext i; exact map_inj hb he (congr_fun h i)
State after:
no goals

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
⊢ k = arity✝ →
    HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = arity✝ ∧ HEq f a✝¹ ∧ HEq v a✝
Tactic:
rintro rfl
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = k ∧ HEq f a✝¹ ∧ HEq v a✝

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ HEq f a✝¹ → (HEq (fun i => (map b e) (v i)) fun i => (map b e) (a✝ i)) → k = k ∧ HEq f a✝¹ ∧ HEq v a✝
Tactic:
simp
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ f = a✝¹ → ((fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)) → f = a✝¹ ∧ v = a✝

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
a✝¹ : L.Func k
a✝ : Fin k → Semiterm L ξ₁ n₁
⊢ f = a✝¹ → ((fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)) → f = a✝¹ ∧ v = a✝
Tactic:
rintro rfl h
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ f = f ∧ v = a✝

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ f = f ∧ v = a✝
Tactic:
simp
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ v = a✝

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
⊢ v = a✝
Tactic:
funext i
State after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
i : Fin k
⊢ v i = a✝ i

State before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
b✝ : Fin n₁ → Fin n₂
e✝ : ξ₁ → ξ₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
hb : Function.Injective b
he : Function.Injective e
k : ℕ
f : L.Func k
v a✝ : Fin k → Semiterm L ξ₁ n₁
h : (fun i => (map b e) (v i)) = fun i => (map b e) (a✝ i)
i : Fin k
⊢ v i = a✝ i
Tactic:
exact map_inj hb he (congr_fun h i)
State after:
no goals