Theorem: LO.FirstOrder.Structure.Monotone.term_monotone (Arithmetization/Vorspiel/Lemmata.lean)

State before:
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
t : Semiterm L ξ n
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
⊢ Semiterm.valm M e₁ ε₁ t ≤ Semiterm.valm M e₂ ε₂ t
Tactic:
induction t <;> simp [*, Semiterm.val_func]
State after:
case func
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.valm M e₁ ε₁ (a✝ a) ≤ Semiterm.valm M e₂ ε₂ (a✝ a)
⊢ (func a✝¹ fun i => Semiterm.val inst✝¹ e₁ ε₁ (a✝ i)) ≤ func a✝¹ fun i => Semiterm.val inst✝¹ e₂ ε₂ (a✝ i)

State before:
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
ih : ∀ (a : Fin k), Semiterm.valm M e₁ ε₁ (v a) ≤ Semiterm.valm M e₂ ε₂ (v a)
⊢ (func f fun i => Semiterm.val inst✝¹ e₁ ε₁ (v i)) ≤ func f fun i => Semiterm.val inst✝¹ e₂ ε₂ (v i)
Tactic:
case func k f v ih =>
  exact Monotone.monotone f _ _ ih
State after:
no goals

State before:
L : Language
M : Type u_1
inst✝² : LE M
inst✝¹ : Structure L M
inst✝ : Monotone L M
ξ : Type u_2
n : ℕ
e₁ e₂ : Fin n → M
ε₁ ε₂ : ξ → M
he : ∀ (i : Fin n), e₁ i ≤ e₂ i
hε : ∀ (i : ξ), ε₁ i ≤ ε₂ i
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ n
ih : ∀ (a : Fin k), Semiterm.valm M e₁ ε₁ (v a) ≤ Semiterm.valm M e₂ ε₂ (v a)
⊢ (func f fun i => Semiterm.val inst✝¹ e₁ ε₁ (v i)) ≤ func f fun i => Semiterm.val inst✝¹ e₂ ε₂ (v i)
Tactic:
exact Monotone.monotone f _ _ ih
State after:
no goals