mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case rfind
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
hf : Partrec ↑f✝
this✝ : Partrec fun a ↦ ↑f✝ (a.2 ::ᵥ a.1)
this : Partrec₂ fun a ↦ ↑fun b ↦ decide (id (f✝ ((a, b).2 ::ᵥ (a, b).1)) = 0)
⊢ Partrec fun v ↦ Nat.rfind fun n ↦ Part.some (decide (f✝ (n ::ᵥ v) = 0))

Tactic:
exact _root_.Partrec.rfind this

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)

Tactic:
simp [e]

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this✝ : Nat.Partrec fun n ↦ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ x ∈ (Option.none <|> Code.evaln k cg n)

Tactic:
simp [e]

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  · refine evalInduction h fun a h IH ↦ ?_
    rcases e : f a with - | a'
    · rw [Part.mem_unique h
          (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]
      exact ⟨ReflTransGen.refl, e⟩
    · rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;>
        cases Part.mem_some_iff.1 h
      obtain ⟨h₁, h₂⟩ := IH a' e
      exact ⟨ReflTransGen.head e h₁, h₂⟩
  · refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_
    · refine PFun.mem_fix_iff.2 (Or.inl ?_)
      rw [h₂]
      apply Part.mem_some
    · refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)
      rw [h]
      apply Part.mem_some

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab : Reaches f₁ a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

Tactic:
rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | ab)

Goal state after:
case inl
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₂ : σ₂
b₁ : σ₁
aa : tr b₁ a₂
ab : Reaches f₁ b₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂

case inr
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂ → Prop
H : Respects f₁ f₂ tr
a₁ : σ₁
a₂ : σ₂
aa : tr a₁ a₂
b₁ : σ₁
ab✝ : Reaches f₁ a₁ b₁
ab : TransGen (fun a b ↦ b ∈ f₁ a) a₁ b₁
⊢ ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: Γ : Type ?u.8
Γ' : Type ?u.12
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ n, f default = List.replicate n default
⊢ ListBlank Γ'

Tactic:
apply l.liftOn (fun l ↦ ListBlank.mk (l.flatMap f))
  rintro l _ ⟨i, rfl⟩; obtain ⟨n, e⟩ := hf; refine Quotient.sound' (Or.inl ⟨i * n, ?_⟩)
  rw [List.flatMap_append, mul_comm]; congr
  induction i with
  | zero => rfl
  | succ i IH =>
    simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ,
      List.flatMap_cons]

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

Goal state before:
pp: case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S

pp: case left.right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.2 ∈ Finset.univ

Tactic:
· simp only [default, TM1.stmts, Finset.mem_insertNone, Option.mem_def, Option.some_inj,
        forall_eq', Finset.mem_biUnion]
      exact ⟨_, ss.1, TM1.stmts₁_self⟩

Goal state after:
case left.right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.2 ∈ Finset.univ
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ ∀ {q : Λ' M} {a : Γ} {q' : Λ' M} {s : TM0.Stmt Γ}, (q', s) ∈ tr M q a → q ∈ ↑(trStmts M S) → q' ∈ ↑(trStmts M S)

Tactic:
intro q a q' s h₁ h₂

Goal state after:
case right
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
q : Λ' M
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
h₁ : (q', s) ∈ tr M q a
h₂ : q ∈ ↑(trStmts M S)
⊢ q' ∈ ↑(trStmts M S)
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg.mpr.cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a :: x = b :: t ++ u
hP : P.rmatch (b :: t) = true
⊢ ∃ t u, x = t ++ u ∧ (P.deriv a).rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [List.cons_append, List.cons_eq_cons] at h
          refine ⟨t, u, h.2, ?_, hQ⟩
          rw [rmatch] at hP
          convert! hP
          exact h.1

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

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ k)

Tactic:
rw [h]; exact s

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

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ k)

Tactic:
rw [h]; exact s

Goal state after:
Module: Mathlib.Topology.Category.CompHausLike.Limits

Goal state before:
pp: P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x y : ↑(X a).toTop
⊢ (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) y → x = y

Tactic:
hxy

Goal state after:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
a : α
x y : ↑(X a).toTop
hxy : (ConcreteCategory.hom (ι X a)) x = (ConcreteCategory.hom (ι X a)) y
⊢ x = y
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case mpr
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

