mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.EffectiveEpi

Goal state before:
pp: X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (compHausToCondensed.map f)

Tactic:
CondensedSet.epi_iff_locallySurjective_on_compHaus

Goal state after:
X✝ Y✝ : CompHaus
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ∀ (S : CompHaus) (y : (compHausToCondensed.obj Y✝).obj.obj (Opposite.op S)),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom ((compHausToCondensed.map f).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((compHausToCondensed.obj Y✝).obj.map (Opposite.op φ))) y
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
x : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x

Tactic:
;

Goal state after:
S : Profinite
F✝ F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ Profinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
x : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
x : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x

Tactic:
;

Goal state after:
S : LightProfinite
F✝ F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst✝ : Finite ↑X.toTop
x✝¹ : Cofan fun x ↦ LightProfinite.of PUnit.{?u.15 + 1}
x✝ : (fintypeCatAsCofan X).pt ⟶ x✝¹.pt
h : ∀ (j : ↑X.toTop), (fintypeCatAsCofan X).inj j ≫ x✝ = x✝¹.inj j
x : ↑(fintypeCatAsCofan X).pt.toTop
⊢ (ConcreteCategory.hom x✝) x =
    (ConcreteCategory.hom
        (ConcreteCategory.ofHom
          { toFun := fun x ↦ (ConcreteCategory.hom (x✝¹.inj x)) PUnit.unit, continuous_toFun := ⋯ }))
      x
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
have : Finite T := Finite.of_surjective f' f'_surj

Goal state after:
X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
this : Finite T
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont } ≫ f'))
      a✝ =
    (ConcreteCategory.hom g') a✝

Tactic:
;

Goal state after:
X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑Y.toTop
⊢ (ConcreteCategory.hom
        (CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont } ≫ f'))
      a✝ =
    (ConcreteCategory.hom g') a✝
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom
        (f ≫ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont }))
      a✝ =
    (ConcreteCategory.hom g) a✝

Tactic:
;

Goal state after:
X Y S T : Profinite
inst✝² : Finite ↑S.toTop
f : X ⟶ Y
inst✝¹ : Mono f
f' : S ⟶ T
inst✝ : Epi f'
g : X ⟶ S
g' : Y ⟶ T
h_comm : f ≫ g' = g ≫ f'
k_fun : (fun X ↦ ↑X.toTop) Y → (fun X ↦ ↑X.toTop) S
k_cont : Continuous k_fun
h₁ : ⇑(ConcreteCategory.hom f') ∘ k_fun = ⇑(ConcreteCategory.hom g')
h₂ : k_fun ∘ ⇑(ConcreteCategory.hom f) = ⇑(ConcreteCategory.hom g)
a✝ : ↑X.toTop
⊢ (ConcreteCategory.hom
        (f ≫ CompHausLike.ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := k_fun, continuous_toFun := k_cont }))
      a✝ =
    (ConcreteCategory.hom g) a✝
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Tactic:
;

Goal state after:
case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
g : α → F β
f : β → γ
x : t α
⊢ Comp.instApplicativeComp = inst✝¹
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝¹

Tactic:
;

Goal state after:
case e_4
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ : Type u
f : β → F γ
g : α → β
x : t α
⊢ Comp.instApplicativeComp = inst✝¹
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)

Tactic:
;

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x

Tactic:
;

Goal state after:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h' : j < (↑x).succ
⊢ ¬p j

Tactic:
rcases Nat.lt_succ_iff_lt_or_eq.1 h' with (h' | rfl)

Goal state after:
case inl
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
j : ℕ
h'✝ : j < (↑x).succ
h' : j < ↑x
⊢ ¬p j

case inr
p : ℕ → Prop
x : Upto p
h : ¬p ↑x
h' : ↑x < (↑x).succ
⊢ ¬p ↑x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ pure (bimap f✝ f'✝ <$> x✝) = pure (bimap f✝ f'✝ x✝)

