-- Module: Mathlib.ModelTheory.Algebra.Ring.Basic
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) }
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) }
inl₃ :
  Sum.inl (Sigma.mk (β := fun (l : ℕ) ↦ ring.Functions l) 0 zero) ∈
    {
      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) 0 one) ∈
    {
      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) }

Tactic:
cases f