mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Stonean.Basic

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

Tactic:
rw [← cancel_epi f]

Goal state after:
X Y : Stonean
f : X ⟶ Y
h✝ : Epi f
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
C : Set ((fun X ↦ ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X ↦ ↑X.toTop) Y) := Cᶜ
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
g : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ mkFinite (ULift.{u_1, 0} (Fin 2)) :=
  ConcreteCategory.ofHom { toFun := fun x ↦ { down := 1 }, continuous_toFun := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pos.bit1
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }

Tactic:
obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)

Goal state after:
case pos.bit1
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m ++ [Γ'.cons]) l₁ c d }
          { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step tr) { l := some q.succ, var := ?m.498, stk := elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d }
    { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
⊢ ∃ l₁' l₂' s',
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step tr) { l := some q.succ, var := s, stk := elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d }
        { l := some (unrev q), var := s', stk := elim (l₂' ++ [Γ'.cons]) l₁' c d }
Module: Mathlib.Condensed.Light.Basic

Goal state before:
pp: C : Type w
inst✝ : Category.{v, w} C
X Y : LightCondensed C
f g : X ⟶ Y
h : ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
⊢ f = g

Tactic:
apply Sheaf.hom_ext
  ext
  exact h _

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

Goal state before:
pp: 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 = g

Tactic:
rw [← cancel_epi f]

Goal state after:
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 := ⋯ }
⊢ f ≫ h = f ≫ g
Module: Mathlib.Topology.Category.Profinite.CofilteredLimit

Goal state before:
pp: case refine_1
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✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
⊢ IsOpen ((fun a ↦ hj.elim a) ⁻¹' A)

Tactic:
convert! isOpen_empty

Goal state after:
case e'_3
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✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
⊢ (fun a ↦ hj.elim a) ⁻¹' A = ∅
Module: Mathlib.Topology.Category.LightProfinite.Extend

Goal state before:
pp: F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : LightProfiniteᵒᵖ ⥤ C
S : LightProfinite
x✝¹ x✝ : CostructuredArrow toLightProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
this : (toLightProfinite.map f.left.unop).op ≫ x✝.hom = x✝¹.hom
⊢ (CostructuredArrow.proj toLightProfinite.op (Opposite.op S) ⋙ toLightProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toLightProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
simp only [comp_obj, CostructuredArrow.proj_obj, op_obj, const_obj_obj, Functor.comp_map,
        CostructuredArrow.proj_map, op_map, ← map_comp, this, const_obj_map, Category.comp_id]

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

Goal state before:
pp: case fix.refine_1
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
k : Cont'
H : codeSupp f.fix k ⊆ S
H' : trStmts₁ (trNormal f.fix k) ⊆ S ∧ codeSupp f (Cont'.fix f k) ⊆ S
h : codeSupp' f (Cont'.fix f k) ∪ (trStmts₁ (Λ'.clear natEnd main (trNormal f (Cont'.fix f k))) ∪ {Λ'.ret k}) ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S

Tactic:
simp only [codeSupp', codeSupp, Finset.union_subset_iff, contSupp, trStmts₁,
        Finset.insert_subset_iff] at h H ⊢
      exact ⟨h.1, ⟨H.1.1, h⟩, H.2⟩

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

Goal state before:
pp: X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.obj).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
i : (e.functor.obj X).obj ≅
  (e.functor.obj
      (LocallyConstant.functor.obj
        ((e.functor.obj X).obj.obj (toProfinite.op.obj (Opposite.op (of PUnit.{u + 1})))))).obj :=
  Condensed.isoLocallyConstantOfIsColimit (e.functor.obj X).obj h
⊢ LocallyConstant.functor.essImage X

