mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.LightProfinite.Injective

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : Type u_3
T : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : CompactSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : CompactSpace Y
inst✝⁶ : T2Space Y
inst✝⁵ : TotallyDisconnectedSpace Y
inst✝⁴ : TopologicalSpace S
inst✝³ : T2Space S
inst✝² : Finite S
inst✝¹ : TopologicalSpace T
inst✝ : T2Space T
f : X → Y
hf : Continuous[inst✝¹⁰, inst✝⁸] f
f_inj : Function.Injective f
f' : S → T
f'_surj : Function.Surjective f'
g : X → S
hg : Continuous[inst✝¹⁰, inst✝⁴] g
g' : Y → T
hg' : Continuous[inst✝⁸, inst✝¹] g'
h_comm : g' ∘ f = f' ∘ g
⊢ ∃ k, Continuous[inst✝⁸, inst✝⁴] k ∧ f' ∘ k = g' ∧ k ∘ f = g

Tactic:
by
  -- `T` is finite because it admits a surjection from a finite set
  have : Finite T := Finite.of_surjective f' f'_surj
  -- define the closed partition `Z` so `Z i` is the image under `f` of the fiber of `g` at `i`
  let Z : S → Set Y := fun i ↦ f '' g ⁻¹' {i}
  have Z_closed (i) : IsClosed (Z i) :=
    (IsClosedEmbedding.isClosed_iff_image_isClosed (Continuous.isClosedEmbedding hf f_inj)).mp
    (IsClosed.preimage hg isClosed_singleton)
  have Z_disj : univ.PairwiseDisjoint Z := by
    rw [Set.pairwiseDisjoint_iff]
    simp only [image_inter_nonempty_iff, Z]
    rintro _ _ _ _ ⟨_, rfl, ⟨_, rfl, hy⟩⟩
    rw [f_inj hy]
  -- define `D i` to be the fiber of `g'` at `f' i`
  let D : S → Set Y := fun i ↦ g' ⁻¹' ({f' i})
  -- each `D i` is clopen
  have D_clopen i : IsClopen (D i) := IsClopen.preimage (isClopen_discrete {f' i}) hg'
  -- each `Z i` is contained in `D i`
  have Z_subset_D i : Z i ⊆ D i := by
    intro z hz
    rw [mem_preimage, mem_singleton_iff]
    obtain ⟨x, _, _⟩ := (mem_image _ _ _).mp hz
    have h_comm' : g' (f x) = f' (g x) := congr_fun h_comm x
    simp_all
  -- obtain a clopen partition `C` of `Y` such that `Z i ⊆ C i ⊆ D i`.
  obtain ⟨C, C_clopen, Z_subset_C, C_subset_D, C_cover_D, C_disj⟩ :=
    exists_clopen_partition_of_clopen_cover Z_closed D_clopen Z_subset_D Z_disj
  have D_cover_univ : univ ⊆ (⋃ i, D i) := by
    intro y _
    simp only [mem_iUnion]
    obtain ⟨s, hs⟩ := f'_surj (g' y)
    grind
  have C_cover_univ : ⋃ i, C i = univ := univ_subset_iff.mp (subset_trans D_cover_univ C_cover_D)
  -- define k to be the unique map sending C i to ψ i
  have h_glue (i j : S) (x : Y) (hxi : x ∈ C i) (hxj : x ∈ C j) : i = j := by
    rw [Set.pairwiseDisjoint_iff] at C_disj
    exact C_disj (by simp) (by simp) ⟨x, by grind⟩
  refine ⟨liftCover C (fun i _ ↦ i) h_glue C_cover_univ, IsLocallyConstant.continuous ?_, ?_, ?_⟩
  · rw [IsLocallyConstant.iff_isOpen_fiber]
    intro s
    convert! (C_clopen s).2
    ext y
    simp [preimage_liftCover]
  · ext y
    -- y is contained in C i for some i
    have hy : y ∈ ⋃ i, C i := by simp [C_cover_univ]
    obtain ⟨i, hi⟩ := mem_iUnion.mp hy
    simpa [liftCover_of_mem hi] using symm (C_subset_D i hi)
  · ext x
    simp [liftCover_of_mem <| Z_subset_C (g x) (by simpa [mem_image] using ⟨x, rfl, rfl⟩)]

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β
xs : t α
⊢ toList (f <$> xs) = f <$> toList xs

Tactic:
by
  simp only [toList_spec, Free.map_eq_map, foldMap_hom, foldMap_map, FreeMonoid.ofList_toList,
    FreeMonoid.map_of, Function.comp_def]

Goal state after:
Module: Mathlib.Control.LawfulFix

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

Tactic:
intro hh

Goal state after:
case pos.mp
α : 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 : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a
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
⊢ (∃ i, b ∈ approx (⇑f) i a) → b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
intro hh

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
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
simp only [callCC, ExceptT.callCC, @callCC_dummy m _]

Goal state after:
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.mk dummy✝.run = dummy✝
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
simp only [Part.fix_def f h₀]
    constructor <;> intro hh
    · exact ⟨_, hh⟩
    have h₁ := Nat.find_spec h₀
    rw [dom_iff_mem] at h₁
    obtain ⟨y, h₁⟩ := h₁
    replace h₁ := approx_mono' f _ _ h₁
    suffices y = b by
      subst this
      exact h₁
    obtain ⟨i, hh⟩ := hh
    revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
    wlog case : i ≤ j
    · rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
    replace hh := approx_mono f case _ _ hh
    apply Part.mem_unique h₁ hh

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

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (fibres π σ)ᶜ

Tactic:
fibres_compl_eq_iUnion π σ hσ'

Goal state after:
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i})
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
p : α ⟹ «repeat» n Prop
i : Fin2 n
x : Subtype_ p i
⊢ (toSubtype p ⊚ ofSubtype p) i x = id i x

Tactic:
induction i <;> simp only [id, toSubtype, comp, ofSubtype] at *

Goal state after:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), toSubtype p a✝ (ofSubtype p a✝ x) = x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ toSubtype (dropFun p) a✝ (ofSubtype (dropFun p) a✝ x) = x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝¹ : CommRing R
X : LightCondMod R
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi ((lightProfiniteToLightCondSet ⋙ free R).map (cover π))
g : (lightProfiniteToLightCondSet ⋙ free R).obj T ⟶ X
r_inf : T ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
σ : S ⟶ LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞})
hr : LightProfinite.fibreIncl ∞ (π ≫ snd S ℕ∪{∞}) ≫ r_inf = 𝟙 (LightProfinite.fibre ∞ (π ≫ snd S ℕ∪{∞}))
⊢ Cocone
    (parallelPair (lightProfiniteToLightCondSet.map (CompHausLike.pullback.fst π π))
        (lightProfiniteToLightCondSet.map (CompHausLike.pullback.snd π π)) ⋙
      free R)

