Theorem: GenericProduction.eq_iff_lhs_and_rhs_eq (FormalSystems/Chomsky/Grammar.lean)

State before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ ↔ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Tactic:
constructor
State after:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs

case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂

State before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs

case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Tactic:
. intro h; rw [h]; exact ⟨ rfl, rfl ⟩
State after:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂

State before:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Tactic:
. intro ⟨ h₁, h₂ ⟩
  match p₁ with
  | ⟨ l, r, _ ⟩ => simp at h₁; simp at h₂; simp_rw [h₁, h₂]
State after:
no goals

State before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Tactic:
intro h
State after:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs

State before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
Tactic:
rw [h]
State after:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₂.lhs = p₂.lhs ∧ p₂.rhs = p₂.rhs

State before:
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₂.lhs = p₂.lhs ∧ p₂.rhs = p₂.rhs
Tactic:
exact ⟨ rfl, rfl ⟩
State after:
no goals

State before:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
Tactic:
intro ⟨ h₁, h₂ ⟩
State after:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h₁ : p₁.lhs = p₂.lhs
h₂ : p₁.rhs = p₂.rhs
⊢ p₁ = p₂

State before:
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h₁ : p₁.lhs = p₂.lhs
h₂ : p₁.rhs = p₂.rhs
⊢ p₁ = p₂
Tactic:
match p₁ with
| ⟨ l, r, _ ⟩ => simp at h₁; simp at h₂; simp_rw [h₁, h₂]
State after:
no goals

State before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.lhs = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Tactic:
simp at h₁
State after:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂

State before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Tactic:
simp at h₂
State after:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : r = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂

State before:
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : r = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
Tactic:
simp_rw [h₁, h₂]
State after:
no goals