Tactic:
obtain he | ⟨v'', he₁', _⟩ := PFun.mem_fix_iff.1 he

Goal state after:
case mpr.inl
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝¹ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he✝ : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
he : Sum.inl v' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)

case mpr.inr
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he✝ : v' ∈ f.fix.eval v✝
hr✝ : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Sum.inr a'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v) →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' : Sum.inr v'' ∈ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)
right✝ :
  v' ∈ PFun.fix (fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) v''
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
⊢ x ≠ y → (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y

Tactic:
hxy

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Module: Mathlib.Topology.Category.Profinite.Basic

Goal state before:
pp: case hnc
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 := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ V

Tactic:
refine mt (fun α => hVU α) ?_

Goal state after:
case hnc
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 := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ U
Module: Mathlib.Topology.DiscreteQuotient

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid
compat : ∀ (A B : DiscreteQuotient X) (h : A ≤ B), ofLE h (Qs A) = Qs B
x✝¹ x✝ : DiscreteQuotient X
h : x✝¹ ≤ x✝
⊢ x✝¹.proj ⁻¹' {Qs x✝¹} ⊆ x✝.proj ⁻¹' {Qs x✝}

Tactic:
by
    rw [← compat _ _ h]
    exact fiber_subset_ofLE _ _

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

Goal state before:
pp: case hnc
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 := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ V

Tactic:
refine mt (fun α => hVU α) ?_

Goal state after:
case hnc
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 := ⋯ }
x : ↑X.toTop
⊢ (ConcreteCategory.hom f).toFun x ∉ U
Module: Mathlib.Condensed.TopComparison

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
⊢ (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y → a x = a y

Tactic:
hxy

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
G : C ⥤ TopCat
X : Type w'
inst✝² : TopologicalSpace X
Z B : C
π : Z ⟶ B
inst✝¹ : HasPullback π π
inst✝ : PreservesLimit (cospan π π) G
a : C(↑(G.obj Z), X)
ha : ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.fst π π))) = ⇑a ∘ ⇑(ConcreteCategory.hom (G.map (pullback.snd π π)))
x y : ↑(G.obj Z)
hxy : (ConcreteCategory.hom (G.map π)) x = (ConcreteCategory.hom (G.map π)) y
⊢ a x = a y
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case fix.false
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.19} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.21} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif false then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Tactic:
refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)

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

Goal state before:
pp: I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
have : DiscreteTopology (toProfinite.obj X) := ⟨rfl⟩

Goal state after:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
this : DiscreteTopology ↑(toProfinite.obj X).toTop
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g
Module: Mathlib.Topology.Category.Profinite.Extend

Goal state before:
pp: case right
I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst✝ : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left✝² : Discrete PUnit.{1}
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
i : I
left✝¹ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s : F.obj i ⟶ X
w : f = c.π.app i ≫ toProfinite.map s
left✝ : ((e.inverse ⋙ functor c).obj { down := i }).left ⟶ { left := left✝², right := X, hom := f }.left
s' : F.obj i ⟶ X
w'✝ : f = c.π.app i ≫ toProfinite.map s'
w' : c.π.app i ≫ toProfinite.map s = c.π.app i ≫ toProfinite.map s'
⊢ StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor c).obj { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝¹, right := s, w := w } =
    StructuredArrow.Hom.right (𝟙 ((e.inverse ⋙ functor c).obj { down := i })) ≫
      StructuredArrow.Hom.right { left := left✝, right := s', w := w'✝ }

Tactic:
exact toProfinite.map_injective <| Epi.left_cancellation _ _ w'

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

Goal state before:
pp: I : Type u
inst✝² : SmallCategory I
inst✝¹ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
C : Type u_1
inst✝ : Category.{v_1, u_1} C
G : Profiniteᵒᵖ ⥤ C
S : Profinite
x✝¹ x✝ : CostructuredArrow toProfinite.op (Opposite.op S)
f : x✝¹ ⟶ x✝
⊢ (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ G).map f ≫ G.map x✝.hom =
    G.map x✝¹.hom ≫ ((const (CostructuredArrow toProfinite.op (Opposite.op S))).obj (G.obj (Opposite.op S))).map f

