mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∩ G.F.f t,
        pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
G : g.Realizer
σ✝ : Type ?u.88
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝, F := F✝, eq := eq✝ }.F.f s ∩ G.F.f t,
        pt := ({ σ := σ✝, F := F✝, eq := eq✝ }.F.pt, G.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝, F := F✝, eq := eq✝ }.F.inf a b, G.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : F✝¹.toFilter = f
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = g
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.f s ∩ { σ := σ✝, F := F✝, eq := eq✝ }.F.f t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.inf a b, { σ := σ✝, F := F✝, eq := eq✝ }.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
eq✝¹ : F✝¹.toFilter = f
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = g
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.f s ∩ { σ := σ✝, F := F✝, eq := eq✝ }.F.f t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.pt, { σ := σ✝, F := F✝, eq := eq✝ }.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := eq✝¹ }.F.inf a b, { σ := σ✝, F := F✝, eq := eq✝ }.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    f ⊓ g
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.f s ∩ { σ := σ✝, F := F✝, eq := ⋯ }.F.f t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.pt, { σ := σ✝, F := F✝, eq := ⋯ }.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.inf a b, { σ := σ✝, F := F✝, eq := ⋯ }.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    F✝¹.toFilter ⊓ F✝.toFilter

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ {
        f := fun x ↦
          match x with
          | (s, t) => { σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.f s ∩ { σ := σ✝, F := F✝, eq := ⋯ }.F.f t,
        pt := ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.pt, { σ := σ✝, F := F✝, eq := ⋯ }.F.pt),
        inf := fun x x_1 ↦
          match x with
          | (a, a') =>
            match x_1 with
            | (b, b') => ({ σ := σ✝¹, F := F✝¹, eq := ⋯ }.F.inf a b, { σ := σ✝, F := F✝, eq := ⋯ }.F.inf a' b'),
        inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter =
    F✝¹.toFilter ⊓ F✝.toFilter
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
      { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
⊢ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    { sets := {a | ∃ b, F✝¹.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } ⊓
      { sets := {a | ∃ b, F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }.F.f s = F.F.f (E.symm s)

Tactic:
;

Goal state after:
α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ { σ := τ, F := Ctop.ofEquiv E F.F, eq := ⋯ }.F.f s = F.F.f (E.symm s)
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
n : ↑ℕ∪{∞}.toTop
⊢ Continuous Subtype.val

Tactic:
;

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
n : ↑ℕ∪{∞}.toTop
⊢ Continuous Subtype.val
Module: Mathlib.Data.DFinsupp.FiniteInfinite

Goal state before:
pp: ι✝ : Type u
γ : Type w
β : ι✝ → Type v
β₁ : ι✝ → Type v₁
β₂ : ι✝ → Type v₂
ι : Type u_1
π : ι → Type u_2
inst✝² : ∀ (i : ι), Nontrivial (π i)
inst✝¹ : (i : ι) → Zero (π i)
inst✝ : Infinite ι
this : DecidableEq ι := Classical.decEq ι
⊢ Infinite (Π₀ (i : ι), π i)

Tactic:
;

Goal state after:
ι✝ : Type u
γ : Type w
β : ι✝ → Type v
β₁ : ι✝ → Type v₁
β₂ : ι✝ → Type v₂
ι : Type u_1
π : ι → Type u_2
inst✝² : ∀ (i : ι), Nontrivial (π i)
inst✝¹ : (i : ι) → Zero (π i)
inst✝ : Infinite ι
this : DecidableEq ι := Classical.decEq ι
⊢ Infinite (Π₀ (i : ι), π i)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
G : (i : α) → (m i).Realizer
x✝ : Set β
σ✝ : Type ?u.147
F : CFilter (Set α) σ✝
eq✝ : F.toFilter = f
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ { σ := σ✝, F := F, eq := eq✝ }.F.f s), (G i).F.f (f_1 i h),
            pt := ⟨{ σ := σ✝, F := F, eq := eq✝ }.F.pt, fun i x ↦ (G i).F.pt⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨a, f_1⟩ =>
                match x_1 with
                | ⟨b, f'⟩ => ⟨{ σ := σ✝, F := F, eq := eq✝ }.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f.bind m).sets

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
G : (i : α) → (m i).Realizer
x✝ : Set β
σ✝ : Type ?u.147
F : CFilter (Set α) σ✝
eq✝ : F.toFilter = f
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ { σ := σ✝, F := F, eq := eq✝ }.F.f s), (G i).F.f (f_1 i h),
            pt := ⟨{ σ := σ✝, F := F, eq := eq✝ }.F.pt, fun i x ↦ (G i).F.pt⟩,
            inf := fun x x_1 ↦
              match x with
              | ⟨a, f_1⟩ =>
                match x_1 with
                | ⟨b, f'⟩ => ⟨{ σ := σ✝, F := F, eq := eq✝ }.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩,
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f.bind m).sets
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ a✝ : α
⊢ count a✝ ((DFinsupp.toMultiset.comp toDFinsupp) {x✝}) = count a✝ ((AddMonoidHom.id (Multiset α)) {x✝})

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ a✝ : α
⊢ count a✝ ((DFinsupp.toMultiset.comp toDFinsupp) {x✝}) = count a✝ ((AddMonoidHom.id (Multiset α)) {x✝})
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ i✝ : α
⊢ (((toDFinsupp.comp DFinsupp.toMultiset).comp (DFinsupp.singleAddHom (fun i ↦ ℕ) x✝)) 1) i✝ =
    (((AddMonoidHom.id (Π₀ (x : α), ℕ)).comp (DFinsupp.singleAddHom (fun i ↦ ℕ) x✝)) 1) i✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ i✝ : α
⊢ (((toDFinsupp.comp DFinsupp.toMultiset).comp (DFinsupp.singleAddHom (fun i ↦ ℕ) x✝)) 1) i✝ =
    (((AddMonoidHom.id (Π₀ (x : α), ℕ)).comp (DFinsupp.singleAddHom (fun i ↦ ℕ) x✝)) 1) i✝
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(uIcc f g) = ∏ i ∈ (f ⊓ g).support ∪ (f ⊔ g).support, #(uIcc (f i) (g i))
Module: Mathlib.Data.DFinsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∪ t)) i = (toDFinsupp s ⊔ toDFinsupp t) i
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
a : α
h : ∃ a_1, (fun x ↦ a_1 = x) = ↑(mk a) := (mk a).property
⊢ (mk a).out = a

Tactic:
;

Goal state after:
α : Sort u_1
a : α
h : ∃ a_1, (fun x ↦ a_1 = x) = ↑(mk a) := (mk a).property
⊢ (mk a).out = a
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ ⟨fun b ↦ out ⟨s, h⟩ = b, ⋯⟩ = ⟨s, h⟩

Tactic:
;

Goal state after:
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ ⟨fun b ↦ out ⟨s, h⟩ = b, ⋯⟩ = ⟨s, h⟩
Module: Mathlib.Data.Erased

Goal state before:
pp: α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ (fun b ↦ out ⟨s, h⟩ = b) = s

Tactic:
;

Goal state after:
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x ↦ a = x) = s
⊢ (fun b ↦ out ⟨s, h⟩ = b) = s
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝¹ : α✝
x✝ : Erased β✝
⊢ (Functor.mapConst x✝¹ x✝).out = ((Functor.map ∘ Function.const β✝) x✝¹ x✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝¹ : α✝
x✝ : Erased β✝
⊢ (Functor.mapConst x✝¹ x✝).out = ((Functor.map ∘ Function.const β✝) x✝¹ x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ : Type u_1
x✝ : Erased α✝
⊢ id <$> x✝ = x✝

Tactic:
;

Goal state after:
α✝ : Type u_1
x✝ : Erased α✝
⊢ id <$> x✝ = x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ : Type u_1
x✝ : Erased α✝
⊢ (id <$> x✝).out = x✝.out

Tactic:
;

Goal state after:
α✝ : Type u_1
x✝ : Erased α✝
⊢ (id <$> x✝).out = x✝.out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ <* y✝ = Function.const β✝ <$> x✝ <*> y✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ <* y✝ = Function.const β✝ <$> x✝ <*> y✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ <* y✝).out = (Function.const β✝ <$> x✝ <*> y✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ <* y✝).out = (Function.const β✝ <$> x✝ <*> y✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ *> y✝).out = (Function.const α✝ id <$> x✝ <*> y✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ *> y✝).out = (Function.const α✝ id <$> x✝ <*> y✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ pure g✝ <*> x✝ = g✝ <$> x✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ pure g✝ <*> x✝ = g✝ <$> x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (pure g✝ <*> x✝).out = (g✝ <$> x✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (pure g✝ <*> x✝).out = (g✝ <$> x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
        let a ← x✝
        pure (f✝ a)).out =
    (f✝ <$> x✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
        let a ← x✝
        pure (f✝ a)).out =
    (f✝ <$> x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    f✝ <*> x✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    f✝ <*> x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
        let x ← f✝
        x <$> x✝).out =
    (f✝ <*> x✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
        let x ← f✝
        x <$> x✝).out =
    (f✝ <*> x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ pure x✝ >>= f✝ = f✝ x✝

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ (pure x✝ >>= f✝).out = (f✝ x✝).out

Tactic:
;

Goal state after:
α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ (pure x✝ >>= f✝).out = (f✝ x✝).out
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
;

Goal state after:
α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ (x✝ >>= f✝ >>= g✝).out = (x✝ >>= fun x ↦ f✝ x >>= g✝).out

Tactic:
;

Goal state after:
α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ (x✝ >>= f✝ >>= g✝).out = (x✝ >>= fun x ↦ f✝ x >>= g✝).out
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂

Tactic:
;

Goal state after:
α : Type u_1
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }

Tactic:
;

Goal state after:
α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ q.blur' ⋯ = q.blur' h

Tactic:
;

Goal state after:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ q.blur' ⋯ = q.blur' h
Module: Mathlib.Data.Semiquot

Goal state before:
pp: case e_s
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s

Tactic:
;

Goal state after:
case e_s
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a
Module: Mathlib.Data.Fin.FlagRange

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
⊢ ∃ y, f y = x

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
⊢ ∃ y, f y = x
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b
⊢ (mk aq).liftOn f h✝ = f a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b
⊢ (mk aq).liftOn f h✝ = f a
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a, ∃ (_ : a ∈ q), b ∈ f a

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a, ∃ (_ : a ∈ q), b ∈ f a
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin

Tactic:
;

Goal state after:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q

Tactic:
;

Goal state after:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q

Tactic:
;

Goal state after:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin

Tactic:
;

Goal state after:
C : FloatCfg
e : ℤ
m : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
m' : ℕ := m.succ
ss : m'.size = m.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m.size - ↑prec) emin
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m' : ℕ
v : ValidFinite e m'.succ
ss : m'.size = m'.succ.size
⊢ ValidFinite e m'

Tactic:
;

Goal state after:
C : FloatCfg
e : ℤ
m' : ℕ
v : ValidFinite e m'.succ
ss : m'.size = m'.succ.size
⊢ ValidFinite e m'
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin

Tactic:
;

Goal state after:
C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.size - ↑prec) emin
Module: Mathlib.Data.Semiquot

Goal state before:
pp: α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ pure (t.get h) ≤ pure (s.get ⋯)

Tactic:
;

Goal state after:
α : Type u_1
s t : Semiquot α
h : t.IsPure
st : s ≤ t
⊢ pure (t.get h) ≤ pure (s.get ⋯)
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin

Tactic:
;

Goal state after:
C : FloatCfg
e : ℤ
m' : ℕ
v : emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
ss : m'.size = m'.succ.size
⊢ emin ≤ e + ↑prec - 1 ∧ e + ↑prec - 1 ≤ ↑emax ∧ e = max (e + ↑m'.succ.size - ↑prec) emin
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ 1 = j

Tactic:
;

Goal state after:
case pos
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hi : ¬i = 0
hj : j = 0
hij : b = a
⊢ 1 = j
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take 0 ⋯ v i = i.elim0

Tactic:
;

Goal state after:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin 0
⊢ take 0 ⋯ v i = i.elim0
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ ↑i = ↑0

Tactic:
;

Goal state after:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
h : 0 < n
i : Fin (Nat.succ 0)
⊢ ↑i = ↑0
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ v (castLE h (last (m + 1))) = v ⟨m + 1, h⟩

Tactic:
;

Goal state after:
case succ.last
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
m : ℕ
a✝ : ∀ (h : m < n) (i : Fin m.succ), take m.succ h v i = snoc (take m ⋯ v) (v ⟨m, h⟩) i
h : m + 1 < n
⊢ v (castLE h (last (m + 1))) = v ⟨m + 1, h⟩