Tactic:
;

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ pure (bimap f✝ f'✝ <$> x✝) = pure (bimap f✝ f'✝ x✝)
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    (assert (∃ i, (Fix.approx f i x).Dom) fun h ↦ ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x

Tactic:
;

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    (assert (∃ i, (Fix.approx f i x).Dom) fun h ↦ ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x

Tactic:
;

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) → Nat.find h' = k + ↑z → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x

Tactic:
;

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
⊢ p (k + ↑z) → Nat.find h' = k + ↑z → ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
x✝¹ : Perm α
x✝ : α
⊢ (((Equiv.refl α).symm.trans x✝¹).trans (Equiv.refl α)) x✝ = (id x✝¹) x✝

Tactic:
;

Goal state after:
α : Type ?u.3
x✝¹ : Perm α
x✝ : α
⊢ (((Equiv.refl α).symm.trans x✝¹).trans (Equiv.refl α)) x✝ = (id x✝¹) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.3
x✝³ : α✝ ≃ β✝
x✝² : β✝ ≃ γ✝
x✝¹ : Perm α✝
x✝ : γ✝
⊢ (((x✝³.trans x✝²).symm.trans x✝¹).trans (x✝³.trans x✝²)) x✝ =
    (((fun p ↦ (x✝².symm.trans p).trans x✝²) ∘ fun p ↦ (x✝³.symm.trans p).trans x✝³) x✝¹) x✝

Tactic:
;

Goal state after:
α✝ β✝ γ✝ : Type ?u.3
x✝³ : α✝ ≃ β✝
x✝² : β✝ ≃ γ✝
x✝¹ : Perm α✝
x✝ : γ✝
⊢ (((x✝³.trans x✝²).symm.trans x✝¹).trans (x✝³.trans x✝²)) x✝ =
    (((fun p ↦ (x✝².symm.trans p).trans x✝²) ∘ fun p ↦ (x✝³.symm.trans p).trans x✝³) x✝¹) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ Finset.map (Equiv.refl α).toEmbedding x✝ ↔ a✝ ∈ id x✝

Tactic:
;

Goal state after:
α : Type ?u.4
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ Finset.map (Equiv.refl α).toEmbedding x✝ ↔ a✝ ∈ id x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.4
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
⊢ a✝ ∈ Finset.map (k.trans h).toEmbedding x✝ ↔
    a✝ ∈ ((fun s ↦ Finset.map h.toEmbedding s) ∘ fun s ↦ Finset.map k.toEmbedding s) x✝

Tactic:
;

Goal state after:
α✝ β✝ γ✝ : Type ?u.4
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
⊢ a✝ ∈ Finset.map (k.trans h).toEmbedding x✝ ↔
    a✝ ∈ ((fun s ↦ Finset.map h.toEmbedding s) ∘ fun s ↦ Finset.map k.toEmbedding s) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
x✝ : Fintype α
⊢ Fintype.ofBijective ⇑(Equiv.refl α) ⋯ = id x✝

Tactic:
;

Goal state after:
α : Type ?u.4
x✝ : Fintype α
⊢ Fintype.ofBijective ⇑(Equiv.refl α) ⋯ = id x✝
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (fun a ↦ (Function.comp fun x2 ↦ a :: x2) ∘ fun x1 x2 ↦ x1 ++ x2) <$> f a <*> traverse f as <*> traverse f bs =
    (fun a ↦ (fun x1 x2 ↦ x1 ++ x2) ∘ fun x2 ↦ a :: x2) <$> f a <*> traverse f as <*> traverse f bs

Tactic:
;

Goal state after:
F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ (fun a ↦ (Function.comp fun x2 ↦ a :: x2) ∘ fun x1 x2 ↦ x1 ++ x2) <$> f a <*> traverse f as <*> traverse f bs =
    (fun a ↦ (fun x1 x2 ↦ x1 ++ x2) ∘ fun x2 ↦ a :: x2) <$> f a <*> traverse f as <*> traverse f bs
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝ y✝ : FreeMonoid α
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝ * y✝)) =
    flip (List.foldrM f) (FreeMonoid.toList x✝) * flip (List.foldrM f) (FreeMonoid.toList y✝)

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝ y✝ : FreeMonoid α
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝ * y✝)) =
    flip (List.foldrM f) (FreeMonoid.toList x✝) * flip (List.foldrM f) (FreeMonoid.toList y✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝¹ * y✝)) x✝ =
    (flip (List.foldrM f) (FreeMonoid.toList x✝¹) * flip (List.foldrM f) (FreeMonoid.toList y✝)) x✝

