mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
inst✝ : TotallyDisconnectedSpace X
⊢ IsTopologicalBasis {s | IsClopen s}

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.2
  intro x U hxU U_op
  have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU
  rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩
  use V
  tauto

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case mp
X Y : Profinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : Profinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z := ofHom (fun X ↦ TotallyDisconnectedSpace ↑X) { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := 0 }.down
⊢ False

Tactic:
exact top_ne_bot H

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case cons₂
ns : List ℕ
k : Cont
IH :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepRet k v) b₂ ∧
        Reaches₁ (TM2.step tr) { l := some (Λ'.ret (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
          b₂
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (Λ'.ret (trCont (Cont.cons₂ ns k))), var := s,
          stk := elim (trList v) [] [] (trContStack (Cont.cons₂ ns k)) }
        b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none
    exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V

Tactic:
have := hU.1.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU

Goal state after:
case refine_3
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set ↑C.pt.toTop
hC : IsLimit C
hU : IsClopen U
S : Set (Set ↑(toTopCat.mapCone C).pt)
hS : S ⊆ {U | ∃ j, ∃ V ∈ {W | IsClopen W}, U = ⇑(ConcreteCategory.hom ((toTopCat.mapCone C).π.app j)) ⁻¹' V}
h : U = ⋃₀ S
j : ↑S → J := fun s ↦ Exists.choose ⋯
V : (s : ↑S) → Set ↑(F.obj (j s)).toTop := fun s ↦ ⋯.choose
hV : ∀ (s : ↑S), IsClopen (V s) ∧ ↑s = ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s
hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i)
hsU : U ⊆ ⋃ i, (fun s ↦ ⇑(ConcreteCategory.hom (C.π.app (j s))) ⁻¹' V s) i
this : ∃ t, U ⊆ ⋃ i ∈ t, ⇑(ConcreteCategory.hom (C.π.app (j i))) ⁻¹' V i
⊢ ∃ j V, IsClopen V ∧ U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
Module: Mathlib.Topology.Category.LightProfinite.Basic

Goal state before:
pp: case mp
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X ↦ TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
H : ((ConcreteCategory.hom h).toFun y).down = { down := 0 }.down
⊢ False

Tactic:
exact top_ne_bot H

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: K S : Finset Λ'
q : Λ'
⊢ Supports (insert q K) S ↔ TM2.SupportsStmt S (tr q) ∧ Supports K S

Tactic:
simp [Supports]

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: S : Finset Λ'
q : Λ'
⊢ Supports {q} S ↔ TM2.SupportsStmt S (tr q)

Tactic:
simp [Supports]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case inr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
refine ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, ?_⟩

Goal state after:
case inr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }
Module: Mathlib.Condensed.Discrete.LocallyConstant

Goal state before:
pp: P : TopCat → Prop
inst✝³ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝² : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑S.toTop) (Y.obj (op (of P PUnit.{u + 1})))
inst✝¹ : PreservesFiniteProducts Y
inst✝ : HasExplicitFiniteCoproducts P
a : Fiber ⇑f
⊢ (ConcreteCategory.hom (sigmaComparison Y fun a ↦ ↑↑a))
      ((ConcreteCategory.hom (inv (sigmaComparison Y fun a ↦ ↑↑a))) (counitAppAppImage f)) a =
    counitAppAppImage f a

Tactic:
exact congrFun (Iso.inv_hom_id_apply (asIso (sigmaComparison Y (fun a ↦ (fiber f a).1)))
    (counitAppAppImage f)) _

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

Goal state before:
pp: X Y : LightCondSet
f : X ⟶ Y
⊢ ∀ (i : (S : LightProfinite) × X.obj.obj (Opposite.op S)),
    Continuous fun a ↦
      (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ LightCondSet.coinducingCoprod✝ X) ⟨i, a⟩

Tactic:
intro ⟨S, x⟩

Goal state after:
X Y : LightCondSet
f : X ⟶ Y
S : LightProfinite
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ LightCondSet.coinducingCoprod✝ X)
      ⟨⟨S, x⟩, a⟩
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F S)

