mathlib

1a393e7a - feat(tactic/explode): support exploding "let" expressions and improve handling of "have" expressions (#3632)

feat(tactic/explode): support exploding "let" expressions and improve handling of "have" expressions (#3632) The current #explode has little effect on proofs using "let" expressions, e.g., #explode nat.exists_infinite_primes. #explode also occasionally ignores certain dependencies due to macros occurring in "have" expressions. See examples below. This PR fixes these issues. theorem foo {p q : Prop}: p → p := λ hp, have hh : p, from hp, hh #explode foo -- missing dependencies at forall introduction theorem bar {p q : Prop}: p → p := λ hp, (λ (hh : p), hh) hp #explode bar -- expected behavior