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

Goal state before:
pp: case refine_4
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
⊢ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
      M.evalFrom s (List.take (↑n) (List.take (↑m) x)) ∧
    M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t

Tactic:
have hq : M.evalFrom (M.evalFrom s ((x.take m).take n)) ((x.take m).drop n) =
      M.evalFrom s ((x.take m).take n) := by
    rw [List.take_take, min_eq_left hle, ← evalFrom_of_append, heq, ← min_eq_left hle, ←
      List.take_take, min_eq_left hle, List.take_append_drop]

Goal state after:
case refine_4
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (↑n) (List.take (↑m) x))
⊢ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
      M.evalFrom s (List.take (↑n) (List.take (↑m) x)) ∧
    M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
Module: Mathlib.Computability.DFA

Goal state before:
pp: case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (↑n) (List.take (↑m) x))
⊢ M.evalFrom s (List.take (↑n) (List.take (↑m) x) ++ (List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x)) = t

Tactic:
← List.append_assoc,

Goal state after:
case right
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
s t : σ
hlen : Fintype.card σ ≤ x.length
hx : M.evalFrom s x = t
n m : Fin (Fintype.card σ + 1)
hneq : n ≠ m
heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)
hle : ↑n ≤ ↑m
hq :
  M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) =
    M.evalFrom s (List.take (↑n) (List.take (↑m) x))
⊢ M.evalFrom s (List.take (↑n) (List.take (↑m) x) ++ List.drop (↑n) (List.take (↑m) x) ++ List.drop (↑m) x) = t
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if bit a m = 0 then if f false true = true then bit b n else 0
    else
      if bit b n = 0 then if f true false = true then bit a m else 0
      else
        have n' := bit a m / 2;
        have m' := bit b n / 2;
        let b₁ := bit a m % 2 = 1;
        let b₂ := bit b n % 2 = 1;
        have r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    bit (f a b) (bitwise f m n)

Tactic:
simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit,
    ite_false]

Goal state after:
f : Bool → Bool → Bool
a : Bool
m : ℕ
b : Bool
n : ℕ
ham : bit a m ≠ 0
hbn : bit b n ≠ 0
⊢ (if f a b = true then bitwise f m n + bitwise f m n + 1 else bitwise f m n + bitwise f m n) =
    bit (f a b) (bitwise f m n)
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
hg :
  ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop,
      ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₂ * (fun x ↦ ‖g x‖) x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

Tactic:
obtain ⟨c₄, hc₄_pos : 0 < c₄, hg⟩ := hg

