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

Goal state before:
pp: T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ ¬g.Derives [Symbol.nonterminal t] s

Tactic:
derives_iff_eq_or_head

Goal state after:
T : Type u_1
g : ContextFreeGrammar T
t : g.NT
hgt : ∀ r ∈ g.rules, r.input ≠ t
s : List (Symbol T g.NT)
hs : s ≠ [Symbol.nonterminal t]
⊢ ¬([Symbol.nonterminal t] = s ∨ ∃ v, g.Produces [Symbol.nonterminal t] v ∧ g.Derives v s)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x ↦ (f x)⁻¹

Tactic:
cases hf.eventually_atTop_zero_or_pos_or_neg with
  | inl hf' =>
    refine fun b hb => ⟨1, by simp, 1, by simp, ?_⟩
    have hb_pos := hb.1
    filter_upwards [hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx'
    intro u hu
    simp only [hx, inv_zero, mul_zero, Set.Icc_self, Set.mem_singleton_iff, hx' u hu.1]
  | inr hf_pos_or_neg =>
    suffices GrowsPolynomially fun x => |(f x)⁻¹| by
      cases hf_pos_or_neg with
      | inl hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => |(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          rw [abs_of_nonneg (inv_nonneg_of_nonneg (le_of_lt hx₁))]
        rwa [iff_eventuallyEq hmain]
      | inr hf' =>
        have hmain : (fun x => (f x)⁻¹) =ᶠ[atTop] fun x => -|(f x)⁻¹| := by
          filter_upwards [hf'] with x hx₁
          simp [abs_of_nonpos (inv_nonpos.mpr (le_of_lt hx₁))]
        rw [iff_eventuallyEq hmain]
        exact this.neg
    have hf' : ∀ᶠ x in atTop, f x ≠ 0 := by
      cases hf_pos_or_neg with
      | inl H => filter_upwards [H] with _ hx; exact (ne_of_lt hx).symm
      | inr H => filter_upwards [H] with _ hx; exact (ne_of_gt hx).symm
    simp only [abs_inv]
    have hf := hf.abs
    intro b hb
    have hb_pos := hb.1
    obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf b hb
    refine ⟨c₂⁻¹, by change 0 < c₂⁻¹; positivity, ?_⟩
    refine ⟨c₁⁻¹, by change 0 < c₁⁻¹; positivity, ?_⟩
    filter_upwards [hf, hf', (tendsto_id.const_mul_atTop hb_pos).eventually_forall_ge_atTop hf']
      with x hx hx' hx''
    intro u hu
    have h₁ : 0 < |f u| := by rw [abs_pos]; exact hx'' u hu.1
    refine ⟨?lb, ?ub⟩
    case lb =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).2
    case ub =>
      rw [← mul_inv]
      gcongr
      exact (hx u hu).1

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
⊢ (∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) →
    0 ≤ f x →
      (∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y) →
        ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)

Tactic:
hf₁

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
h✝ : 0 ≤ p
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 ≤ f x →
    (∀ (y : ℝ), b * id x ≤ y → 0 ≤ f y) →
      ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₁ ^ p * f x ^ p) (c₂ ^ p * f x ^ p)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
hx' : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ^ p = 0

Tactic:
simp only [hx, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx'

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hzero : ∀ᶠ (x : ℝ) in atTop, f x = 0
x : ℝ
hx : f x = 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hx' : ∀ u ∈ Set.Icc (b * x) x, f u = 0
⊢ f u ^ p = 0
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
⊢ (∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)) →
    0 < f x →
      (∀ (y : ℝ), b * id x ≤ y → 0 < f y) →
        ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₂ ^ p * f x ^ p) (c₁ ^ p * f x ^ p)

Tactic:
hf₁

Goal state after:
f : ℝ → ℝ
p : ℝ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : 0 < c₁
c₂ : ℝ
hc₂_mem : c₂ > 0
hfnew : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hc₁p : 0 < c₁ ^ p
hc₂p : 0 < c₂ ^ p
hp : p < 0
hpos : ∀ᶠ (x : ℝ) in atTop, 0 < f x
x : ℝ
a✝ : 0 < x
hf₁ : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
⊢ 0 < f x →
    (∀ (y : ℝ), b * id x ≤ y → 0 < f y) →
      ∀ u ∈ Set.Icc (b * x) x, f u ^ p ∈ Set.Icc (c₂ ^ p * f x ^ p) (c₁ ^ p * f x ^ p)
