awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁
ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂
h : ((LHom.id L).onBoundedFormula f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₁ : (id f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₂ : (id f₁).imp (id f₂) = id (f₁.imp f₂)
h₃ : f₁.imp (id f₂) = id (f₁.imp f₂)
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
have h₄ : f₁.imp f₂ = id (f₁.imp f₂)
Tactic: rw [onBoundedFormula, ih1, ih2, id, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f₁ f₂ : L.BoundedFormula α n_1
ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁
ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂
h : ((LHom.id L).onBoundedFormula f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₁ : (id f₁).imp ((LHom.id L).onBoundedFormula f₂) = id (f₁.imp f₂)
h₂ : (id f₁).imp (id f₂) = id (f₁.imp f₂)
h₃ : f₁.imp (id f₂) = id (f₁.imp f₂)
h₄ : f₁.imp f₂ = id (f₁.imp f₂)
⊢ (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
have h₅ : f₁.imp f₂ = f₁.imp f₂
Tactic: rw [onBoundedFormula, ih1, ih2, id, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : (LHom.id L).onBoundedFormula f = id f
⊢ (LHom.id L).onBoundedFormula f.all = id f.all
have h : ((LHom.id L).onBoundedFormula f).all = id f.all
Tactic: rw [onBoundedFormula, ih3, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : (LHom.id L).onBoundedFormula f = id f
h : ((LHom.id L).onBoundedFormula f).all = id f.all
⊢ (LHom.id L).onBoundedFormula f.all = id f.all
have h₁ : (id f).all = id f.all
Tactic: rw [onBoundedFormula, ih3, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : (LHom.id L).onBoundedFormula f = id f
h : ((LHom.id L).onBoundedFormula f).all = id f.all
h₁ : (id f).all = id f.all
⊢ (LHom.id L).onBoundedFormula f.all = id f.all
have h₂ : f.all = id f.all
Tactic: rw [onBoundedFormula, ih3, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n n_1 : ℕ
f : L.BoundedFormula α (n_1 + 1)
ih3 : (LHom.id L).onBoundedFormula f = id f
h : ((LHom.id L).onBoundedFormula f).all = id f.all
h₁ : (id f).all = id f.all
h₂ : f.all = id f.all
⊢ (LHom.id L).onBoundedFormula f.all = id f.all
have h₃ : f.all = f.all
Tactic: rw [onBoundedFormula, ih3, id, id]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
⊢ (LHom.id L).onBoundedFormula f = id f
have h : ∀ {n : ℕ}, Eq (α := L.BoundedFormula α n) ((LHom.id L).onBoundedFormula falsum) (id falsum)
Tactic: induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
h : ∀ {n : ℕ}, Eq (α := L.BoundedFormula α n) ((LHom.id L).onBoundedFormula falsum) (id falsum)
⊢ (LHom.id L).onBoundedFormula f = id f
have h₁ : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)), (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
Tactic: induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
h : ∀ {n : ℕ}, Eq (α := L.BoundedFormula α n) ((LHom.id L).onBoundedFormula falsum) (id falsum)
h₁ : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)), (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
⊢ (LHom.id L).onBoundedFormula f = id f
have h₂ : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
  (LHom.id L).onBoundedFormula (rel R ts) = id (rel R ts)
Tactic: induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
h : ∀ {n : ℕ}, Eq (α := L.BoundedFormula α n) ((LHom.id L).onBoundedFormula falsum) (id falsum)
h₁ : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)), (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
h₂ :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (LHom.id L).onBoundedFormula (rel R ts) = id (rel R ts)
⊢ (LHom.id L).onBoundedFormula f = id f
have h₃ : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n) (ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁)
  (ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂), (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
Tactic: induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
h : ∀ {n : ℕ}, Eq (α := L.BoundedFormula α n) ((LHom.id L).onBoundedFormula falsum) (id falsum)
h₁ : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)), (LHom.id L).onBoundedFormula (equal t₁ t₂) = id (equal t₁ t₂)
h₂ :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (LHom.id L).onBoundedFormula (rel R ts) = id (rel R ts)
h₃ :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n) (ih1 : (LHom.id L).onBoundedFormula f₁ = id f₁)
    (ih2 : (LHom.id L).onBoundedFormula f₂ = id f₂), (LHom.id L).onBoundedFormula (f₁.imp f₂) = id (f₁.imp f₂)
⊢ (LHom.id L).onBoundedFormula f = id f
have h₄ : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1)) (ih3 : (LHom.id L).onBoundedFormula f = id f),
  (LHom.id L).onBoundedFormula f.all = id f.all
Tactic: induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
⊢ Eq (α := L.BoundedFormula α n → L''.BoundedFormula α n) (φ.comp ψ).onBoundedFormula
    (φ.onBoundedFormula ∘ ψ.onBoundedFormula)
have h : ∀ (f : L.BoundedFormula α n), (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
⊢ (φ.comp ψ).onBoundedFormula (rel R ts) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R ts)
have h : (φ.onRelation (ψ.onRelation R)).boundedFormula ((φ.onTerm ∘ ψ.onTerm) ∘ ts) =
  φ.onBoundedFormula ((ψ.onRelation R).boundedFormula (ψ.onTerm ∘ ts))
Tactic: simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
have h : ∀ {n : ℕ},
  Eq (α := L''.BoundedFormula α n) ((φ.comp ψ).onBoundedFormula falsum)
    ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)
