-- 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) }
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) }
⊢ 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) 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) }
Tactic: cases f
Cleared hypotheses: fst, f