Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: case addAssoc
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ addAssoc.toSentence ↔ toProp K addAssoc

pp: case zeroAdd
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ zeroAdd.toSentence ↔ toProp K zeroAdd

pp: case negAddCancel
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ negAddCancel.toSentence ↔ toProp K negAddCancel

pp: case mulAssoc
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ mulAssoc.toSentence ↔ toProp K mulAssoc

pp: case mulComm
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ mulComm.toSentence ↔ toProp K mulComm

pp: case oneMul
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ oneMul.toSentence ↔ toProp K oneMul

pp: case existsInv
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ existsInv.toSentence ↔ toProp K existsInv

pp: case leftDistrib
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ leftDistrib.toSentence ↔ toProp K leftDistrib

pp: case existsPairNE
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ existsPairNE.toSentence ↔ toProp K existsPairNE

Tactic:
<;>

Goal state after:
case addAssoc
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ addAssoc.toSentence ↔ toProp K addAssoc

case zeroAdd
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ zeroAdd.toSentence ↔ toProp K zeroAdd

case negAddCancel
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ negAddCancel.toSentence ↔ toProp K negAddCancel

case mulAssoc
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ mulAssoc.toSentence ↔ toProp K mulAssoc

case mulComm
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ mulComm.toSentence ↔ toProp K mulComm

case oneMul
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ oneMul.toSentence ↔ toProp K oneMul

case existsInv
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ existsInv.toSentence ↔ toProp K existsInv

case leftDistrib
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ leftDistrib.toSentence ↔ toProp K leftDistrib

case existsPairNE
K : Type u_2
inst✝⁵ : Add K
inst✝⁴ : Mul K
inst✝³ : Neg K
inst✝² : Zero K
inst✝¹ : One K
inst✝ : CompatibleRing K
⊢ K ⊨ existsPairNE.toSentence ↔ toProp K existsPairNE