Tactic:
by
  refine Cocone.ofCofork (Cofork.ofπ (g -
    (lightProfiniteToLightCondSet ⋙ free R).map
      (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd _ _)) ≫ g +
    (lightProfiniteToLightCondSet ⋙ free R).map
      (r_inf ≫ LightProfinite.fibreIncl ∞ (π ≫ snd _ _) ≫ π ≫ fst _ _ ≫ σ ≫
        LightProfinite.fibreIncl ∞ (π ≫ snd _ _)) ≫ g) ?_)
  rw [← cancel_epi ((lightProfiniteToLightCondSet ⋙ free R).map <| cover π)]
  apply (isColimitOfPreserves (lightProfiniteToLightCondSet ⋙ free R)
      (coproductIsColimit _ _)).hom_ext
  rintro ⟨⟨⟩⟩
  · simp [← map_comp_assoc, -Functor.map_comp]
    rfl
  · -- simp? [← map_comp_assoc, -Functor.map_comp] says:
    simp only [pair_obj_right, mapCocone_ι_app,
      Functor.comp_map, parallelPair_obj_zero, parallelPair_obj_one, parallelPair_map_left,
      Preadditive.comp_add, Preadditive.comp_sub, ← map_comp_assoc, parallelPair_map_right]
    have : cover π = (BinaryCofan.IsColimit.desc' (coproductIsColimit _ _)
        (CompHausLike.pullback.lift _ _ (𝟙 T) (𝟙 T) (by simp))
        (CompHausLike.pullback.lift _ _
          ((CompHausLike.pullback.fst _ _) ≫ LightProfinite.fibreIncl _ _)
          ((pullback.snd _ _) ≫ LightProfinite.fibreIncl _ _)
          (by simp [pullback.condition]))).val := rfl
    -- simp? [this, ← Functor.map_comp] says:
    simp only [this, pair_obj_left, pair_obj_right, BinaryCofan.IsColimit.desc'_coe,
      IsColimit.fac, BinaryCofan.mk_inr, ← Functor.map_comp,
      pullback.lift_fst, IsColimit.fac_assoc, assoc,
      pullback.lift_snd]
    -- simp? [-Functor.map_comp, ← assoc, hr] says:
    simp only [← assoc, hr, id_comp, sub_self, zero_add]
    simp [pullback.condition]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (dlookup a l).toList