Tactic:
;

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝¹ y✝ : FreeMonoid α
x✝ : KleisliCat.mk m β
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝¹ * y✝)) x✝ =
    (flip (List.foldrM f) (FreeMonoid.toList x✝¹) * flip (List.foldrM f) (FreeMonoid.toList y✝)) x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ : Type ?u.17
x✝ : α✝
⊢ f (pure x✝) = pure x✝

Tactic:
;

Goal state after:
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ : Type ?u.17
x✝ : α✝
⊢ f (pure x✝) = pure x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ β✝ : Type ?u.17
x✝ : Const α (α✝ → β✝)
y✝ : Const α α✝
⊢ f (x✝ <*> y✝) = f x✝ <*> f y✝

Tactic:
;

Goal state after:
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ β✝ : Type ?u.17
x✝ : Const α (α✝ → β✝)
y✝ : Const α α✝
⊢ f (x✝ <*> y✝) = f x✝ <*> f y✝
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (⇑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip f) x

Tactic:
simp only [foldlM.ofFreeMonoid, Function.flip_def, MonoidHom.coe_mk, OneHom.coe_mk,
    Function.comp_apply, FreeMonoid.toList_of, List.foldlM_cons, List.foldlM_nil, bind_pure,
    foldlM.mk, op_inj]

Goal state after:
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : β
⊢ (fun a ↦ f a x) = fun a ↦ f a x
Module: Mathlib.Control.Fold

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)

Tactic:
;

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = (foldrM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x

Tactic:
simp only [foldrm, toList_spec, foldMap_hom_free (foldrM.ofFreeMonoid f),
    foldrm.ofFreeMonoid_comp_of, foldrM.get, FreeMonoid.ofList_toList]

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.PredLast pp p_1 }) i.fs
⊢ True = ofRepeat (α.PredLast' pp i.fs ↑x)

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.PredLast pp p_1 }) i.fs
⊢ True = ofRepeat (α.PredLast' pp i.fs ↑x)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }) i.fs
⊢ ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2)) = ((↑x).1 = (↑x).2)

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }) i.fs
⊢ ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2)) = ((↑x).1 = (↑x).2)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ ((↑x).1 = (↑x).2) = ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2))

Tactic:
;

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ ((↑x).1 = (↑x).2) = ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2))
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ f ⊥

Tactic:
;

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ f ⊥
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) (n✝ + 1) i✝ ≤ approx (⇑f) (n✝ + 1).succ i✝

Tactic:
;

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) (n✝ + 1) i✝ ≤ approx (⇑f) (n✝ + 1).succ i✝
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) n✝ ≤ approx (⇑f) (n✝ + 1)

Tactic:
;

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) n✝ ≤ approx (⇑f) (n✝ + 1)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) 0

Tactic:
;

Goal state after:
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (⇑f) 0 ≤ approx (⇑f) 0
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)

pp: case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
;

Goal state after:
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)

case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ (id <$> x✝).run = x✝.run

Tactic:
;

Goal state after:
M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ (id <$> x✝).run = x✝.run
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝
x✝ : α✝ → WriterT ω M β✝
⊢ (pure x✝¹ >>= x✝).run = (x✝ x✝¹).run

Tactic:
;

Goal state after:
M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝
x✝ : α✝ → WriterT ω M β✝
⊢ (pure x✝¹ >>= x✝).run = (x✝ x✝¹).run