Tactic:
exact ⟨_, ⟨e.functor.preimageIso ((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

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

Goal state before:
pp: case refine_1
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
⊢ ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ i xi, x = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

Tactic:
intro (f : LocallyConstant c.pt X)

Goal state after:
case refine_1
I : Type u
inst✝² : Category.{u, u} I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
f : LocallyConstant (↑c.pt.toTop) X
⊢ ∃ i xi, f = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case refine_1
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ i xi, x = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi

Tactic:
intro (f : LocallyConstant c.pt X)

Goal state after:
case refine_1
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
f : LocallyConstant (↑c.pt.toTop) X
⊢ ∃ i xi, f = (ConcreteCategory.hom (((locallyConstantPresheaf X).mapCocone c.op).ι.app i)) xi
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 → Part.fix f x = Fix.approx f k.succ x

Tactic:
dsimp [Part.fix]

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

Tactic:
dsimp [Part.fix]

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
⊢ (assert (∃ i, (Fix.approx f i x).Dom) fun h ↦ ⋯.fix (fixAux f) Upto.zero x) = none
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:
ext
  simp [(· ∘ ·), foldrM.ofFreeMonoid, foldrM.mk, Function.flip_def]

Goal state after:
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)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none

Tactic:
simpa [hn'] using Option.isSome_iff_ne_none.mp rfl

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

Goal state before:
pp: case mk
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ { map := map✝, mapConst := mapConst✝ } = { map := fun {α β} ↦ Equiv.map eqv }

Tactic:
congr <;> ext <;> [rw [← h₀]; rw [← h₁]]

Goal state after:
case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³ → x✝²
x✝ : t' x✝³
⊢ map✝ x✝¹ x✝ = x✝¹ <$> x✝

case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
x✝³ x✝² : Type u
x✝¹ : x✝³
x✝ : t' x✝²
⊢ mapConst✝ x✝¹ x✝ = mapConst x✝¹ x✝
Module: Mathlib.Data.BitVec

Goal state before:
pp: z : ℤ
w : ℕ
⊢ { toFin := ↑z }.toInt = (↑z).toInt

Tactic:
rw [toInt_ofFin, Fin.val_intCast, Int.natCast_pow, Nat.cast_ofNat, Int.ofNat_toNat,
      toInt_intCast]

Goal state after:
z : ℤ
w : ℕ
⊢ (max (z % 2 ^ (w + 1)) 0).bmod (2 ^ (w + 1)) = z.bmod (2 ^ (w + 1))
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
inst✝ : PartialOrder α
F : CFilter α σ
E : σ ≃ τ
f : σ → α
p : σ
g : σ → σ → σ
h₁ : ∀ (a b : σ), f (g a b) ≤ f a
h₂ : ∀ (a b : σ), f (g a b) ≤ f b
a b : τ
⊢ f (E.symm (E (g (E.symm a) (E.symm b)))) ≤ f (E.symm b)

Tactic:
simpa using h₂ (E.symm a) (E.symm b)

Goal state after:
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: case mk.mk.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } →
    s✝ ∈
      { 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:
rintro ⟨s, t, h⟩

Goal state after:
case mk.mk.mp
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
s : σ✝¹
t : σ✝
h : F✝¹.f s ∩ F✝.f t ⊆ s✝
⊢ s✝ ∈
    { 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.Filter

Goal state before:
pp: case mk.mk.mpr
α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
σ✝¹ : Type ?u.88
F✝¹ : CFilter (Set α) σ✝¹
σ✝ : Type ?u.92
F✝ : CFilter (Set α) σ✝
s✝ : Set α
⊢ s✝ ∈
      { 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 := ⋯ } →
    s✝ ∈ { sets := {a | ∃ a_1 b, F✝¹.f a_1 ∩ F✝.f b ⊆ a}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Tactic:
· rintro ⟨_, ⟨a, ha⟩, _, ⟨b, hb⟩, rfl⟩
        exact ⟨a, b, inter_subset_inter ha hb⟩

Goal state after:
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc g).support
h : x ∉ f.support ∪ g.support
⊢ False

Tactic:
refine notMem_support_iff.2 ?_ hx

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ (f.rangeIcc g).support
h : x ∉ f.support ∪ g.support
⊢ (f.rangeIcc g) x = 0
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : Erased α) (y : Erased β), x <* y = Function.const β <$> x <*> y

Tactic:
intros; ext; simp [Seq.seq, SeqLeft.seqLeft]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert a b s).entries = ⟨a, b⟩ :: s.entries

Tactic:
rw [entries_insert, kerase_of_notMem_keys h]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝ ↔
    dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
constructor <;> intro h'

Goal state after:
case mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

case mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝
⊢ dlookup x✝ s₁.entries = some y✝ ∨ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type ?u.51
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
⊢ s₂.liftOn (f a₁) ⋯ = s₂.liftOn (f a₂) ⋯

Tactic:
have H' : f a₁ = f a₂ := funext fun _ => H _ _ _ _ p (Perm.refl _)

Goal state after:
α : Type u
β : α → Type v
γ : Type ?u.51
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H : ∀ (a₁ b₁ a₂ b₂ : AList β), a₁.entries ~ a₂.entries → b₁.entries ~ b₂.entries → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries ~ a₂.entries
H' : f a₁ = f a₂
⊢ s₂.liftOn (f a₁) ⋯ = s₂.liftOn (f a₂) ⋯
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : Finmap β
⊢ (keysLookupEquiv.symm (keysLookupEquiv x✝)).keys = (↑(keysLookupEquiv x✝)).1

Tactic:
by
    simp only [Equiv.symm_apply_apply, keysLookupEquiv_apply_coe_fst]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ ∀ (a_1 b_1 : Sigma β), (b_1 ∈ if a = a_1.fst then some ⟨a, b⟩ else none) → a_1.fst = b_1.fst

Tactic:
rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩
    dsimp
    split_ifs with h <;> simp +contextual [h]

Goal state after:
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
f : β✝ → α✝
hf : f ∈ image (const β✝) s
ha : a ∈ image f t
⊢ a ∈ s

Tactic:
mem_image

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
f : β✝ → α✝
hf : ∃ a ∈ s, const β✝ a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ s
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
f : β✝ → β✝
hf : f ∈ image (const α✝ id) s
ha : a ∈ image f t
⊢ a ∈ t

Tactic:
mem_image

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
f : β✝ → β✝
hf : ∃ a ∈ s, const α✝ id a = f
ha : ∃ a_1 ∈ t, f a_1 = a
⊢ a ∈ t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
h₂ : ¬a' = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
subst h₁

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
bh : β a
h₂ : ¬a' = a
⊢ dlookup a (kerase a' (⟨a, bh⟩ :: tl)) = dlookup a (⟨a, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₂ : a₂ ∈ l.keys
b₁ : β a₁
l₁ l₂ : List (Sigma β)
a₁_nin_l₁ : ¬a₁ ∈ l₁.keys
x✝ : a₂ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
ha₁ : a₁ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
h' : ¬a₂ ∈ l₁.keys
⊢ kerase a₂ (l₁ ++ l₂) = kerase a₁ (kerase a₂ (l₁ ++ ⟨a₁, b₁⟩ :: l₂))

Tactic:
by
            simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
              @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (Ne.symm h)]

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

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : a = a'
⊢ b ∈ dlookup a ((⟨a', snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a', snd✝⟩ :: tail✝) ∨ ¬a ∈ (⟨a', snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂

Tactic:
subst h₁

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (tail✝.kunion l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ tail✝.keys ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
snd✝ : β a
⊢ b ∈ dlookup a ((⟨a, snd✝⟩ :: tail✝).kunion l₂) ↔
    b ∈ dlookup a (⟨a, snd✝⟩ :: tail✝) ∨ ¬a ∈ (⟨a, snd✝⟩ :: tail✝).keys ∧ b ∈ dlookup a l₂
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (List.map Prod.toSigma f.graph.toList).NodupKeys

Tactic:
rw [List.NodupKeys, List.keys, List.map_map, Prod.fst_comp_toSigma, List.nodup_map_iff_inj_on]
      · rintro ⟨b, m⟩ hb ⟨c, n⟩ hc (rfl : b = c)
        rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc
        dsimp at hb hc
        rw [← hc.1, hb.1]
      · apply Finset.nodup_toList

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ l.lookupFinsupp a = x ↔ x ∈ lookup a l

Tactic:
lookupFinsupp_apply

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ (lookup a l).getD 0 = x ↔ x ∈ lookup a l
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ (m * n).bodd = (m.bodd && n.bodd)

Tactic:
rcases m with m | m <;> rcases n with n | n

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (ofNat m * ofNat n).bodd = ((ofNat m).bodd && (ofNat n).bodd)

case ofNat.negSucc
m n : ℕ
⊢ (ofNat m * -[n+1]).bodd = ((ofNat m).bodd && -[n+1].bodd)

case negSucc.ofNat
m n : ℕ
⊢ (-[m+1] * ofNat n).bodd = (-[m+1].bodd && (ofNat n).bodd)

case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] * -[n+1]).bodd = (-[m+1].bodd && -[n+1].bodd)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise or m n = m.lor n

Tactic:
rcases m with m | m <;> rcases n with n | n

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise or (ofNat m) (ofNat n) = (ofNat m).lor (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise and m n = m.land n

Tactic:
rcases m with m | m <;> rcases n with n | n

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ bitwise and (ofNat m) (ofNat n) = (ofNat m).land (ofNat n)

case ofNat.negSucc
m n : ℕ
⊢ bitwise and (ofNat m) -[n+1] = (ofNat m).land -[n+1]

case negSucc.ofNat
m n : ℕ
⊢ bitwise and -[m+1] (ofNat n) = -[m+1].land (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ bitwise and -[m+1] -[n+1] = -[m+1].land -[n+1]