awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
⊢ VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure
have h : ∀ (A : Set α) (hA : MeasurableSet A),
  (↑(VectorMeasure.restrict μ.toSignedMeasure s) : Set α → ℝ) A = (↑(μ.restrict s).toSignedMeasure : Set α → ℝ) A
Tactic: ext A hA
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν
have rw : (∀ (i : Set α), MeasurableSet i → (↑μ.toSignedMeasure : Set α → ℝ) i ≤ (↑ν.toSignedMeasure : Set α → ℝ) i) ↔
  ∀ (s : Set α),
    MeasurableSet s → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [Measure.le_iff, VectorMeasure.le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (∀ (i : Set α), MeasurableSet i → (↑μ.toSignedMeasure : Set α → ℝ) i ≤ (↑ν.toSignedMeasure : Set α → ℝ) i) ↔
    ∀ (s : Set α),
      MeasurableSet s → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a : ∀ (s : Set α) (hs : MeasurableSet s),
  (↑μ.toSignedMeasure : Set α → ℝ) s ≤ (↑ν.toSignedMeasure : Set α → ℝ) s ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: congrm ∀ s, (hs : MeasurableSet s) → ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ (↑μ.toSignedMeasure : Set α → ℝ) s ≤ (↑ν.toSignedMeasure : Set α → ℝ) s ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ≤ ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) s) ↔
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [toSignedMeasure_apply_measurable hs, real_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ≤ ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) s) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply ENNReal.toReal_le_toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
a : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ≤ ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) s) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply ENNReal.toReal_le_toReal
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p q : T.CompleteType α
h :
  Eq (α := Set L[[α]].Sentence) ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) p)
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) q)
⊢ p = q
have mk : ∀ (toTheory : L[[α]].Theory) (subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory) (isMaximal' : toTheory.IsMaximal)
  (h :
    Eq (α := Set L[[α]].Sentence)
      ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (mk (T := T) toTheory subset' isMaximal'))
      ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) q)),
  mk (T := T) toTheory subset' isMaximal' = q
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
q : T.CompleteType α
toTheory : L[[α]].Theory
subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory
isMaximal' : toTheory.IsMaximal
h :
  Eq (α := Set L[[α]].Sentence)
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (mk (T := T) toTheory subset' isMaximal'))
    ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) q)
⊢ mk (T := T) toTheory subset' isMaximal' = q
have mk : ∀ (toTheory_1 : L[[α]].Theory) (subset'_1 : (L.lhomWithConstants α).onTheory T ⊆ toTheory_1)
  (isMaximal'_1 : toTheory_1.IsMaximal)
  (h :
    Eq (α := Set L[[α]].Sentence)
      ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (mk (T := T) toTheory subset' isMaximal'))
      ((fun (p : T.CompleteType α) ↦ (↑p : L[[α]].Theory)) (mk (T := T) toTheory_1 subset'_1 isMaximal'_1))),
  mk (T := T) toTheory subset' isMaximal' = mk (T := T) toTheory_1 subset'_1 isMaximal'_1
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.ModelTheory.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
Carrier : Type (max (max u w) v)
struc : L[[α]].Structure Carrier
h : Model (L := L[[α]]) Carrier {φ, Formula.not φ}
nonempty' : Nonempty Carrier
⊢ False
have h₁ : Carrier ⊨ φ ∧ Carrier ⊨ Formula.not φ
Tactic: simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
⊢ False
have h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
Tactic: have h : ¬IsSatisfiable ({φ, φ.not} : L[[α]].Theory) := by
      rintro ⟨@⟨_, _, h, _⟩⟩
      simp only [model_iff, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] at h
      exact h.2 h.1
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
⊢ False
have refine : {φ, Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)
Tactic: refine h (p.isMaximal.1.mono ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
φ : L[[α]].Sentence
hf : Formula.not φ ∈ p
ht : φ ∈ p
h : ¬IsSatisfiable (L := L[[α]]) {φ, Formula.not φ}
⊢ {φ, Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)
have rw : φ ∈ (↑p : Set L[[α]].Sentence) ∧ Formula.not φ ∈ (↑p : Set L[[α]].Sentence)
Tactic: rw [insert_subset_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} ∅ ↔
    ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
have rw : ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔
  ∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x
Tactic: rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔
    ∃ (x : T.CompleteType α),
      Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x
have h : (∃ (x : T.CompleteType α),
    Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x) →
  ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
Tactic: refine
    ⟨fun h =>
      ⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
          completeTheory.isMaximal L[[α]] h.some⟩,
        (((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
      ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
have rw : Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | Formula.not φ ∈ p} ∅ ↔
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | {Formula.not φ} ⊆ (↑p : Set L[[α]].Sentence)} ∅
Tactic: rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
have h : ∀ (x : T.CompleteType α),
  Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} x ↔
    Membership.mem (γ := Set (T.CompleteType α))
      (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Types (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} Set.univ ↔
    ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
have h : Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
  (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
Tactic: have h : { p : T.CompleteType α | S ⊆ ↑p } = ⋂₀ ((fun φ => { p | φ ∈ p }) '' S) := by
    ext
    simp [subset_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
⊢ Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)} Set.univ ↔
    ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
have simp_rw : (∀ (s : Set (T.CompleteType α)),
    Membership.mem (γ := Set (Set (T.CompleteType α)))
        ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
      s = Set.univ) ↔
  ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ
Tactic: simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h :
  Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | S ⊆ (↑p : Set L[[α]].Sentence)}
    (⋂₀ ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S))
⊢ (∀ (s : Set (T.CompleteType α)),
      Membership.mem (γ := Set (Set (T.CompleteType α)))
          ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
        s = Set.univ) ↔
    ∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ
have refine : (∀ φ ∈ S, Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | φ ∈ p} Set.univ) →
  ∀ (s : Set (T.CompleteType α)),
    Membership.mem (γ := Set (Set (T.CompleteType α)))
        ((fun (φ : L[[α]].Sentence) ↦ {p : T.CompleteType α | φ ∈ p}) '' S) s →
      s = Set.univ