Module: Mathlib.Computability.Encoding

Goal state before:
pp: x : ℕ
⊢ decodeNat (List.map sectionΓ'Bool (List.map inclusionBoolΓ' (encodeNat x))) = x

Tactic:
by simp [Function.comp_def]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ M.evalFrom ∅ x = ∅

Tactic:
induction x using List.reverseRecOn with
  | nil => rw [evalFrom_nil, εClosure_empty]
  | append_singleton x a ih => rw [evalFrom_append_singleton, ih, stepSet_empty]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false (n + 1)) = ofNat' (Nat.bit true n) + 1

Tactic:
ofNat'_bit,

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' (n + 1)) = ofNat' (Nat.bit true n) + 1
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' (n + 1)) = ofNat' (Nat.bit true n) + 1

Tactic:
ofNat'_bit,

Goal state after:
case true
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' (n + 1)) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
ih : ∃ n, M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)

Tactic:
obtain ⟨n, _⟩ := ih

Goal state after:
case step
α : Type u
σ : Type v
M : εNFA α σ
s₁ s₂ s✝ t✝ : σ
a✝¹ : t✝ ∈ M.step s✝ none
a✝ : M.εClosure {s₁} s✝
n : ℕ
h✝ : M.IsPath s₁ s✝ (List.replicate n none)
⊢ ∃ n, M.IsPath s₁ t✝ (List.replicate n none)
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ : σ
h : ∃ t, M.IsPath s₁ t (List.replicate n✝ none) ∧ s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}

Tactic:
obtain ⟨t, _, _⟩ := h

Goal state after:
case succ
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
n✝ : ℕ
a✝ : ∀ {s₂ : σ}, M.IsPath s₁ s₂ (List.replicate n✝ none) → s₂ ∈ M.εClosure {s₁}
s₂ t : σ
left✝ : M.IsPath s₁ t (List.replicate n✝ none)
right✝ : s₂ ∈ M.step t none
⊢ s₂ ∈ M.εClosure {s₁}
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ true = (ofNat (Option ℕ) (f (a ::ᵥ v))).isSome → (b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b)

Tactic:
rcases f (a ::ᵥ v) with - | c

Goal state after:
case refine_2.zero
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
⊢ true = (ofNat (Option ℕ) 0).isSome → (b = pred 0 ↔ ofNat (Option ℕ) 0 = some b)

case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
⊢ true = (ofNat (Option ℕ) (c + 1)).isSome → (b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b)
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
← Option.some_inj,

