awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₁.listEncode ++ l') = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 f₁ :: listDecode l'
ih2 :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f₂.listEncode ++ l') = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 f₂ :: listDecode l'
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (if h : 2 ≤ (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l))).length then
      sigmaImp
          (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
            (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l))) 0 ⋯)
          (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
            (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l))) 1 h) ::
        drop 2 (listDecode (f₁.listEncode ++ (f₂.listEncode ++ l)))
    else []) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (f₁ ⟹ f₂) :: listDecode l

Tactic:
simp only [ih1, ih2, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, getElem_cons_succ, sigmaImp_apply, drop_succ_cons, drop_zero]

Premises used: zero_le, List.length_cons, List.drop_zero, reduceDIte, FirstOrder.Language.BoundedFormula.sigmaImp_apply, List.getElem_cons_zero, List.drop_succ_cons, List.getElem_cons_succ, le_add_iff_nonneg_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode
        ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n_1 + 1) f).snd (β := fun (n : ℕ) ↦
              L.BoundedFormula α n).listEncode ++
          l') =
      Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n_1 + 1) f :: listDecode l'
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
all :
  listDecode ((∀' f).listEncode ++ l) = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l
⊢ listDecode
      ((Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f)).snd (β := fun (n : ℕ) ↦
            L.BoundedFormula α n).listEncode ++
        l) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l

Tactic:
simp only [] at *
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f.listEncode ++ l') = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n_1 + 1) f :: listDecode l'
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
all :
  (if h : 1 ≤ (listDecode (f.listEncode ++ l)).length then
      sigmaAll
          (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
            (listDecode (f.listEncode ++ l)) 0 h) ::
        drop 1 (listDecode (f.listEncode ++ l))
    else []) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l
⊢ listDecode ((∀' f).listEncode ++ l) = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l

Tactic:
rw [listEncode, cons_append, listDecode]

Premises used: FirstOrder.Language.BoundedFormula.listDecode, FirstOrder.Language.BoundedFormula.listEncode, List.cons_append
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
l_1 : List ((n : ℕ) × L.BoundedFormula α n)
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih :
  ∀ (l' : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
    listDecode (f.listEncode ++ l') = Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) (n_1 + 1) f :: listDecode l'
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
⊢ (if h : 1 ≤ (listDecode (f.listEncode ++ l)).length then
      sigmaAll
          (getElem (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
            (listDecode (f.listEncode ++ l)) 0 h) ::
        drop 1 (listDecode (f.listEncode ++ l))
    else []) =
    Sigma.mk (β := fun (n : ℕ) ↦ L.BoundedFormula α n) n_1 (∀' f) :: listDecode l

Tactic:
simp only [ih, length_cons, le_add_iff_nonneg_left, _root_.zero_le, ↓reduceDIte,
      getElem_cons_zero, sigmaAll_apply, drop_succ_cons, drop_zero]

Premises used: zero_le, List.length_cons, List.drop_zero, reduceDIte, List.getElem_cons_zero, List.drop_succ_cons, FirstOrder.Language.BoundedFormula.sigmaAll_apply, le_add_iff_nonneg_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
⊢ listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        [φ]) =
    [φ]

Tactic:
have h := listDecode_encode_list [φ]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h :
  listDecode
      (flatMap (fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode)
        [φ]) =
    [φ]
⊢ listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode = [φ]

Tactic:
rw [flatMap_singleton] at h

Premises used: List.flatMap_singleton
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h : listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode = [φ]
rw : getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length) [φ] 0 = some φ
⊢ getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length)
      (listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode) 0 =
    some φ

Tactic:
rw [h]
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
φ : (n : ℕ) × L.BoundedFormula α n
h : listDecode φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode = [φ]
⊢ getElem? (valid := fun (as : List ((n : ℕ) × L.BoundedFormula α n)) (i : ℕ) ↦ i < as.length) [φ] 0 = some φ

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ Function.Injective (β := List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
    fun (φ : (n : ℕ) × L.BoundedFormula α n) ↦ φ.snd (β := fun (n : ℕ) ↦ L.BoundedFormula α n).listEncode

Tactic:
BoundedFormula.encoding.encode_injective

Premises used: Computability.Encoding.encode_injective, FirstOrder.Language.BoundedFormula.encoding
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ #((n : ℕ) × L.BoundedFormula α n) ≤ max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans ?_)

Premises used: Computability.Encoding.card_le_card_list, Iff.mp, LE.le.trans, FirstOrder.Language.BoundedFormula.encoding, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine :
  lift.{max (max u' v) u, max (max u' v) u}
      #(List (Encoding.Γ (α := (n : ℕ) × L.BoundedFormula α n) BoundedFormula.encoding)) ≤
    lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
⊢ #((n : ℕ) × L.BoundedFormula α n) ≤ max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
refine lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans ?_)

Premises used: Computability.Encoding.card_le_card_list, Iff.mp, LE.le.trans, FirstOrder.Language.BoundedFormula.encoding, Cardinal.lift_le
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
rw :
  lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
⊢ lift.{max (max u' v) u, max (max u' v) u}
      #(List (Encoding.Γ (α := (n : ℕ) × L.BoundedFormula α n) BoundedFormula.encoding)) ≤
    lift.{max (max u u') v, max (max u u') v} (max ℵ₀ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
rw [encoding_Γ, mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0,
    max_le_iff]

Premises used: Cardinal.mk_list_eq_max_mk_aleph0, max_le_iff, Cardinal.lift_aleph0, FirstOrder.Language.BoundedFormula.encoding_Γ, Cardinal.lift_max
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
⟨?_, le_max_left _ _⟩

Premises used: And.intro, le_max_left
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
refine :
  lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)) ∧
    ℵ₀ ≤ max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
refine ⟨?_, le_max_left _ _⟩
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
rw :
  lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]

Premises used: le_rfl, Cardinal.mk_nat, Cardinal.add_eq_max, FirstOrder.Language.Term.card_sigma, Cardinal.mk_sum
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
simp :
  ℵ₀ + (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) +
      (lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
simp only [lift_add, lift_lift, lift_aleph0]

Premises used: Cardinal.lift_lift, Cardinal.lift_aleph0, Cardinal.lift_add
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable.{u' + 1} (constantsOn α).Symbols

Tactic:
mk_le_aleph0_iff.mp ?_

Premises used: Cardinal.mk_le_aleph0_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
refine : #(constantsOn α).Symbols ≤ ℵ₀
⊢ Countable.{u' + 1} (constantsOn α).Symbols

Tactic:
refine mk_le_aleph0_iff.mp ?_

Premises used: Cardinal.mk_le_aleph0_iff, Iff.mp
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ (constantsOn α).card ≤ ℵ₀

Tactic:
simpa only [card_constantsOn, mk_le_aleph0_iff]

Premises used: Cardinal.mk_le_aleph0_iff, FirstOrder.Language.card_constantsOn
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
simp : #L[[α]].Symbols ≤ ℵ₀
⊢ Countable L[[α]].Symbols

Tactic:
simp only [← mk_le_aleph0_iff]

Premises used: Cardinal.mk_le_aleph0_iff
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
simp : L.card ≤ ℵ₀ ∧ (constantsOn α).card ≤ ℵ₀
⊢ L[[α]].card ≤ ℵ₀

Tactic:
simp only [withConstants, card_sum, add_le_aleph0, lift_le_aleph0]

Premises used: Cardinal.add_le_aleph0, Cardinal.lift_le_aleph0, FirstOrder.Language.withConstants, FirstOrder.Language.card_sum
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
simp : Countable L.Symbols ∧ Countable.{u' + 1} (constantsOn α).Symbols
⊢ L.card ≤ ℵ₀ ∧ (constantsOn α).card ≤ ℵ₀

Tactic:
simp only [card, mk_le_aleph0_iff]

Premises used: FirstOrder.Language.card, Cardinal.mk_le_aleph0_iff
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
left : Countable L.Symbols
right : Countable.{u' + 1} (constantsOn α).Symbols
⊢ Countable L.Symbols ∧ Countable.{u' + 1} (constantsOn α).Symbols

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable L.Symbols

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable.{u' + 1} (constantsOn α).Symbols

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable ((n : ℕ) × L.BoundedFormula α n)

Tactic:
Cardinal.mk_le_aleph0_iff.mp (BoundedFormula.card_le.trans (max_le (le_refl _) ?_))

Premises used: le_refl, Cardinal.mk_le_aleph0_iff, max_le, Iff.mp, LE.le.trans, FirstOrder.Language.BoundedFormula.card_le
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
refine : lift.{max u v, u'} #α + lift.{u', max u v} L.card ≤ ℵ₀
⊢ Countable ((n : ℕ) × L.BoundedFormula α n)

Tactic:
refine Cardinal.mk_le_aleph0_iff.mp (BoundedFormula.card_le.trans (max_le (le_refl _) ?_))

Premises used: le_refl, Cardinal.mk_le_aleph0_iff, max_le, Iff.mp, LE.le.trans, FirstOrder.Language.BoundedFormula.card_le
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
simp : Countable α ∧ Countable L.Symbols
⊢ lift.{max u v, u'} #α + lift.{u', max u v} L.card ≤ ℵ₀

Tactic:
simp only [card, add_le_aleph0, lift_le_aleph0, mk_le_aleph0_iff]

Premises used: Cardinal.add_le_aleph0, Cardinal.lift_le_aleph0, FirstOrder.Language.card, Cardinal.mk_le_aleph0_iff
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
left : Countable α
right : Countable L.Symbols
⊢ Countable α ∧ Countable L.Symbols

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable α

Tactic:
infer_instance
-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable (L.Formula α)

Tactic:
(Function.Injective.countable
    (f := fun φ => (⟨0, φ⟩ : Σ n, L.BoundedFormula α n))) <| sigma_mk_injective

Premises used: Function.Injective.countable, sigma_mk_injective
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ φ ⟹[T] φ

Tactic:
fun _ _ _ => id

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, id, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Theory.Imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
M : Type u_1
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
⊢ Std.Refl (α := L.BoundedFormula α n) T.Imp

Tactic:
⟨Imp.refl⟩

Premises used: Std.Refl.mk, FirstOrder.Language.Theory.Imp.refl
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⟹[T] ψ
h2 : ψ ⟹[T] θ
⊢ φ ⟹[T] θ

Tactic:
fun M v xs => (h2 M v xs) ∘ (h1 M v xs)

Premises used: FirstOrder.Language.Theory.ModelsBoundedFormula, Function.comp, FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.Theory.Imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
M : Type u_1
inst : Nonempty M
inst_1 : L.Structure M
inst_2 : M ⊨ T
⊢ IsTrans (L.BoundedFormula α n) T.Imp

Tactic:
⟨fun _ _ _ => Imp.trans⟩

Premises used: IsTrans.mk, FirstOrder.Language.Theory.Imp.trans
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (⊥ ⟹ φ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_bot, false_implies]

Premises used: false_implies, FirstOrder.Language.BoundedFormula.realize_bot, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⟹ ⊤).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_top, implies_true]

Premises used: FirstOrder.Language.BoundedFormula.realize_top, implies_true, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
simp : φ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
⊢ (φ ⟹ φ ⊔ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]

Premises used: FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.realize_sup
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
Or.inl

Premises used: Or.inl
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
exact Or.inl

Premises used: Or.inl
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
simp : ψ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
⊢ (ψ ⟹ φ ⊔ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]

Premises used: FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.realize_sup
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ ψ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
Or.inr

Premises used: Or.inr
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ ψ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
exact Or.inr

Premises used: Or.inr
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
simp : φ.Realize v xs ∨ ψ.Realize v xs → θ.Realize v xs
⊢ (φ ⊔ ψ ⟹ θ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]

Premises used: FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.BoundedFormula.realize_sup
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs ∨ ψ.Realize v xs → θ.Realize v xs

Tactic:
fun h => h.elim (h₁ M v xs) (h₂ M v xs)

Premises used: Or.elim
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs ∨ ψ.Realize v xs → θ.Realize v xs

Tactic:
exact fun h => h.elim (h₁ M v xs) (h₂ M v xs)
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
⊢ φ ⊔ ψ ⟹[T] θ ↔ φ ⟹[T] θ ∧ ψ ⟹[T] θ

Tactic:
⟨fun h => ⟨(imp_sup_left _ _).trans h, (imp_sup_right _ _).trans h⟩,
    fun ⟨h₁, h₂⟩ => sup_imp h₁ h₂⟩

Premises used: FirstOrder.Language.Theory.imp_sup_right, _private.0.FirstOrder.Language.Theory.sup_imp_iff.match_1, FirstOrder.Language.Theory.imp_sup_left, FirstOrder.Language.Theory.Imp, Max.max, And.intro, Iff.intro, FirstOrder.Language.Theory.Imp.trans, FirstOrder.Language.Theory.sup_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
simp : φ.Realize v xs ∧ ψ.Realize v xs → φ.Realize v xs
⊢ (φ ⊓ ψ ⟹ φ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs ∧ ψ.Realize v xs → φ.Realize v xs

Tactic:
And.left

Premises used: And.left
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs ∧ ψ.Realize v xs → φ.Realize v xs

Tactic:
exact And.left

Premises used: And.left
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
simp : φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs
⊢ (φ ⊓ ψ ⟹ ψ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Equivalence
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs

Tactic:
And.right

Premises used: And.right