hello! good work on the website! great idea.
for the And introduction problem, the provided solution uses the And.intro constructor, understandably so:
theorem and_intro (p : Prop) (q : Prop) (hp : p) (hq : q) : p ∧ q := And.intro hp hq
however, the main box submission disallows using the constructor, both by name and by pattern (in refine and exact statements), meaning that pulling this solution directly in results in an unsolved problem, which feels weird. Is this intended?
hello! good work on the website! great idea.
for the And introduction problem, the provided solution uses the And.intro constructor, understandably so:
however, the main box submission disallows using the constructor, both by name and by pattern (in
refineandexactstatements), meaning that pulling this solution directly in results in an unsolved problem, which feels weird. Is this intended?