Goal state after:
case refine_2.succ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' ↑f
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun n_1 ↦ ↑(some (ofNat (Option ℕ) (f (n_1 ::ᵥ v))).isSome)
c : ℕ
this : true = (ofNat (Option ℕ) (c + 1)).isSome
⊢ some b = some (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b c : σ
h₁ : Reaches₁ f a c
h₂ : b ∈ f a
⊢ Reaches f b c

Tactic:
by
  rcases TransGen.head'_iff.1 h₁ with ⟨b', hab, hbc⟩
  cases Option.mem_unique hab h₂; exact hbc

Goal state after:
Module: Mathlib.Computability.StateTransition

Goal state before:
pp: σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
⊢ False

Tactic:
let ⟨_, b0⟩ := mem_eval.1 h

Goal state after:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
x✝ : Reaches₁ f b c
bc : Reaches₁ f b c := x✝
left✝ : Reaches f a b
b0 : f b = none
⊢ False
Module: Mathlib.Computability.RE

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val✝ : β
⊢ (bif Sum.casesOn (Sum.inl val✝) (fun b ↦ true) fun b ↦ false then
      Sum.casesOn (Sum.inl val✝) (fun b ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun c ↦ Part.some Option.none
    else
      Sum.casesOn (Sum.inl val✝) (fun b ↦ Part.some Option.none) fun b ↦ Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (Sum.inl val✝) (g a) (h a))

Tactic:
simp only [Bool.cond_true, Bool.cond_false]

Goal state after:
Module: Mathlib.Computability.RE

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val✝ : γ
⊢ (bif Sum.casesOn (Sum.inr val✝) (fun b ↦ true) fun b ↦ false then
      Sum.casesOn (Sum.inr val✝) (fun b ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun c ↦ Part.some Option.none
    else
      Sum.casesOn (Sum.inr val✝) (fun b ↦ Part.some Option.none) fun b ↦ Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (Sum.inr val✝) (g a) (h a))

Tactic:
simp only [Bool.cond_true, Bool.cond_false]

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case rfind
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
hO : ∀ g ∈ O, Nat.Partrec g
f✝ : ℕ →. ℕ
hf✝ : Nat.RecursiveIn O f✝
ih : Nat.Partrec f✝
⊢ Nat.Partrec fun a ↦ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f✝ (Nat.pair a n)

Tactic:
exact .rfind ih

Goal state after:
Module: Mathlib.Computability.RecursiveIn

Goal state before:
pp: case rfind
f : ℕ →. ℕ
O : Set (ℕ →. ℕ)
f✝ : ℕ →. ℕ
a✝ : Nat.Partrec f✝
ih : Nat.RecursiveIn O f✝
⊢ Nat.RecursiveIn O fun a ↦ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f✝ (Nat.pair a n)

Tactic:
exact .rfind ih

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
a head✝ : α
⊢ (char a).rmatch [head✝] = true ↔ [head✝] = [a]

Tactic:
rw [rmatch, deriv, List.singleton_inj]
      split <;> tauto

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : a = head✝
⊢ rmatch 0 tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
zero_rmatch,

Goal state after:
case cons.cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : a = head✝
⊢ false = true ↔ head✝ = a ∧ head :: tail = []
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case cons.cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : ¬a = head✝
⊢ rmatch 0 tail = true ↔ head✝ = a ∧ head :: tail = []

Tactic:
zero_rmatch,

Goal state after:
case cons.cons.isFalse
α : Type u_1
inst✝ : DecidableEq α
a head✝ head : α
tail : List α
h✝ : ¬a = head✝
⊢ false = true ↔ head✝ = a ∧ head :: tail = []
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₁ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₂ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L))) b
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (bif p v then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif (fun x ↦ p) (Tape.mk' ∅ (addBottom L)).head v then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b

Tactic:
beta_reduce

Goal state after:
case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
l : Λ
p : σ → Bool
q₁ q₂ : TM2.Stmt Γ Λ σ
IH₁ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₁ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))) b
IH₂ :
  ∀ {v : σ} {S : (k : K) → List (Γ k)} (L : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse) →
      ∃ b,
        TrCfg (TM2.stepAux q₂ v S) b ∧
          Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L))) b
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
⊢ ∃ b,
    TrCfg (bif p v then TM2.stepAux q₁ v S else TM2.stepAux q₂ v S) b ∧
      Reaches (TM1.step (tr M))
        (bif p v then TM1.stepAux (trNormal q₁) v (Tape.mk' ∅ (addBottom L))
        else TM1.stepAux (trNormal q₂) v (Tape.mk' ∅ (addBottom L)))
        b
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
⊢ ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i =
    ⋂ i, ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' ⋂ (_ : i ∈ G), Vs i

Tactic:
apply congrArg

Goal state after:
case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := ⋯
Vs : J → Set ↑(F.obj j) := ⋯
V : Set ↑(F.obj j) := ⋯
⊢ (fun i ↦ ⋂ (_ : i ∈ G), (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i) = fun i ↦
    ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' ⋂ (_ : i ∈ G), Vs i
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := fun x he ↦ ⋯.some
Vs : J → Set ↑(F.obj j) := fun e ↦ if h : e ∈ G then ⇑(ConcreteCategory.hom (F.map (g e h))) ⁻¹' U e else Set.univ
V : Set ↑(F.obj j) := ⋂ e ∈ G, Vs e
e : J
⊢ ⋂ (_ : e ∈ G), (fun x ↦ (ConcreteCategory.hom (C.π.app e)) x) ⁻¹' U e =
    ⋂ (_ : e ∈ G), ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' Vs e

Tactic:
apply congrArg

Goal state after:
case e'_3.mpr.refine_2
J : Type v
inst✝¹ : Category.{w, v} J
inst✝ : IsCofiltered J
F : J ⥤ TopCat
C : Cone F
hC : IsLimit C
T : (j : J) → Set (Set ↑(F.obj j))
hT : ∀ (j : J), IsTopologicalBasis (T j)
univ : ∀ (i : J), Set.univ ∈ T i
inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i
compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i
U0 : Set ↑C.pt
U : (i : J) → Set ↑(F.obj i)
G : Finset J
h1 : ∀ i ∈ G, U i ∈ T i
h2 : U0 = ⋂ i ∈ G, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i
j : J
hj : ∀ {X : J}, X ∈ G → Nonempty (j ⟶ X)
g : (e : J) → e ∈ G → (j ⟶ e) := ⋯
Vs : J → Set ↑(F.obj j) := ⋯
V : Set ↑(F.obj j) := ⋯
e : J
⊢ (fun x ↦ (fun x ↦ (ConcreteCategory.hom (C.π.app e)) x) ⁻¹' U e) = fun i ↦
    ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' Vs e
Module: Mathlib.Topology.Category.LightProfinite.AsLimit

Goal state before:
pp: S : LightProfinite
n : ℕ
⊢ lightToProfinite.map (S.proj n) =
    (lightToProfinite.obj S).asLimitCone.π.app
      ((IsCofiltered.sequentialFunctor (DiscreteQuotient ↑(lightToProfinite.obj S).toTop)).obj (Opposite.op n))

Tactic:
simp only [toCompHausLike_map]
  let c : Cone (S.diagram ⋙ lightToProfinite) := S.toLightDiagram.cone
  let hc : IsLimit c := S.toLightDiagram.isLimit
  exact liftedLimitMapsToOriginal_inv_map_π hc _

Goal state after:
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})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ (ConcreteCategory.hom (Y.map (isTerminalPUnit.from (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)).op))
      (Fiber.image (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a) =
    (ConcreteCategory.hom
        (Y.map
          (componentHom f g.unop a ≫
              isTerminalPUnit.from
                (fiber f
                  (Fiber.mk (⇑f)
                    ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a))))).op))
      (Fiber.image (⇑f)
        (Fiber.mk (⇑f) ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a))))

