-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem seq [Applicative m] [LawfulApplicative m] {x : m α}
    (hf : SatisfiesM p₁ f) (hx : SatisfiesM p₂ x)
    (H : ∀ {f a}, p₁ f → p₂ a → q (f a)) : SatisfiesM q (f <*> x)

Proof state:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ pure Subtype.val <*> ((pure fun x x_1 => ⟨x.val x_1.val, ⋯⟩) <*> f <*> x) =
    pure Subtype.val <*> f <*> (pure Subtype.val <*> x)

Tactic:
simp [SatisfiesM, seq_assoc]

Result:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ pure (Function.comp Subtype.val ∘ fun x x_1 => ⟨x.val x_1.val, ⋯⟩) <*> f <*> x =
    (fun a => a ∘ Subtype.val) <$> (pure Subtype.val <*> f) <*> x

Proof state:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x : m α
hf : SatisfiesM p₁ f
hx : SatisfiesM p₂ x
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
⊢ SatisfiesM q (f <*> x)

Tactic:
match f, x, hf, hx with | _, _, ⟨f, rfl⟩, ⟨x, rfl⟩ => ?_

Result:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ SatisfiesM q (Subtype.val <$> f <*> Subtype.val <$> x)

Proof state:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ Subtype.val <$>
      ((fun x x_1 =>
            match x with
            | ⟨a, h₁⟩ =>
              match x_1 with
              | ⟨b, h₂⟩ => ⟨a b, ⋯⟩) <$>
          f <*>
        x) =
    Subtype.val <$> f <*> Subtype.val <$> x

Tactic:
simp only [← pure_seq]

Result:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ pure Subtype.val <*> ((pure fun x x_1 => ⟨x.val x_1.val, ⋯⟩) <*> f <*> x) =
    pure Subtype.val <*> f <*> (pure Subtype.val <*> x)

Proof state:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ SatisfiesM q (Subtype.val <$> f <*> Subtype.val <$> x)

Tactic:
refine ⟨(fun ⟨a, h₁⟩ ⟨b, h₂⟩ => ⟨a b, H h₁ h₂⟩) <$> f <*> x, ?_⟩

Result:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ Subtype.val <$>
      ((fun x x_1 =>
            match x with
            | ⟨a, h₁⟩ =>
              match x_1 with
              | ⟨b, h₂⟩ => ⟨a b, ⋯⟩) <$>
          f <*>
        x) =
    Subtype.val <$> f <*> Subtype.val <$> x

Proof state:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ pure (Function.comp Subtype.val ∘ fun x x_1 => ⟨x.val x_1.val, ⋯⟩) <*> f <*> x =
    (pure fun a => a ∘ Subtype.val) <*> (pure Subtype.val <*> f) <*> x

Tactic:
simp [seq_assoc, Function.comp_def]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ pure (Function.comp Subtype.val ∘ fun x x_1 => ⟨x.val x_1.val, ⋯⟩) <*> f <*> x =
    (fun a => a ∘ Subtype.val) <$> (pure Subtype.val <*> f) <*> x

Tactic:
simp only [← pure_seq]

Result:
m : Type u_1 → Type u_2
α α✝ : Type u_1
p₁ : (α → α✝) → Prop
f✝ : m (α → α✝)
p₂ : α → Prop
q : α✝ → Prop
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
x✝ : m α
hf : SatisfiesM p₁ f✝
hx : SatisfiesM p₂ x✝
H : ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
f : m { a // p₁ a }
x : m { a // p₂ a }
⊢ pure (Function.comp Subtype.val ∘ fun x x_1 => ⟨x.val x_1.val, ⋯⟩) <*> f <*> x =
    (pure fun a => a ∘ Subtype.val) <*> (pure Subtype.val <*> f) <*> x