mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
⊢ g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
⊢ traverse pure = pure

Tactic:
by

Goal state after:
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
g : α → F β
h : β → G γ
⊢ traverse (Comp.mk ∘ map h ∘ g) = Comp.mk ∘ map (traverse h) ∘ traverse g

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
β γ : Type u
f : β → γ
⊢ traverse (pure ∘ f) = pure ∘ map f

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → β
h : β → G γ
⊢ traverse (h ∘ g) = traverse h ∘ map g

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
g : α → G β
h : β → γ
⊢ traverse (map h ∘ g) = map (map h) ∘ traverse g

Tactic:
by

Goal state after:
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
η : ApplicativeTransformation F G
f : α → F β
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) = (fun {α} ↦ η.app α) ∘ traverse f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := fun n ↦ { k // f ≫ k = g ≫ lightToProfinite.map (S.proj n) }
next : (n : ℕ) → lifts n → lifts (n + 1) := fun n k ↦ ⟨⋯.choose, ⋯⟩
k_seq : (n : ℕ) → lifts n := fun n ↦ Nat.rec ⟨k0, h_down0⟩ next n
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := { pt := Y, π := NatTrans.ofOpSequence (fun n ↦ ↑(k_seq n)) ⋯ }
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
⊢ f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone =
    (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)

Tactic:
apply (isLimitOfPreserves _ S.asLimit).uniq (k_cone.extend f)

Goal state after:
S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
this✝¹ : ∀ (n : ℕ), Finite ↑(lightToProfinite.obj (S.component n)).toTop
this✝ : Nonempty ↑(lightToProfinite.obj (S.component 0)).toTop
this : ∀ (n : ℕ), Epi (S.transitionMap n)
k0 : Y ⟶ lightToProfinite.obj (S.diagram.obj (Opposite.op 0))
h_down0 : f ≫ k0 = g ≫ lightToProfinite.map (S.proj 0)
h_comm :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      f ≫ k = g ≫ lightToProfinite.map (S.proj (n + 1)) ≫ lightToProfinite.map (S.transitionMap n)
h_step :
  ∀ (n : ℕ) (k : Y ⟶ lightToProfinite.obj (S.component n)),
    f ≫ k = g ≫ lightToProfinite.map (S.proj n) →
      ∃ k', k' ≫ lightToProfinite.map (S.transitionMap n) = k ∧ f ≫ k' = g ≫ lightToProfinite.map (S.proj (n + 1))
lifts : ℕ → Type (max 0 u) := ⋯
next : (n : ℕ) → lifts n → lifts (n + 1) := ⋯
k_seq : (n : ℕ) → lifts n := ⋯
h_down : ∀ (n : ℕ), f ≫ ↑(k_seq n) = g ≫ lightToProfinite.map (S.proj n)
h_up : ∀ (n : ℕ), ↑(k_seq (n + 1)) ≫ lightToProfinite.map (S.transitionMap n) = ↑(k_seq n)
k_cone : Cone (S.diagram ⋙ lightToProfinite) := ⋯
hg : g = (isLimitOfPreserves lightToProfinite S.asLimit).lift (k_cone.extend f)
⊢ ∀ (j : ℕᵒᵖ),
    (f ≫ (isLimitOfPreserves lightToProfinite S.asLimit).lift k_cone) ≫
        (lightToProfinite.mapCone S.asLimitCone).π.app j =
      (k_cone.extend f).π.app j
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Prod

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ InternallyProjective ((free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (P ⊗ S).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (P ◁ π)) ≫ g = g' ≫ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : Profinite
g : X ⟶ lightToProfinite.obj S
f : X ⟶ Y
h : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: S : LightProfinite
inst✝ : Nonempty ↑S.toTop
X Y : LightProfinite
g : X ⟶ S
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
by

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Sum

Tactic:
by

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝¹ : Bitraversable t
F : Type u → Type u
inst✝ : Applicative F
⊢ LawfulBitraversable Const

Tactic:
by

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (_root_.flip t)

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ InternallyProjective ((free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e

Tactic:
by

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ LawfulTraversable (t α)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
this : Upto.GT p = InvImage (fun x1 x2 ↦ x1 < x2) fun y ↦ x - ↑y
⊢ WellFounded (Upto.GT p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Upto

Goal state before:
pp: p : ℕ → Prop
x : ℕ
h : p x
⊢ WellFounded (Upto.GT p)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompl t F G)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
⊢ ⇑(Equiv.refl α).uniqueCongr = id

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: ⊢ ∀ {α β γ : Type ?u.3} (k : α ≃ β) (h : β ≃ γ), ⇑(k.trans h).uniqueCongr = ⇑h.uniqueCongr ∘ ⇑k.uniqueCongr

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
⊢ (fun p ↦ ((Equiv.refl α).symm.trans p).trans (Equiv.refl α)) = id

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

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

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
⊢ (fun s ↦ Finset.map (Equiv.refl α).toEmbedding s) = id

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

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

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

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

Tactic:
by

Goal state after:
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: ⊢ ∀ {α β γ : Type ?u.4} (k : α ≃ β) (h : β ≃ γ),
    (fun x ↦ Fintype.ofBijective ⇑(k.trans h) ⋯) = (fun x ↦ Fintype.ofBijective ⇑h ⋯) ∘ fun x ↦ Fintype.ofBijective ⇑k ⋯

Tactic:
by

Goal state after:
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
n : ℕ
n_ih :
  ∀ (z : Upto p),
    p (n + ↑z) →
      Nat.find h' = n + ↑z →
        ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f n.succ x'
z : Upto p
_this : p (n + 1 + ↑z)
hk : Nat.find h' = n + 1 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x✝ : α
⊢ ¬(Fix.approx f (↑z) x).Dom

Tactic:
by

Goal state after:
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
⊢ Part.fix f x = Fix.approx f (Nat.find h').succ x

Tactic:
by

Goal state after:
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
⊢ Part.fix f x = none

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α : Type u_1
x : Option α
⊢ Option.traverse pure x = pure x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : Option α
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (Option.traverse f <$> Option.traverse g x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α β : Type u_1
f : α → β
x : Option α
⊢ Option.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
η : ApplicativeTransformation F G
inst✝ : LawfulApplicative F
α : Type u_1
β : Type u
f : α → F β
x : Option α
⊢ (fun {α} ↦ η.app α) (Option.traverse f x) = Option.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α : Type u_1
xs : List α
⊢ List.traverse pure xs = pure xs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α β : Type u_1
f : α → β
x : List α
⊢ List.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : List α
⊢ (fun {α} ↦ η.app α) (List.traverse f x) = List.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

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

Tactic:
by

Goal state after:
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 α'
⊢ traverse f (a :: as ++ bs) = (fun x1 x2 ↦ x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
⊢ [] ∈ traverse f [] ↔ Forall₂ (fun b a ↦ b ∈ f a) [] []

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
⊢ [] ∈ traverse f (a :: as) ↔ Forall₂ (fun b a ↦ b ∈ f a) [] (a :: as)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f [] ↔ Forall₂ (fun b a ↦ b ∈ f a) (b :: bs) []

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: α' β' : Type u
f : α' → Set β'
a : α'
as : List α'
b : β'
bs : List β'
⊢ b :: bs ∈ traverse f (a :: as) ↔ Forall₂ (fun b a ↦ b ∈ f a) (b :: bs) (a :: as)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
G : Type u → Type u
inst✝ : Applicative G
α β γ : Type u
g : α → β
f : β → G γ
x : σ ⊕ α
⊢ Sum.traverse f (g <$> x) = Sum.traverse (f ∘ g) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : σ ⊕ α
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) x = Comp.mk (Sum.traverse f <$> Sum.traverse g x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
G : Type u → Type u
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
g : α → G β
f : β → γ
x : σ ⊕ α
⊢ (fun x ↦ f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x ↦ f <$> g x) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: σ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α : Type u_1
β : Type u
f : α → F β
x : σ ⊕ α
⊢ (fun {α} ↦ η.app α) (Sum.traverse f x) = Sum.traverse ((fun {α} ↦ η.app α) ∘ f) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
⊢ ∀ (x y : FreeMonoid α),
    op (↾flip (List.foldl f) (FreeMonoid.toList (x * y))) =
      op (↾flip (List.foldl f) (FreeMonoid.toList x)) * op (↾flip (List.foldl f) (FreeMonoid.toList y))

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

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

Tactic:
by

Goal state after:
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 α),
    op (flip (List.foldlM f) (FreeMonoid.toList (x * y))) =
      op (flip (List.foldlM f) (FreeMonoid.toList x)) * op (flip (List.foldlM f) (FreeMonoid.toList y))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
⊢ last.rev = fz

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ i.castSucc.rev = i.rev.fs

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ i.rev.rev = i

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∉ Finset.map { toFun := fs, inj' := ⋯ } elems

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ ∀ (x : Fin2 (n + 1)), x ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ofFin i.toFin = i

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

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

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

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

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

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

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ FreeMonoid.toList (foldMap FreeMonoid.of xs) = FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ FreeMonoid.toList (foldMap FreeMonoid.of xs).reverse.reverse =
    (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ (List.foldr cons [] (FreeMonoid.toList (foldMap FreeMonoid.of xs)).reverse).reverse =
    ((ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)))) []).reverse

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ ((ConcreteCategory.hom (unop ((Foldl.ofFreeMonoid (flip cons)) (foldMap FreeMonoid.of xs)))) []).reverse = toList xs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝² : Traversable t
inst✝¹ : LawfulTraversable t
inst✝ : Monoid γ
f : α → β
g : β → γ
xs : t α
⊢ foldMap g (f <$> xs) = foldMap (g ∘ f) xs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → α
xs : t β
x : α
⊢ foldl f x xs = List.foldl f x (toList xs)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)

Tactic:
change _ = (Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs)).hom _
  rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
    foldr.ofFreeMonoid_comp_of]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)

Tactic:
by

Goal state after: