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

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁶ x✝⁵ : ℕ
ξ✝ : Type u_5
x✝⁴ : Type u_6
x✝³ : Fin x✝⁶ → Fin x✝⁵
x✝² : ξ✝ → x✝⁴
x✝¹ : Function.Injective x✝³
x✝ : Function.Injective x✝²
p : Semiformula L ξ✝ x✝⁶
⊢ (map x✝³ x✝²).hom ⊤ = (map x✝³ x✝²).hom p → ⊤ = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁶ x✝⁵ : ℕ
ξ✝ : Type u_5
x✝⁴ : Type u_6
x✝³ : Fin x✝⁶ → Fin x✝⁵
x✝² : ξ✝ → x✝⁴
x✝¹ : Function.Injective x✝³
x✝ : Function.Injective x✝²
p : Semiformula L ξ✝ x✝⁶
⊢ (map x✝³ x✝²).hom ⊥ = (map x✝³ x✝²).hom p → ⊥ = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
p : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (rel r v) = (map x✝¹ x✝).hom p → rel r v = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
State after:
case hrel
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
case hrel =>
  rintro rfl; simp; rintro rfl h; simp
  funext i; exact map_inj hb hf (congr_fun h i)
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
rintro rfl
State after:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = arity✝ ∧ HEq r r✝ ∧ HEq v v✝

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = arity✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
simp
State after:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ r = r✝ → ((fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)) → r = r✝ ∧ v = v✝

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
r✝ : L.Rel arity✝
v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
⊢ r = r✝ → ((fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)) → r = r✝ ∧ v = v✝
Tactic:
rintro rfl h
State after:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ r = r ∧ v = v✝

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ r = r ∧ v = v✝
Tactic:
simp
State after:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ v = v✝

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
⊢ v = v✝
Tactic:
funext i
State after:
case h
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
i : Fin arity✝
⊢ v i = v✝ i

State before:
case h
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v v✝ : Fin arity✝ → Semiterm L ξ✝ x✝⁴
h : (fun i => (map x✝¹ x✝) (v i)) = fun i => (map x✝¹ x✝) (v✝ i)
i : Fin arity✝
⊢ v i = v✝ i
Tactic:
exact map_inj hb hf (congr_fun h i)
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
p : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (nrel r v) = (map x✝¹ x✝).hom p → nrel r v = p
Tactic:
cases p using cases' <;> simp[Rew.rel, Rew.nrel]
State after:
case hnrel
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝
Tactic:
case hnrel =>
  rintro rfl; simp; rintro rfl h; simp
  funext i; exact map_inj hb hf (congr_fun h i)
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q r : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (p ⋏ q) = (map x✝¹ x✝).hom r → p ⋏ q = r
Tactic:
cases r using cases' <;> simp[Rew.rel, Rew.nrel]
State after:
case hand
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝

State before:
case hand
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝
Tactic:
intro hp hq
State after:
case hand
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝

State before:
case hand
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝
Tactic:
exact ⟨mapl_inj hb hf hp, mapl_inj hb hf hq⟩
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q r : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (p ⋎ q) = (map x✝¹ x✝).hom r → p ⋎ q = r
Tactic:
cases r using cases' <;> simp[Rew.rel, Rew.nrel]
State after:
case hor
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝

State before:
case hor
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝
Tactic:
intro hp hq
State after:
case hor
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝

State before:
case hor
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
hp : (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝
hq : (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝
⊢ p = p✝ ∧ q = q✝
Tactic:
exact ⟨mapl_inj hb hf hp, mapl_inj hb hf hq⟩
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p : Semiformula L ξ✝ (x✝² + 1)
q : Semiformula L ξ✝ x✝²
⊢ (map b e).hom (∀' p) = (map b e).hom q → ∀' p = q
Tactic:
cases q using cases' <;> simp[Rew.rel, Rew.nrel, q_map]
State after:
case hall
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝

State before:
case hall
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝
Tactic:
intro h
State after:
case hall
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝

State before:
case hall
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
Tactic:
exact mapl_inj (b := 0 :> Fin.succ ∘ b)
(Matrix.injective_vecCons ((Fin.succ_injective _).comp hb) (fun _ => (Fin.succ_ne_zero _).symm)) hf h
State after:
no goals

State before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p : Semiformula L ξ✝ (x✝² + 1)
q : Semiformula L ξ✝ x✝²
⊢ (map b e).hom (∃' p) = (map b e).hom q → ∃' p = q
Tactic:
cases q using cases' <;> simp[Rew.rel, Rew.nrel, q_map]
State after:
case hex
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝

State before:
case hex
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
⊢ (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝ → p = p✝
Tactic:
intro h
State after:
case hex
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝

State before:
case hex
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ x✝² x✝¹ : ℕ
ξ✝ : Type u_5
x✝ : Type u_6
b : Fin x✝² → Fin x✝¹
e : ξ✝ → x✝
hb : Function.Injective b
hf : Function.Injective e
p p✝ : Semiformula L ξ✝ (x✝² + 1)
h : (map (0 :> Fin.succ ∘ b) e).hom p = (map (0 :> Fin.succ ∘ b) e).hom p✝
⊢ p = p✝
Tactic:
exact mapl_inj (b := 0 :> Fin.succ ∘ b)
(Matrix.injective_vecCons ((Fin.succ_injective _).comp hb) (fun _ => (Fin.succ_ne_zero _).symm)) hf h
State after:
no goals