Goal state after:
f g : ℝ → ℝ
hg✝ : GrowsPolynomially g
hf : f =Θ[atTop] g
hf' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_pos : 0 < c₁
hf_lb : ∀ᶠ (x : ℝ) in atTop, c₁ * ‖g x‖ ≤ ‖f x‖
c₂ : ℝ
hc₂_pos : 0 < c₂
hf_ub : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ c₂ * ‖g x‖
c₃ : ℝ
hc₃_pos : 0 < c₃
c₄ : ℝ
hc₄_pos : 0 < c₄
hg :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x ↦ ‖g x‖) u ∈ Set.Icc (c₃ * (fun x ↦ ‖g x‖) x) (c₄ * (fun x ↦ ‖g x‖) x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Module: Mathlib.Data.Nat.Bitwise

Goal state before:
pp: case pos
m n : ℕ
h : (m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

pp: case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2

Tactic:
· simp only [h, mod_two_eq_zero_iff_testBit_zero, testBit_zero, xor_mod_two_eq_one, decide_not,
      Bool.decide_iff_dist, Bool.not_eq_false', beq_iff_eq, decide_eq_decide]
    lia

Goal state after:
case neg
m n : ℕ
h : ¬(m + n) % 2 = 0
⊢ (m ^^^ n) % 2 = (m + n) % 2
Module: Mathlib.Data.List.ReduceOption

Goal state before:
pp: case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), (tl.concat x).reduceOption = tl.reduceOption ++ x.toList
x : Option α
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList

Tactic:
simp only [concat_eq_append, reduceOption_append] at hl

Goal state after:
case cons
α : Type u_1
hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), tl.reduceOption ++ [x].reduceOption = tl.reduceOption ++ x.toList
⊢ ((hd :: tl).concat x).reduceOption = (hd :: tl).reduceOption ++ x.toList
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 x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
Option.mem_def,

Goal state after:
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 x : ℕ
h : x ∈ rfindOpt fun k ↦ Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : (Code.evaln k cf n <|> Code.evaln k cg n) = Option.some x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
Module: Mathlib.Computability.PartrecBasis

Goal state before:
pp: f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec' fun v ↦ f v.head

Tactic:
by
    obtain ⟨c, rfl⟩ := exists_code.1 hf
    simpa [eval_eq_rfindOpt] using
      rfindOpt <|
        of_prim <|
          Primrec.encode_iff.2 <|
            primrec_evaln.comp <|
              (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
                Primrec.vector_head.comp Primrec.vector_tail

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

Goal state before:
pp: Γ : Type u_1
inst✝ : Inhabited Γ
b : Γ
L R : ListBlank Γ
⊢ write b (mk' L R) = mk' L (ListBlank.cons b R.tail)

Tactic:
simp [mk']

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

Goal state before:
pp: case right.some.some.branch
Γ : 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
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.branch p q₁ q₂) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
cases h : p a v <;> rw [trAux, h] at h₁
      · refine IH₂ _ (TM1.stmts_trans ?_ h₂) h₁ hs.2
        unfold TM1.stmts₁
        exact Finset.mem_insert_of_mem (Finset.mem_union_right _ TM1.stmts₁_self)
      · refine IH₁ _ (TM1.stmts_trans ?_ h₂) h₁ hs.1
        unfold TM1.stmts₁
        exact Finset.mem_insert_of_mem (Finset.mem_union_left _ TM1.stmts₁_self)

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: case neg
α : 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
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
rw [ih]
      constructor <;> rintro ⟨t, u, h, hP, hQ⟩
      · exact ⟨a :: t, u, by tauto⟩
      · rcases t with - | ⟨b, t⟩
        · contradiction
        · 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.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ Tape Bool

Tactic:
refine
      Tape.mk' (L.flatMap (fun x ↦ (enc x).toList.reverse) ⟨n, ?_⟩)
        (R.flatMap (fun x ↦ (enc x).toList) ⟨n, ?_⟩)

Goal state after:
case refine_1
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (enc default).toList.reverse = List.replicate n default

case refine_2
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
⊢ (enc default).toList = List.replicate n default
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α),
    t.length < x.length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
clear star_rmatch_iff

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
IH :
  ∀ (t : List α),
    t.length < x.length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
⊢ P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.write (f (ListBlank.cons a R).head v) q)) v (trTape' enc0 L (ListBlank.cons a R)))
    (trCfg enc enc0
      (stepAux q v (Tape.write (f (Tape.mk' L (ListBlank.cons a R)).head v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]

Goal state after:
case some.write
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun a b ↦ b ∈ step (tr enc dec M) a)
    (stepAux (trNormal dec q) v
      (trTape' enc0 (ListBlank.cons (f a v) L).tail (ListBlank.cons (ListBlank.cons (f a v) L).head R)))
    (trCfg enc enc0 (stepAux q v (Tape.write (f a v) (Tape.mk' L (ListBlank.cons a R)))))
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
⊢ Reaches step (stepNormal f Cont.halt v'.tail) (stepRet k₀ v₀)

Tactic:
apply ReflTransGen.single; rw [e₀]; rfl

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ univ.PairwiseDisjoint (Z ∘ ⇑e)

Tactic:
simpa [← e.injective.injOn.pairwiseDisjoint_image]

Goal state after:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case of_equiv
X : Type u_4
I : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : Finite I
α✝ β✝ : Type u_5
e : α✝ ≃ β✝
IH :
  ∀ {Z D : α✝ → Set X},
    (∀ (i : α✝), IsClosed[inst✝⁴] (Z i)) →
      (∀ (i : α✝), IsClopen (D i)) →
        (∀ (i : α✝), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : α✝), IsClopen (C i)) ∧
                (∀ (i : α✝), Z i ⊆ C i) ∧ (∀ (i : α✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : β✝ → Set X
Z_closed : ∀ (i : β✝), IsClosed[inst✝⁴] (Z i)
D_clopen : ∀ (i : β✝), IsClopen (D i)
Z_subset_D : ∀ (i : β✝), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
⊢ ∃ C,
    (∀ (i : β✝), IsClopen (C i)) ∧
      (∀ (i : β✝), Z i ⊆ C i) ∧ (∀ (i : β✝), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
| of_equiv e IH =>

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
h : PreirreducibleSpace X
U : Set X
hU : IsOpen U
Un : U.Nonempty
⊢ IsOpen (closure U)

Tactic:
· exact ((preirreducibleSpace_iff_open_dense X).mp h hU Un).closure_eq ▸ isOpen_univ

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

Goal state before:
pp: case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⋯
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen hV)

Tactic:
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq

Goal state after:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⋯
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen hV)) ⁻¹' {0}
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso ((Condensed.forget R).map ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)))

Tactic:
dsimp [Condensed.forget, discreteUnderlyingAdj]

Goal state after:
P : TopCat → Prop
R : Type (u + 1)
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((sheafCompose (coherentTopology CompHaus) (CategoryTheory.forget (ModuleCat R))).map
      ((constantSheafAdj (coherentTopology CompHaus) (ModuleCat R) CompHaus.isTerminalPUnit).counit.app
        ((functor R).obj M)))
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.snd i (prod.mk i a b) = b

Tactic:
induction i with
  | fz => simp_all [prod.snd, prod.mk]
  | fs _ i_ih => apply i_ih

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
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
hf : f i = 0
⊢ Icc (f i) (g i) = 0

Tactic:
have hg : g i = 0 := (gs.prop i).resolve_left
            (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_left _ _) h)

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
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ g.toFun i = 0 }
i : ι
h : i ∉ ↑fs + ↑gs
hf : f i = 0
hg : g i = 0
⊢ Icc (f i) (g i) = 0
Module: Mathlib.Data.Fin.Tuple.Embedding

Goal state before:
pp: case neg
α : Type u_1
x✝ : ↑{(a, b) | a ≠ b}
a b : α
h : (a, b) ∈ {(a, b) | a ≠ b}
i j : Fin 2
hij : (fun i ↦ if i = 0 then a else b) i = (fun i ↦ if i = 0 then a else b) j
hi : ¬i = 0
⊢ i = j

Tactic:
· rw [eq_one_of_ne_zero i hi] at hij ⊢
        by_cases hj : j = 0
        · simp [hj] at hij; exact False.elim (h hij.symm)
        · rw [eq_one_of_ne_zero j hj]

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

Goal state before:
pp: case cons
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : (hd :: tl).NodupKeys
⊢ (map (Sigma.map f fun x ↦ id) (hd :: tl)).NodupKeys

Tactic:
simp only [map_cons, nodupKeys_cons] at nd ⊢

Goal state after:
case cons
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih : tl.NodupKeys → (map (Sigma.map f fun x ↦ id) tl).NodupKeys
nd : ¬hd.fst ∈ tl.keys ∧ tl.NodupKeys
⊢ ¬(Sigma.map f (fun x ↦ id) hd).fst ∈ (map (Sigma.map f fun x ↦ id) tl).keys ∧
    (map (Sigma.map f fun x ↦ id) tl).NodupKeys
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries

Tactic:
intro x y

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup x s₁.entries = dlookup x s₂.entries
x : α
y : β x
⊢ y ∈ dlookup x s₁.entries ↔ y ∈ dlookup x s₂.entries
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
hS' : ¬Nonempty ↑S'.toTop
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
x : ↑T'.toTop
⊢ (ConcreteCategory.hom (π' ≫ ConcreteCategory.ofHom { toFun := fun x ↦ h.elim x, continuous_toFun := ⋯ })) x =
    (ConcreteCategory.hom (𝟙 T')) x

Tactic:
exact h.elim (π' x)

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ∀ (a : α), a ∈ (⟦s₁⟧ ∪ ⟦s₂⟧).keys ↔ a ∈ ⟦s₁⟧.keys ∪ ⟦s₂⟧.keys

Tactic:
by simp [keys]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁✝ s₂✝ : Finmap β
s₁ s₂ : AList β
⊢ ⟦s₁⟧.Disjoint ⟦s₂⟧ → ⟦s₁⟧ ∪ ⟦s₂⟧ = ⟦s₂⟧ ∪ ⟦s₁⟧

Tactic:
intro h
    simp only [AList.toFinmap_eq, union_toFinmap, AList.union_comm_of_disjoint h]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : Finmap β
h : s₁.Disjoint s₃
h' : s₂.Disjoint s₃
h'' : s₁ ∪ s₃ = s₂ ∪ s₃
x : α
this : lookup x (s₁ ∪ s₃) = lookup x (s₂ ∪ s₃)
hs₁ : x ∈ s₁
⊢ lookup x s₁ = lookup x s₂

Tactic:
rwa [lookup_union_left hs₁, lookup_union_left_of_not_in (h _ hs₁)] at this

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 ⋯)
⊢ ((insert i s).inf fun i ↦ (t i).sup (f i)) =
    ((insert i s).pi t).sup fun g ↦ (insert i s).attach.inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)

Tactic:
rw [inf_insert, ih, attach_insert, sup_inf_sup]

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 ⋯)
⊢ ((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 ⋯)) =
    ((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 ⋯)