Tactic:
apply congrArg

Goal state after:
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})))
T✝ : CompHausLike P
g✝ : T✝ ⟶ S✝
inst✝¹ : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝ : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : (functorToPresheaves.obj (Y.obj (op (of P PUnit.{u + 1})))).obj S
a : Fiber ⇑(comap (TopCat.Hom.hom g.unop.hom) f)
⊢ Fiber.image (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a =
    Fiber.image (⇑f)
      (Fiber.mk (⇑f) ((ConcreteCategory.hom g.unop) (preimage (⇑(comap (TopCat.Hom.hom g.unop.hom) f)) a)))
Module: Mathlib.Condensed.Light.InternallyProjective

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ P ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (β_ P ((free R).obj S.toCondensed)).hom ≫ g = g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ P ≫ g = g' ≫ e

Tactic:
refine ⟨S', π, hπ, (β_ _ _).inv ≫ g', ?_⟩

Goal state after:
case refine_1
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : (free R).obj S.toCondensed ⊗ P ⟶ B
S' : LightProfinite
π : S' ⟶ S
hπ : Function.Surjective ⇑(ConcreteCategory.hom π)
g' : P ⊗ (free R).obj S'.toCondensed ⟶ A
hh : P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ (β_ P ((free R).obj S.toCondensed)).hom ≫ g = g' ≫ e
⊢ (lightProfiniteToLightCondSet ⋙ free R).map π ▷ P ≫ g = ((β_ P ((free R).obj S'.toCondensed)).inv ≫ g') ≫ e