Tactic:
simp [lanPresheafIso, Final.colimitIso]
  rfl

Goal state after:
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: S : LightProfinite
F : LightProfiniteᵒᵖ ⥤ Type u
hF : IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F S)

Tactic:
simp [lanPresheafIso, Final.colimitIso]
  rfl

Goal state after:
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
this : Finite T
Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
Z_closed : ∀ (i : S), IsClosed[inst✝⁸] (Z i)
Z_disj : univ.PairwiseDisjoint Z
D : S → Set Y := fun i ↦ g' ⁻¹' {f' i}
D_clopen : ∀ (i : S), IsClopen (D i)
Z_subset_D : ∀ (i : S), Z i ⊆ D i
C : S → Set Y
C_clopen : ∀ (i : S), IsClopen (C i)
Z_subset_C : ∀ (i : S), Z i ⊆ C i
C_subset_D : ∀ (i : S), C i ⊆ D i
C_cover_D : ⋃ i, D i ⊆ ⋃ i, C i
C_disj : univ.PairwiseDisjoint C
D_cover_univ : univ ⊆ ⋃ i, D i
C_cover_univ : ⋃ i, C i = univ
h_glue : ∀ (i j : S), ∀ x ∈ C i, x ∈ C j → i = j
x : X
⊢ ?m.505 ∈ Z (g x)

Tactic:
by simpa [mem_image] using ⟨x, rfl, rfl⟩

Goal state after:
Module: Mathlib.Condensed.TopCatAdjunction

Goal state before:
pp: X Y : CondensedSet
f : X ⟶ Y
⊢ ∀ (i : (S : CompHaus) × X.obj.obj (Opposite.op S)),
    Continuous fun a ↦
      (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ CondensedSet.coinducingCoprod✝ X) ⟨i, a⟩

Tactic:
intro ⟨S, x⟩

Goal state after:
X Y : CondensedSet
f : X ⟶ Y
S : CompHaus
x : X.obj.obj (Opposite.op S)
⊢ Continuous fun a ↦
    (⇑(ConcreteCategory.hom (f.hom.app (Opposite.op (of PUnit.{u + 1})))) ∘ CondensedSet.coinducingCoprod✝ X)
      ⟨⟨S, x⟩, a⟩
Module: Mathlib.Control.EquivFunctor.Instances

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

Tactic:
ext; simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
| curry (fix (uncurry ∘ _f ∘ curry))

Tactic:
LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝¹ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst✝ : LawfulFix ((x : Sigma β) → γ x.fst x.snd)
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
| curry
    (((monotoneUncurry α β γ).comp ({ toFun := _f, monotone' := ⋯ }.comp (monotoneCurry α β γ)))
      (fix ⇑((monotoneUncurry α β γ).comp ({ toFun := _f, monotone' := ⋯ }.comp (monotoneCurry α β γ)))))
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ Function.Surjective (coverToFun (fibreIncl π σ) (π_r π σ))

Tactic:
by
  intro ⟨⟨⟨t, ht⟩, ⟨t', ht'⟩⟩, _⟩
  by_cases h : (π t).2 = none
  · exact ⟨Sum.inr ⟨(⟨⟨t, ht⟩, by grind⟩, ⟨⟨t', ht'⟩, by grind⟩), by grind⟩, by grind⟩
  · obtain ⟨n, hn⟩ := Option.ne_none_iff_exists'.mp h
    exact ⟨Sum.inl ⟨σ n (π t).1, by grind⟩, by grind⟩

Goal state after:
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 β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x✝ : β
⊢ (x✝ ∈
      match
        match x✝² with
        | ⟨a, f_1⟩ =>
          match x✝¹ with
          | ⟨b, f'⟩ => ⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩ with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)) →
    x✝ ∈
      match x✝² with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)

Tactic:
simp only [mem_iUnion, forall_exists_index]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x✝ : β
⊢ ∀ (x : α) (x_1 : x ∈ F.F.f (F.F.inf x✝².fst x✝¹.fst)),
    x✝ ∈ (G x).F.f ((G x).F.inf (x✝².snd x ⋯) (x✝¹.snd x ⋯)) →
      ∃ i, ∃ (i_1 : i ∈ F.F.f x✝².fst), x✝ ∈ (G i).F.f (x✝².snd i i_1)
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 β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x✝ : β
⊢ (x✝ ∈
      match
        match x✝² with
        | ⟨a, f_1⟩ =>
          match x✝¹ with
          | ⟨b, f'⟩ => ⟨F.F.inf a b, fun i h ↦ (G i).F.inf (f_1 i ⋯) (f' i ⋯)⟩ with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)) →
    x✝ ∈
      match x✝¹ with
      | ⟨s, f_1⟩ => ⋃ i, ⋃ (h : i ∈ F.F.f s), (G i).F.f (f_1 i h)

Tactic:
simp only [mem_iUnion, forall_exists_index]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : Filter α
m : α → Filter β
F : f.Realizer
G : (i : α) → (m i).Realizer
x✝² x✝¹ : (s : F.σ) × ((i : α) → i ∈ F.F.f s → (G i).σ)
x✝ : β
⊢ ∀ (x : α) (x_1 : x ∈ F.F.f (F.F.inf x✝².fst x✝¹.fst)),
    x✝ ∈ (G x).F.f ((G x).F.inf (x✝².snd x ⋯) (x✝¹.snd x ⋯)) →
      ∃ i, ∃ (i_1 : i ∈ F.F.f x✝¹.fst), x✝ ∈ (G i).F.f (x✝¹.snd i i_1)
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f : α → Filter β
F : (i : α) → (f i).Realizer
⊢ ∀ (x : Set β), x ∈ (⊤.bind f).sets ↔ x ∈ (⨆ i, f i).sets

Tactic:
by simp [Filter.bind, iSup_sets_eq]

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
b : Bool
⊢ count b l + count (!b) l = l.length

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : α), x ∈ map equiv.symm.toEmbedding univ

Tactic:
by intros; simp

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend (go f (hd :: tl) #[])

Tactic:
go

Goal state after:
case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match f hd with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ l

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys ↔ ∀ (s : Sigma β), s ∈ l → a ≠ s.fst

Tactic:
by
  grind

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ lookupAll a (⟨a, b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a, b⟩ :: l

Tactic:
simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or,
        false_iff, not_forall, not_and, not_not, reduceCtorEq]

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ∃ x, ¬x = b → ⟨a, x⟩ ∈ l
Module: Mathlib.Data.Multiset.Functor

Goal state before:
pp: case e_a.e_a
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a✝ b✝ : List α'
x y : α'
l✝ : List α'
a b : β'
l : List β'
⊢ flip (fun a b l ↦ ↑(a :: b :: l)) a b l = ↑(a :: b :: l)

Tactic:
simpa [flip] using! Perm.swap a b l

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : Finmap β
h : lookup a s = some b
x : α
⊢ lookup x (erase a s ∪ singleton a b) = lookup x s

Tactic:
by
    by_cases h' : x = a
    · subst a
      rw [lookup_union_right notMem_erase_self, lookup_singleton_eq, h]
    · have : x ∉ singleton a b := by rwa [mem_singleton]
      rw [lookup_union_left_of_not_in this, lookup_erase_ne h']

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
⊢ ((t i ×ˢ s.pi t).sup fun i_1 ↦ f i i_1.1 ⊓ s.attach.inf fun i_2 ↦ f (↑i_2) (i_1.2 ↑i_2 ⋯)) ≤ c ↔
    (((insert i s).pi t).sup fun g ↦
        (insert ⟨i, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)) ≤
      c

Tactic:
simp only [Finset.sup_le_iff, mem_product, mem_pi, and_imp, Prod.forall,
    inf_insert, inf_image]

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
c : α
⊢ (∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a),
      a ∈ t i → (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun i ↦ f (↑i) (b ↑i ⋯)) ≤ c) ↔
    ∀ (b : (a : ι) → a ∈ insert i s → κ a),
      (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) →
        f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 ↦ f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x ↦ ⟨↑x, ⋯⟩) ≤ c
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ (m * n).divisors = image (fun p ↦ p.1 * p.2) (m.divisors ×ˢ n.divisors)

Tactic:
← Finset.mul_def,

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ (m * n).divisors = m.divisors * n.divisors
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))

Tactic:
by_cases h : f false false

Goal state after:
case pos
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))

case neg
f : Bool → Bool → Bool
a b : Bool
m n : ℕ
h : ¬f false false = true
⊢ (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) (Nat.bit a m) (Nat.bit b n)+1]
    else ↑(Nat.bitwise f (Nat.bit a m) (Nat.bit b n))) =
    bit (f a b) (bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) m n+1] else ↑(Nat.bitwise f m n))
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.ofNat
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

