tests/elab/simpPreprocess.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            theorem ex (p q r : Prop) (h : p ∧ q ∧ r) : (¬q ∨ r) ∧ (¬r ∨ q) ∧ p := by

            
              simp [h]


            #print ex
	theorem ex (p q r : Prop) (h : p ∧ q ∧ r) : (¬q ∨ r) ∧ (¬r ∨ q) ∧ p := by
	simp [h]

	#print ex