Theorem: Metamath.Statement.trim_le (Metamath/Translate.lean)

State before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : (trim s₁).ctx ≤ s₂.ctx
h₁ : ∀ (a : Formula), a ∈ (trim s₁).ctx.hyps → a ∈ s₂.ctx.hyps
h₂ : (trim s₁).ctx.dj ≤ s₂.ctx.dj
⊢ (DJ.trim s₁.ctx.dj fun x => (fun v => v ∈ vars s₂) x) ≤ s₂.ctx.dj
Tactic:
rw [← e]
State after:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : (trim s₁).ctx ≤ s₂.ctx
h₁ : ∀ (a : Formula), a ∈ (trim s₁).ctx.hyps → a ∈ s₂.ctx.hyps
h₂ : (trim s₁).ctx.dj ≤ s₂.ctx.dj
⊢ (DJ.trim s₁.ctx.dj fun x => (fun v => v ∈ vars s₁) x) ≤ s₂.ctx.dj

State before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : (trim s₁).ctx ≤ s₂.ctx
h₁ : ∀ (a : Formula), a ∈ (trim s₁).ctx.hyps → a ∈ s₂.ctx.hyps
h₂ : (trim s₁).ctx.dj ≤ s₂.ctx.dj
⊢ (DJ.trim s₁.ctx.dj fun x => (fun v => v ∈ vars s₁) x) ≤ s₂.ctx.dj
Tactic:
exact h₂
State after:
no goals

State before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₁) x
Tactic:
rw [e]
State after:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₂) x

State before:
s₁ s₂ : Statement
e : vars s₁ = vars s₂
x✝ : s₁.ctx ≤ (untrim s₂).ctx
h₁ : ∀ (a : Formula), a ∈ s₁.ctx.hyps → a ∈ (untrim s₂).ctx.hyps
h₂ : s₁.ctx.dj ≤ (untrim s₂).ctx.dj
⊢ s₁.ctx.dj ≤ DJ.untrim s₂.ctx.dj fun x => (fun v => v ∈ vars s₂) x
Tactic:
exact h₂
State after:
no goals