Tactic:
rw [← head?_lookupAll]

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ lookupAll a l = (lookupAll a l).head?.toList
Module: Mathlib.Data.Finsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ f.neLocus g = g.neLocus f

Tactic:
simp_rw [neLocus, Finset.union_comm, ne_comm]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
← h

Goal state after:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 ↦ x1 < x2) (↑t) (d :: ds)
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
⊢ CPRankMax 1 x

Tactic:
by
  have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero
  rwa [zero_add, add_zero] at h'

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C n

Tactic:
← bit_decomp n

Goal state after:
C : ℤ → Sort u
n : ℤ
h : (b : Bool) → (n : ℤ) → C (bit b n)
⊢ C (bit n.bodd n.div2)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: b : Bool
n : ℕ
⊢ (↑(Nat.bit b n)).testBit 0 = b

Tactic:
apply Nat.testBit_bit_zero

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔ x ∈ map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ico (a - v) (b - v) | r ∣ x})

Tactic:
mem_map,

Goal state after:
a b r v x : ℤ
⊢ x ∈ {x ∈ Ico a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ico (a - v) (b - v) | r ∣ x}, { toFun := fun x ↦ x + v, inj' := ⋯ } a_1 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔ x ∈ map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
mem_map,

Goal state after:
a b r v x : ℤ
⊢ x ∈ {x ∈ Ioc a b | x ≡ v [ZMOD r]} ↔
    ∃ a_1 ∈ {x ∈ Ioc (a - v) (b - v) | r ∣ x}, { toFun := fun x ↦ x + v, inj' := ⋯ } a_1 = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ ⌈(↑(b % r) - ↑(v % r)) / ↑r⌉ = ↑0

Tactic:
rw [cast_zero, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', zero_mul,
      tsub_nonpos, ← neg_eq_neg_one_mul, neg_lt_sub_iff_lt_add, ← cast_add, cast_lt, cast_le]

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ v % r < r + b % r ∧ b % r ≤ v % r
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l = [] ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
induction l using List.reverseRecOn <;> simp [rtakeWhile]

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

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

Tactic:
by
  simp_rw [rtakeWhile, reverse_reverse]

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

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (head✝ :: (tl ++ [a])) #[] = head✝ :: (tl ++ [f a])

Tactic:
rw [modifyLast.go]

Goal state after:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
q k : ℕ
w : List α
per_q : w.HasPeriod q
per_plus : w.HasPeriod (k + q)
⊢ (drop q w).HasPeriod k

Tactic:
by
  rw [hasPeriod_iff_getElem?] at per_plus per_q ⊢
  simp only [length_drop, getElem?_drop]
  intro i i_lt
  calc
     w[q + i]? = w[i + q]? := congrArg (getElem? w) (add_comm q i)
     _ = w[i]? := (per_q i (by lia)).symm
     _ = w[i + (k + q)]? := per_plus i (by lia)
     _ = w[q + (i + k)]? := congr_arg (getElem? w) (by lia)

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

Goal state before:
pp: l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ mulRightLinearMap l R a ^ (n + 1) = mulRightLinearMap l R (a ^ (n + 1))

Tactic:
by
    rw [pow_succ, pow_succ', mulRightLinearMap_mul, Module.End.mul_eq_comp, pow_mulRightLinearMap]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Dvd

Goal state before:
pp: p a b : ℕ
hp : Prime p
hb : b < p
ha : a ≤ b
⊢ p.Coprime (b.choose a)

Tactic:
rw [Nat.choose_eq_descFactorial_div_factorial]
  exact (hp.coprime_descFactorial_of_lt_of_le hb ha).coprime_div_right
    (Nat.factorial_dvd_descFactorial b a)

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case neg
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
h : (k % p, k / p) ∉ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ 0 = (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
· rw [mem_product, mem_range, mem_range, not_and_or, Nat.lt_succ_iff, not_le, not_lt] at h
    cases h <;> simp [choose_eq_zero_of_lt (by tauto)]

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

Goal state before:
pp: p : PosNum
⊢ (pos p).succ'.pred'.toZNumNeg = ZNum.neg p

Tactic:
rw [PosNum.pred'_succ']; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a + ↑b = -(-↑a + -↑b)

Tactic:
neg_add_rev,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑a + ↑b = - -↑b + - -↑a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (↑q + ↑q) = ↑n + ↑n

Tactic:
rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz 0 rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 0 ∧ BalancedSz (0 + 0 + 1) rr.size

Tactic:
rw [le_antisymm (balancedSz_zero.1 this.symm) rr0]

Goal state after:
case pos.inl.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
rr0 : rr.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
this : BalancedSz 0 rr.size
rl0 : rl.size = 0
⊢ BalancedSz 0 0 ∧ BalancedSz (0 + 0 + 1) 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node3L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
simp [node3L, all_node', and_assoc]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.dual.findMax = t.findMin

Tactic:
rw [← findMin_dual, dual_dual]

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = dest P (dropFun g <$$> x)

Tactic:
M.dest_map

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ g <$$> dest P x = (dropFun g ::: fun x ↦ dropFun g <$$> x) <$$> dest P x
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n : ℕ+
m : ℕ
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
by
  let u := factorMultiset n
  have : n = u.prod := (prod_factorMultiset n).symm
  rw [this, ← PrimeMultiset.prod_smul]
  repeat' rw [PrimeMultiset.factorMultiset_prod]

Goal state after:
Module: Mathlib.Data.PNat.Find

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n' : ℕ
⊢ (∃ a b x, p ⟨a, b⟩) ↔ ∃ h, p ⟨n', h⟩

Tactic:
by
      simp_rw [mk_coe, @exists_comm (_ < _) (_ = _), exists_prop, exists_eq_left']

Goal state after:
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = x * y

Tactic:
← h

Goal state after:
case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h : wp * zp + zp + wp = x * y
⊢ wp + zp + wp * zp = wp * zp + zp + wp
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
    · obtain ⟨c, ha⟩ := exists_gt a
      exact ⟨⟨i, c⟩, right _ ha, left _ _ h⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
rcases H with (rfl | rfl)
  · exact Or.inl rfl
  · exact Or.inr rfl

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁✝ a₂ : (P F).M α
ra₁a₂ : r a₁✝ a₂
b₁eq : b₁ = g <$$> a₁✝
b₂eq : b₂ = g <$$> a₂
a₁ : (P F).M α
⊢ ∀ (b : (P F).M α), r a₁ b → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> b)

Tactic:
a₂

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂✝ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁✝ a₂✝ : (P F).M α
ra₁a₂ : r a₁✝ a₂✝
b₁eq : b₁ = g <$$> a₁✝
b₂eq : b₂ = g <$$> a₂✝
a₁ a₂ : (P F).M α
⊢ r a₁ a₂ → Quot.mk r' (g <$$> a₁) = Quot.mk r' (g <$$> a₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Sigma

Goal state before:
pp: n : ℕ
A : Type u
F : A → TypeVec.{u} n → Type u
inst✝ : (α : A) → MvQPF (F α)
⊢ ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (p : ↑(Sigma.P F) α), Sigma.abs F (f <$$> p) = f <$$> Sigma.abs F p

Tactic:
rintro α β f ⟨x, g⟩; simp only [Sigma.abs, MvPFunctor.map_eq]
                simp only [(· <$$> ·), ← abs_map, ← MvPFunctor.map_eq]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
⊢ ∀ (x y : Cofix F α), r x y → x = y

Tactic:
let r' (x y) := x = y ∨ r x y

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
⊢ ∀ (x y : Cofix F α), r x y → x = y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y

Tactic:
let r' (x y) := x = y ∨ r x y

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : Cofix F → Cofix F → Prop := fun x y ↦ x = y ∨ r x y
⊢ ∀ (x y : Cofix F), r x y → x = y
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
⊢ 0 = ↑(Int.sign 0)

Tactic:
Int.sign_zero,

Goal state after:
case inr.inl
⊢ 0 = ↑0
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = 1

Tactic:
sign_of_pos (inv_pos.mpr hp)

Goal state after:
case inr.inr
r : ℝ
hp : 0 < r
⊢ 1 = 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ (TypeVec.id ::: Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x)) <$$> g Sum.inl Sum.inr x =
    g _root_.id (corec₁ g) x

Tactic:
← h

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x