awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
⊢ Nonempty { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p) }
have a : ∀ q ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}, Theory.ACF (↑q : ℕ) ⊨ᵇ ∼(eqZero p)
Tactic: refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
⊢ (∼(eqZero p)).Realize v xs
have hqp : q ≠ p
Tactic: have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
⊢ (∼(eqZero p)).Realize v xs
have this : K ⊨ Theory.field
Tactic: have := modelField_of_modelACF q K
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
this : K ⊨ Theory.field
x_1 : CompatibleRing K := compatibleRingOfModelField K
⊢ (∼(eqZero p)).Realize v xs
have this₁ : CharP K q
Tactic: have := charP_of_model_fieldOfChar q K
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
p : ℕ
hp : Membership.mem (γ := Set ℕ) {q : ℕ | Nat.Prime q} p
q : ℕ
property : Nat.Prime q
hq : Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property ∉ {Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) p hp}
K : Type
struc : Language.ring.Structure K
is_model : K ⊨ Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)
nonempty' : Nonempty K
v :
  Empty →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
xs :
  Fin 0 →
    (↑(Theory.ModelType.mk (T := Theory.ACF (↑(Subtype.mk (p := fun (p : ℕ) ↦ Nat.Prime p) q property) : ℕ)) K) : Type)
hqp : q ≠ p
x : Field K := fieldOfModelACF q K
this_1 : K ⊨ Theory.field
x_1 : CompatibleRing K := compatibleRingOfModelField K
this : CharP K q
⊢ (∼(eqZero p)).Realize v xs
have a : ¬CharP K p
Tactic: simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
have have : ∀
  (f :
    (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }),
  Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
Tactic: have f : ∀ ψ ∈ Theory.ACF 0,
      { s : Finset Nat.Primes // ∀ q : Nat.Primes, q ∉ s → Theory.ACF q ⊨ᵇ ψ } := by
    intro ψ hψ
    rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl,
      Set.mem_image] at hψ
    apply Classical.choice
    rcases hψ with h | ⟨p, hp, rfl⟩
    · refine ⟨⟨∅, ?_⟩⟩
      intro q _
      exact Theory.models_sentence_of_mem
        (by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm];
            exact Set.mem_union_left _ h)
    · refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
      rintro ⟨q, _⟩ hq ⟨K⟩ _ _
      have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
      let _ := fieldOfModelACF q K
      have := modelField_of_modelACF q K
      let _ := compatibleRingOfModelField K
      have := charP_of_model_fieldOfChar q K
      simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual,
        Term.realize_relabel, Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast,
        realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
      intro _
      exact hqp <| CharP.eq K this inferInstance
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : p ∉ s
⊢ Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
have hpψ₁ : ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ (↑(f x sorry) : Finset Nat.Primes)
Tactic: simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
      Subtype.exists, not_exists] at hpψ
Cleared hypotheses: hpψ
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (hypothesis)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
have hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
Tactic: have hs : ∀ (p : Nat.Primes) ψ, ψ ∈ T0 → p ∉ s → Theory.ACF p ⊨ᵇ ψ := by
    intro p ψ hψ hpψ
    simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and,
      Subtype.exists, not_exists] at hpψ
    exact (f ψ (hT0 hψ)).2 p (hpψ _ hψ)
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : (↑T0 : Set Language.ring.Sentence) ⊆ Theory.ACF 0
h : (↑T0 : Set Language.ring.Sentence) ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s : Finset Nat.Primes // ∀ q ∉ s, Theory.ACF (↑q : ℕ) ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun (φ : ↥T0) ↦ (↑(f (↑φ : Language.ring.Sentence) ⋯) : Finset Nat.Primes)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF (↑p : ℕ) ⊨ᵇ ψ
⊢ Set.Finite (α := Nat.Primes) {p : Nat.Primes | ¬Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
have refine : (↑s : Set Nat.Primes)ᶜ ⊆ fun (p : Nat.Primes) ↦
  ∀ (M : (Theory.ACF (↑p : ℕ)).ModelType) (v : Empty → (↑M : Type)) (xs : Fin 0 → (↑M : Type)),
    BoundedFormula.Realize φ v xs
Tactic: refine Set.Finite.subset (Finset.finite_toSet s) (Set.compl_subset_comm.2 ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Field.IsAlgClosed (goal)
Goal:
φ : Language.ring.Sentence
⊢ Theory.ACF 0 ⊨ᵇ φ ↔ Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
have refine : ¬Theory.ACF 0 ⊨ᵇ φ → ¬Set.Infinite (α := Nat.Primes) {p : Nat.Primes | Theory.ACF (↑p : ℕ) ⊨ᵇ φ}
Tactic: refine ⟨fun h => Set.infinite_of_finite_compl
      (finite_ACF_prime_not_realize_of_ACF_zero_realize φ h),
    not_imp_not.1 ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
x : ring.Symbols
⊢ x ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
have inl : ∀ (fst : ℕ) (f : ring.Functions fst),
  Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) fst f) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
