Theorem: forall_const_and_distrib (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Tactic:
have d := @forall_and A (fun _ ↦ p) q
State after:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ (A → p) ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x

State before:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ (A → p) ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Tactic:
simp only [forall_const] at d
State after:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x

State before:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
A : Type
inst✝ : Nonempty A
p : Prop
q : A → Prop
d : (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
⊢ (∀ (x : A), p ∧ q x) ↔ p ∧ ∀ (x : A), q x
Tactic:
exact d
State after:
no goals