Tactic:
have := f.w
      simp only [op_obj, const_obj_obj, op_map, CostructuredArrow.right_eq_id, const_obj_map,
        Category.comp_id] at this
      simp [← map_comp, this]

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

Goal state before:
pp: case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } fi)
      ((ConcreteCategory.hom (c.π.app k)) x) =
    ({ toFun := fun g ↦ LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } fj)
      ((ConcreteCategory.hom (c.π.app k)) x)

Tactic:
change fi ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x) =
      fj ((c.π.app k ≫ (F ⋙ toLightProfinite).map _) x)

Goal state after:
case refine_2
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop) X
fj : LocallyConstant (↑((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop) X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h✝ : True
x✝ : ↑(toLightProfinite.obj (F.obj k)).toTop
x : ↑(((const ℕᵒᵖ).obj c.pt).obj k).toTop
hx : (ConcreteCategory.hom (c.π.app k)) x = x✝
⊢ fi ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map ki)) x) =
    fj ((ConcreteCategory.hom (c.π.app k ≫ (F ⋙ toLightProfinite).map kj)) x)
Module: Mathlib.Control.Functor.Multivariate

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

Tactic:
simp only [RelLast]; erw [repeatEq_iff_eq]

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

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

Tactic:
simp only [RelLast]; erw [repeatEq_iff_eq]

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
h₁ : (approx (⇑f) (Nat.find h₀) a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
dom_iff_mem

Goal state after:
case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
h₁ : ∃ y, y ∈ approx (⇑f) (Nat.find h₀) a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
⊢ (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → (fs : v ⟹ v') → β v v' fs

Tactic:
intro v v'
  rw [← append1_drop_last v, ← append1_drop_last v']
  intro fs
  rw [← split_dropFun_lastFun fs]
  apply F

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)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (fun a ↦ ωSup (c.map (evalOrderHom a))) x y =
    ωSup (((c.map (monotoneCurry α β γ)).map (evalOrderHom x)).map (evalOrderHom y))

Tactic:
rw [map_comp, map_comp]

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ x.fst x.snd)
x : α
y : β x
⊢ (monotoneCurry α β γ) (fun a ↦ ωSup (c.map (evalOrderHom a))) x y =
    ωSup (c.map (((evalOrderHom y).comp (evalOrderHom x)).comp (monotoneCurry α β γ)))
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)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup ((c.map (evalOrderHom x)).map (evalOrderHom y)) =
    ωSup ((c.map (monotoneUncurry α β γ)).map (evalOrderHom ⟨x, y⟩))

Tactic:
rw [map_comp, map_comp]

Goal state after:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup (c.map ((evalOrderHom y).comp (evalOrderHom x))) =
    ωSup (c.map ((evalOrderHom ⟨x, y⟩).comp (monotoneUncurry α β γ)))
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ b ∈ dlookup a l → ⟨a, b⟩ ∈ l

Tactic:
by
  induction l with
  | nil => grind
  | cons s _ _ => by_cases a = s.fst <;> grind

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

Goal state before:
pp: case pos.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : a = y.fst
h₂ : w ∈ some ⟨a, b⟩
⊢ x = y ∧ ⟨a, b⟩ = w

Tactic:
cases h₂

Goal state after:
case pos.refl.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
h_2 : a = x.fst
h_1 : a = y.fst
⊢ x = y ∧ ⟨a, b⟩ = ⟨a, b⟩
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg.refl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys
x y : Sigma β
h : x.fst ≠ y.fst
w : Sigma β
h_2 : a = x.fst
h_1 : ¬a = y.fst
h₂ : w ∈ none
⊢ x = y ∧ ⟨a, b⟩ = w

Tactic:
cases h₂

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

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ image (fun p ↦ p.1 * p.2) (image Subtype.val (m.divisors ×ˢ n.divisors).attach) =
    map { toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ } (m.divisors ×ˢ n.divisors).attach

Tactic:
Finset.map_eq_image,

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ image (fun p ↦ p.1 * p.2) (image Subtype.val (m.divisors ×ˢ n.divisors).attach) =
    image (⇑{ toFun := fun p ↦ (↑p).1 * (↑p).2, inj' := ⋯ }) (m.divisors ×ˢ n.divisors).attach