Tactic: refine ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ T.IsSatisfiable
have rw : Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable
Tactic: rw [← isSatisfiable_onTheory_iff (lhomWithConstants_injective L α)]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
⊢ Nonempty (T.CompleteType α) ↔ ((L.lhomWithConstants α).onTheory T).IsSatisfiable
have rw : Eq (α := Set (T.CompleteType α)) {p : T.CompleteType α | ∅ ⊆ (↑p : Set L[[α]].Sentence)} ∅ ↔
  Eq (α := Set (T.CompleteType α)) Set.univ ∅
Tactic: rw [nonempty_iff_univ_nonempty, nonempty_iff_ne_empty, Ne, not_iff_comm,
    ← union_empty ((L.lhomWithConstants α).onTheory T), ← setOf_subset_eq_empty_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
ι : Type u_1
S : ι → L[[α]].Theory
⊢ Eq (α := Set (T.CompleteType α)) (⋂ (i : ι), {p : T.CompleteType α | S i ⊆ (↑p : Set L[[α]].Sentence)})
    {p : T.CompleteType α | ⋃ (i : ι), S i ⊆ (↑p : Set L[[α]].Sentence)}
have h : ∀ (x : T.CompleteType α),
  Membership.mem (γ := Set (T.CompleteType α)) (⋂ (i : ι), {p : T.CompleteType α | S i ⊆ (↑p : Set L[[α]].Sentence)})
      x ↔
    Membership.mem (γ := Set (T.CompleteType α)) {p : T.CompleteType α | ⋃ (i : ι), S i ⊆ (↑p : Set L[[α]].Sentence)} x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ List.foldr (fun (x1 x2 : L[[α]].Sentence) ↦ x1 ⊓ x2) ⊤ t.toList ∈ p ↔
    (↑t : Set L[[α]].Sentence) ⊆ (↑p : Set L[[α]].Sentence)
have simp_rw : (∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
    ∀ φ ∈ t, φ.Realize (M := (↑M : Type (max (max u w) v))) default default) ↔
  ∀ x ∈ (↑t : Set L[[α]].Sentence),
    ∀ (M : ModelType (↑p : Set L[[α]].Sentence)),
      BoundedFormula.Realize (M := (↑M : Type (max (max u w) v))) x default default
Tactic: simp_rw [subset_def, ← SetLike.mem_coe, p.isMaximal.mem_iff_models, models_sentence_iff,
    Sentence.Realize, Formula.Realize, BoundedFormula.realize_foldr_inf, Finset.mem_toList]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
⊢ T.typesWith (φ ⊓ ψ) = T.typesWith φ ∩ T.typesWith ψ
have h : ∀ (p : T.CompleteType α), p ∈ T.typesWith (φ ⊓ ψ) ↔ p ∈ T.typesWith φ ∩ T.typesWith ψ
Tactic: ext p
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
φ ψ : L[[α]].Sentence
p : T.CompleteType α
⊢ p ∈ T.typesWith (φ ⊓ ψ) ↔ p ∈ T.typesWith φ ∩ T.typesWith ψ
have h : (∀ (M : ModelType (↑p : Set L[[α]].Sentence)) (v : Empty → (↑M : Type (max (max u w) v)))
    (xs : Fin 0 → (↑M : Type (max (max u w) v))), BoundedFormula.Realize (φ ⊓ ψ) v xs) ↔
  ∀ (x : ModelType (↑p : Set L[[α]].Sentence)) (x_1 : Empty → (↑x : Type (max (max u w) v)))
    (x_2 : Fin 0 → (↑x : Type (max (max u w) v))), BoundedFormula.Realize φ x_1 x_2 ∧ BoundedFormula.Realize ψ x_1 x_2
Tactic: simp only [mem_typesWith_iff, mem_inter_iff, ← SetLike.mem_coe, p.isMaximal.mem_iff_models,
    ModelsBoundedFormula, ← forall_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
⊢ ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α
have obtain : ∀ (M : ModelType (↑p : Set L[[α]].Sentence)), ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α
Tactic: obtain ⟨M⟩ := p.isMaximal.1
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
⊢ ∃ (M : T.ModelType), p ∈ T.realizedTypes (↑M : Type (max (max u v) w)) α
have refine : (T.typeOf (M :=
    (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
          (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) sorry)) :
      Type (max (max u v) w)))
    fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w)))) =
  p