Tactic:
by_cases h : f false false

Goal state after:
case pos
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : f false false = true
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)

case neg
f : Bool → Bool → Bool
k a✝¹ a✝ : ℕ
h : ¬f false false = true
⊢ (match bif f false false then -[Nat.bitwise (fun x y ↦ !f x y) a✝¹ a✝+1] else ↑(Nat.bitwise f a✝¹ a✝), k with
    | ofNat m, n => m.testBit n
    | -[m+1], n => !m.testBit n) =
    f (a✝¹.testBit k) (a✝.testBit k)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l.reverse).reverse ++ (takeWhile p l.reverse).reverse = l

Tactic:
← List.reverse_append,

Goal state after:
α : Type u_1
p : α → Bool
l : List α
⊢ (takeWhile p l.reverse ++ dropWhile p l.reverse).reverse = l
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
filter_le_of_le hnl

Goal state after:
case inl
n m l : ℕ
hnl : n ≤ l
⊢ Ico l m = Ico l m
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr
α : Type u_1
r : α → α → Prop
s₁ s₂ t : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ t)

Tactic:
cases t with

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mp
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
inhabited_h : Inhabited n
i : l
j : m
⊢ a i j = 0 i j

Tactic:
replace h := DFunLike.congr_fun h (Matrix.single j (default : n) 1)
    simpa using Matrix.ext_iff.2 h i default

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case refine_4.refine_2
α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₂ - Z₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
· obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
Nat.dvd_iff_mod_eq_zero,

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) % b = 0 ↔ b ∣ ofDigits 1 (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) % b = 0 ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
Nat.dvd_iff_mod_eq_zero,

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(chineseRemainderOfMultiset a s nod hs pp) < (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
unfold chineseRemainderOfMultiset

Goal state after:
case mk
ι : Type u_1
a s : ι → ℕ
l : List ι
nod : Multiset.Nodup (Quot.mk (⇑(List.isSetoid ι)) l)
hs : ∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, s i ≠ 0
pp : {x | x ∈ Quot.mk (⇑(List.isSetoid ι)) l}.Pairwise (Coprime on s)
⊢ ↑(Quotient.recOn (motive := fun x ↦
        x.Nodup → (∀ i ∈ x, s i ≠ 0) → {x_1 | x_1 ∈ x}.Pairwise (Coprime on s) → { k // ∀ i ∈ x, k ≡ a i [MOD s i] })
        (Quot.mk (⇑(List.isSetoid ι)) l) (fun l nod x co ↦ chineseRemainderOfList a s l ⋯) ⋯ nod hs pp) <
    (Multiset.map s (Quot.mk (⇑(List.isSetoid ι)) l)).prod