Tactic: rcases x with ⟨_, f⟩ | ⟨_, f⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
x : ring.Symbols
inl :
  ∀ (fst : ℕ) (f : ring.Functions fst),
    Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) fst f) ∈
      {
        val :=
          (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
                Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
            Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
        nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
⊢ x ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
have inr : ∀ (fst : ℕ) (f : ring.Relations fst),
  Sum.inr (Sigma.mk (β := fun (l : ℕ) ↦ ring.Relations l) fst f) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
Tactic: rcases x with ⟨_, f⟩ | ⟨_, f⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
fst : ℕ
f : ring.Functions fst
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) fst f) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
have inl : Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add) ∈
  {
    val :=
      (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
        Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
    nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
Tactic: cases f
Cleared hypotheses: fst, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
fst : ℕ
f : ring.Functions fst
inl :
  Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) fst f) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
have inl₁ : Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul) ∈
  {
    val :=
      (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
        Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
    nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
Tactic: cases f
Cleared hypotheses: fst, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
fst : ℕ
f : ring.Functions fst
inl :
  Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
inl₁ :
  Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
⊢ Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) fst f) ∈
    {
      val :=
        (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
              Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
          Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
      nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
have inl₂ : Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg) ∈
  {
    val :=
      (↑[Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 add),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 2 mul),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 1 neg),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero),
            Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 one)] :
        Multiset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l)),
    nodup := instFintypeSymbolsRing._proof_1 : Finset ((l : ℕ) × ring.Functions l ⊕ (l : ℕ) × ring.Relations l) }
Tactic: cases f
Cleared hypotheses: fst, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (hypothesis)
Goal:
⊢ ring.card = 5
have this : Fintype.card ring.Symbols = 5
Tactic: have : Fintype.card Language.ring.Symbols = 5 := rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Functions n
⊢ ∀ (x : Fin n → R), f_1.toFun (funMap f x) = funMap f (f_1.toFun ∘ x)
have add : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) add x) = funMap (L := ring) add (f_1.toFun ∘ x)
Tactic: cases f
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Functions n
add : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.add x) = funMap (L := ring) ringFunc.add (f_1.toFun ∘ x)
⊢ ∀ (x : Fin n → R), f_1.toFun (funMap f x) = funMap f (f_1.toFun ∘ x)
have mul : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) mul x) = funMap (L := ring) mul (f_1.toFun ∘ x)
Tactic: cases f
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Functions n
add : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.add x) = funMap (L := ring) ringFunc.add (f_1.toFun ∘ x)
mul : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.mul x) = funMap (L := ring) ringFunc.mul (f_1.toFun ∘ x)
⊢ ∀ (x : Fin n → R), f_1.toFun (funMap f x) = funMap f (f_1.toFun ∘ x)
have neg : ∀ (x : Fin 1 → R), f_1.toFun (funMap (L := ring) neg x) = funMap (L := ring) neg (f_1.toFun ∘ x)
Tactic: cases f
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Functions n
add : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.add x) = funMap (L := ring) ringFunc.add (f_1.toFun ∘ x)
mul : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.mul x) = funMap (L := ring) ringFunc.mul (f_1.toFun ∘ x)
neg : ∀ (x : Fin 1 → R), f_1.toFun (funMap (L := ring) ringFunc.neg x) = funMap (L := ring) ringFunc.neg (f_1.toFun ∘ x)
⊢ ∀ (x : Fin n → R), f_1.toFun (funMap f x) = funMap f (f_1.toFun ∘ x)
have zero : ∀ (x : Fin 0 → R), f_1.toFun (funMap (L := ring) zero x) = funMap (L := ring) zero (f_1.toFun ∘ x)
Tactic: cases f
Cleared hypotheses: n, f
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.Basic (goal)
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : NonAssocRing R
inst_1 : NonAssocRing S
inst_2 : CompatibleRing R
inst_3 : CompatibleRing S
f_1 : R ≃+* S
n : ℕ
f : ring.Functions n
add : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.add x) = funMap (L := ring) ringFunc.add (f_1.toFun ∘ x)
mul : ∀ (x : Fin 2 → R), f_1.toFun (funMap (L := ring) ringFunc.mul x) = funMap (L := ring) ringFunc.mul (f_1.toFun ∘ x)
neg : ∀ (x : Fin 1 → R), f_1.toFun (funMap (L := ring) ringFunc.neg x) = funMap (L := ring) ringFunc.neg (f_1.toFun ∘ x)
zero :
  ∀ (x : Fin 0 → R), f_1.toFun (funMap (L := ring) ringFunc.zero x) = funMap (L := ring) ringFunc.zero (f_1.toFun ∘ x)
⊢ ∀ (x : Fin n → R), f_1.toFun (funMap f x) = funMap f (f_1.toFun ∘ x)
have one : ∀ (x : Fin 0 → R), f_1.toFun (funMap (L := ring) one x) = funMap (L := ring) one (f_1.toFun ∘ x)
Tactic: cases f
Cleared hypotheses: n, f