Tactic: refine ⟨(M.subtheoryModel p.subset).reduct (L.lhomWithConstants α), fun a => (L.con a : M), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
⊢ (T.typeOf (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w)))) =
    p
have refine : ∀ (φ : L[[α]].Sentence),
  Membership.mem (γ := T.CompleteType α)
      (T.typeOf (M :=
        (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
              (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) sorry)) :
          Type (max (max u v) w)))
        fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w))))
      φ ↔
    φ ∈ p
Tactic: refine SetLike.ext fun φ => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
φ : L[[α]].Sentence
⊢ Membership.mem (γ := T.CompleteType α)
      (T.typeOf (M :=
        (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
              (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
          Type (max (max u v) w)))
        fun (a : α) ↦ (↑(L.con a) : (↑M : Type (max (max u v) w))))
      φ ↔
    φ ∈ p
have simp : (Formula.Realize (L := L) (M :=
    (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
          (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) sorry)) :
      Type (max (max u v) w)))
    ((_root_.Equiv.symm Formula.equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) fun (a : α) ↦
    (↑(L.con a) : (↑M : Type (max (max u v) w)))) ↔
  φ ∈ p
Tactic: simp only [CompleteType.mem_typeOf]
-- Lean 4 proof step from Mathlib.ModelTheory.Types (goal)
Goal:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
M : ModelType (↑p : Set L[[α]].Sentence)
φ : L[[α]].Sentence
⊢ (Formula.Realize (L := L) (M :=
      (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
            (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) ⋯)) :
        Type (max (max u v) w)))
      ((_root_.Equiv.symm Formula.equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) fun (a : α) ↦
      (↑(L.con a) : (↑M : Type (max (max u v) w)))) ↔
    φ ∈ p
have _ : (↑(ModelType.reduct (T := T) (L.lhomWithConstants α)
          (M.subtheoryModel (T := (↑p : Set L[[α]].Sentence)) (T' := (L.lhomWithConstants α).onTheory T) sorry)) :
      Type (max (max u v) w)) ⊨
    φ ↔
  (↑M : Type (max (max u v) w)) ⊨ φ
Tactic: refine
    (@Formula.realize_equivSentence_symm_con _
      ((M.subtheoryModel p.subset).reduct (L.lhomWithConstants α)) _ _ M.struc _ φ).trans
      (_root_.trans (_root_.trans ?_ (p.isMaximal.isComplete.realize_sentence_iff φ M))
        (p.isMaximal.mem_iff_models φ).symm)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ Fintype.card.{u_1} (InfinitePlace K) - 1 = 0
have rw : Nat.totient 3 / 2 - 1 = 0
Tactic: rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide),
      zero_add, nrComplexPlaces_eq_totient_div_two (n := 3)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (hypothesis)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
have hrank : rank K = 0
Tactic: have hrank : rank K = 0 := by
    dsimp only [rank]
    rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide),
      zero_add, nrComplexPlaces_eq_totient_div_two (n := 3)]
    rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
⊢ u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) ⋯, -IsUnit.unit (a := hζ.toInteger) ⋯,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) ⋯) 2]
have obtain : ∀ (x : ↥(torsion K)) (e : Fin (rank K) → ℤ)
  (hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i),
  u ∈
    [1, -1, IsUnit.unit (a := hζ.toInteger) sorry, -IsUnit.unit (a := hζ.toInteger) sorry,
      HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) sorry) 2,
      -HPow.hPow (β := ℕ) (IsUnit.unit (a := hζ.toInteger) sorry) 2]
Tactic: obtain ⟨⟨x, e⟩, hxu, -⟩ := exist_unique_eq_mul_prod _ u
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ u = (↑x : (𝓞 K)ˣ)
have rw : (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i = (↑x : (𝓞 K)ˣ) * 1
Tactic: rw [← mul_one x.1, hxu]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i = (↑x : (𝓞 K)ˣ) * 1
have h : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i) 1
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i) 1
have h : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i)
  (∏ x_1 ∈ ∅, fundSystem K x_1 ^ (x, e).2 x_1)
Tactic: rw [← Finset.prod_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
h :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i)
    (∏ x_1 ∈ ∅, fundSystem K x_1 ^ (x, e).2 x_1)
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i) 1
have rw : Type
Tactic: rw [← Finset.prod_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
h :
  Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i)
    (∏ x_1 ∈ ∅, fundSystem K x_1 ^ (x, e).2 x_1)
rw : Type
⊢ Eq.{u_1 + 1} (α := (𝓞 K)ˣ) (∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i) 1
have rw₁ : Fin (rank K) → (𝓞 K)ˣ
Tactic: rw [← Finset.prod_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Three (goal)
Goal:
K : Type u_1
inst : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = (↑(x, e).1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ (x, e).2 i
⊢ Eq (α := Finset (Fin (rank K))) Finset.univ ∅
have h : IsEmpty (Fin 0)
Tactic: rw [Finset.univ_eq_empty_iff, hrank]