Tactic: induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
h :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula α n) ((φ.comp ψ).onBoundedFormula falsum)
      ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
have h₁ : ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
  (φ.comp ψ).onBoundedFormula (equal t₁ t₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁ t₂)
Tactic: induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
h :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula α n) ((φ.comp ψ).onBoundedFormula falsum)
      ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)
h₁ :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (equal t₁ t₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁ t₂)
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
have h₂ : ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
  (φ.comp ψ).onBoundedFormula (rel R ts) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R ts)
Tactic: induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
h :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula α n) ((φ.comp ψ).onBoundedFormula falsum)
      ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)
h₁ :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (equal t₁ t₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁ t₂)
h₂ :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (rel R ts) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R ts)
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
have h₃ : ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
  (ih1 : (φ.comp ψ).onBoundedFormula f₁ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₁)
  (ih2 : (φ.comp ψ).onBoundedFormula f₂ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₂),
  (φ.comp ψ).onBoundedFormula (f₁.imp f₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (f₁.imp f₂)
Tactic: induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
α : Type u'
n : ℕ
L'' : Language
φ : L' →ᴸ L''
ψ : L →ᴸ L'
f : L.BoundedFormula α n
h :
  ∀ {n : ℕ},
    Eq (α := L''.BoundedFormula α n) ((φ.comp ψ).onBoundedFormula falsum)
      ((φ.onBoundedFormula ∘ ψ.onBoundedFormula) falsum)
h₁ :
  ∀ {n : ℕ} (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (equal t₁ t₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (equal t₁ t₂)
h₂ :
  ∀ {n l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
    (φ.comp ψ).onBoundedFormula (rel R ts) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (rel R ts)
h₃ :
  ∀ {n : ℕ} (f₁ f₂ : L.BoundedFormula α n)
    (ih1 : (φ.comp ψ).onBoundedFormula f₁ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₁)
    (ih2 : (φ.comp ψ).onBoundedFormula f₂ = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f₂),
    (φ.comp ψ).onBoundedFormula (f₁.imp f₂) = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) (f₁.imp f₂)
⊢ (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f
have h₄ : ∀ {n : ℕ} (f : L.BoundedFormula α (n + 1))
  (ih3 : (φ.comp ψ).onBoundedFormula f = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f),
  (φ.comp ψ).onBoundedFormula f.all = (φ.onBoundedFormula ∘ ψ.onBoundedFormula) f.all
Tactic: induction f with
  | falsum => rfl
  | equal => simp [Term.bdEqual]
  | rel => simp only [onBoundedFormula, comp_onRelation, comp_onTerm, Function.comp_apply]; rfl
  | imp _ _ ih1 ih2 =>
    simp only [onBoundedFormula, Function.comp_apply, ih1, ih2]
  | all _ ih3 => simp only [ih3, onBoundedFormula, Function.comp_apply]
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.LeftInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.onBoundedFormula ∘ φ.toLHom.onBoundedFormula) id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.onBoundedFormula ∘ φ.toLHom.onBoundedFormula) id
⊢ Function.LeftInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw₁ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.comp φ.toLHom).onBoundedFormula id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.onBoundedFormula ∘ φ.toLHom.onBoundedFormula) id
rw₁ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.comp φ.toLHom).onBoundedFormula id
⊢ Function.LeftInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw₂ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (LHom.id L).onBoundedFormula id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.onBoundedFormula ∘ φ.toLHom.onBoundedFormula) id
rw₁ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (φ.invLHom.comp φ.toLHom).onBoundedFormula id
rw₂ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) (LHom.id L).onBoundedFormula id
⊢ Function.LeftInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw₃ : Eq (α := L.BoundedFormula α n → L.BoundedFormula α n) id id
Tactic: rw [Function.leftInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.left_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
⊢ Function.RightInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.onBoundedFormula ∘ φ.invLHom.onBoundedFormula) id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.onBoundedFormula ∘ φ.invLHom.onBoundedFormula) id
⊢ Function.RightInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw₁ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.comp φ.invLHom).onBoundedFormula id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.onBoundedFormula ∘ φ.invLHom.onBoundedFormula) id
rw₁ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.comp φ.invLHom).onBoundedFormula id
⊢ Function.RightInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw₂ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (LHom.id L').onBoundedFormula id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n : ℕ
φ : L ≃ᴸ L'
rw : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.onBoundedFormula ∘ φ.invLHom.onBoundedFormula) id
rw₁ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (φ.toLHom.comp φ.invLHom).onBoundedFormula id
rw₂ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) (LHom.id L').onBoundedFormula id
⊢ Function.RightInverse (α := L.BoundedFormula α n) φ.invLHom.onBoundedFormula φ.toLHom.onBoundedFormula
have rw₃ : Eq (α := L'.BoundedFormula α n → L'.BoundedFormula α n) id id
Tactic: rw [Function.rightInverse_iff_comp, ← LHom.comp_onBoundedFormula, φ.right_inv,
      LHom.id_onBoundedFormula]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
⊢ Eq (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    (⋃ (t : Finset (↑s : Type u')),
      (fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
        ((↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α) ∩
          (diagonal α)ᶜ))
have rw : Eq (α := L[[α]].Theory)
  ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
  ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
    ((⋃ (i : Finset (↑s : Type u')),
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)) ∩
      (diagonal α)ᶜ))
Tactic: rw [← image_iUnion, ← iUnion_inter]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
⊢ Eq (α := L[[α]].Theory)
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) '' (s ×ˢ s ∩ (diagonal α)ᶜ))
    ((fun (ab : α × α) ↦ Formula.not (Term.equal (L.con ab.1).term (L.con ab.2).term)) ''
      ((⋃ (i : Finset (↑s : Type u')),
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
            (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)) ∩
        (diagonal α)ᶜ))
have refine : s ×ˢ s =
  ⋃ (i : Finset (↑s : Type u')),
    (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
      (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
Tactic: refine congr(_ '' ($(?_) ∩ _))
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
⊢ s ×ˢ s =
    ⋃ (i : Finset (↑s : Type u')),
      (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
have h : ∀ (i j : α),
  (i, j) ∈ s ×ˢ s ↔
    Membership.mem (γ := Set (α × α))
      (⋃ (i : Finset (↑s : Type u')),
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
      (i, j)
Tactic: ext ⟨i, j⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
i j : α
⊢ (i, j) ∈ s ×ˢ s ↔
    Membership.mem (γ := Set (α × α))
      (⋃ (i : Finset (↑s : Type u')),
        (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α) ×ˢ
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
      (i, j)
have h : i ∈ s ∧ j ∈ s ↔
  ∃ (i_1 : Finset (↑s : Type u')),
    (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i sorry ∈ i_1) ∧
      ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j sorry ∈ i_1
Tactic: simp only [prodMk_mem_set_prod_eq, Finset.coe_map, Function.Embedding.coe_subtype, mem_iUnion,
      mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right]
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
i j : α
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ i_1
have h : ∀ (h : i ∈ s ∧ j ∈ s),
  Membership.mem (γ := Finset { x : α // x ∈ s })
    {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i sorry, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j sorry}
    (Subtype.mk (p := fun (a : α) ↦ a ∈ s) i sorry)
Tactic: refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Syntax (goal)
Goal:
L : Language
α : Type u'
s : Set α
i j : α
h :
  ∀ (h : i ∈ s ∧ j ∈ s),
    Membership.mem (γ := Finset { x : α // x ∈ s })
      {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i ⋯, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j ⋯}
      (Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯)
⊢ i ∈ s ∧ j ∈ s ↔
    ∃ (i_1 : Finset (↑s : Type u')),
      (∃ (x : i ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) i ⋯ ∈ i_1) ∧
        ∃ (x : j ∈ s), Subtype.mk (p := fun (a : α) ↦ a ∈ s) j ⋯ ∈ i_1
have h₁ : ∀ (h : i ∈ s ∧ j ∈ s),
  Membership.mem (γ := Finset { x : α // x ∈ s })
    {Subtype.mk (p := fun (x : α) ↦ x ∈ s) i sorry, Subtype.mk (p := fun (x : α) ↦ x ∈ s) j sorry}
    (Subtype.mk (p := fun (a : α) ↦ a ∈ s) j sorry)
Tactic: refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