mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Cofiltered

Goal state before:
pp: 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
⊢ IsTopologicalBasis {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V}

Tactic:
convert! IsTopologicalBasis.iInf_induced hT fun j (x : C.pt) => C.π.app j x using 1

Goal state after:
case e'_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
⊢ C.pt.str = ⨅ i, induced (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) (F.obj i).str

case e'_3
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
⊢ {U | ∃ j, ∃ V ∈ T j, U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V} =
    {S | ∃ U F_1, (∀ i ∈ F_1, U i ∈ T i) ∧ S = ⋂ i ∈ F_1, (fun x ↦ (ConcreteCategory.hom (C.π.app i)) x) ⁻¹' U i}
Module: Mathlib.Topology.Category.CompHausLike.SigmaComparison

Goal state before:
pp: P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ (ConcreteCategory.hom (sigmaComparison X σ)) x a =
    (ConcreteCategory.hom (Pi.π (fun a ↦ X.obj (Opposite.op (of P (σ a)))) a))
      ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a))))
        ((ConcreteCategory.hom
            (X.map
              (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
                  (productIsProduct fun x ↦ Opposite.op (of P (σ x)))).hom))
          x))

Tactic:
this,

Goal state after:
P : TopCat → Prop
inst✝⁶ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst✝⁵ : PreservesFiniteProducts X
α : Type u
inst✝⁴ : Finite α
σ : α → Type u
inst✝³ : (a : α) → TopologicalSpace (σ a)
inst✝² : ∀ (a : α), CompactSpace (σ a)
inst✝¹ : ∀ (a : α), T2Space (σ a)
inst✝ : ∀ (a : α), HasProp P (σ a)
x : X.obj (Opposite.op (of P ((a : α) × σ a)))
a : α
this :
  ∀ (x : ToType (X.obj (∏ᶜ fun a ↦ Opposite.op (of P (σ a))))),
    (ConcreteCategory.hom (Pi.π (fun b ↦ X.obj (Opposite.op (of P (σ b)))) a))
        ((ConcreteCategory.hom (piComparison X fun a ↦ Opposite.op (of P (σ a)))) x) =
      (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a))) x
⊢ (ConcreteCategory.hom (sigmaComparison X σ)) x a =
    (ConcreteCategory.hom (X.map (Pi.π (fun a ↦ Opposite.op (of P (σ a))) a)))
      ((ConcreteCategory.hom
          (X.map
            (opCoproductIsoProduct' (finiteCoproduct.isColimit fun a ↦ of P (σ a))
                (productIsProduct fun x ↦ Opposite.op (of P (σ x)))).hom))
        x)
Module: Mathlib.Topology.FiberPartition

Goal state before:
pp: S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ f ↑↑x = f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)

Tactic:
this,

Goal state after:
S : Type u_1
Y : Type u_2
f : S → Y
inst✝ : TopologicalSpace S
X : Type u_3
g : Y → X
a : Fiber (g ∘ f)
b : Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))
x : ↑↑b
this : f ↑↑x = Fiber.image (f ∘ fun x ↦ ↑x) b
⊢ Fiber.image (f ∘ fun x ↦ ↑x) b = f ↑(Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)
Module: Mathlib.Condensed.Discrete.Colimit

Goal state before:
pp: case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (counitAppApp (Profinite.of (Opposite.unop Y).obj) X)) f)

Tactic:
rw [incl_of_counitAppApp.{u, u + 1}]

Goal state after:
case e_a
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst✝ : PreservesFiniteProducts X
hX : (S : Profinite) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right✝ : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ (fromPUnit S).obj right✝
f :
  LocallyConstant (↑(toProfinite.obj (Opposite.unop Y)).toTop)
    (X.obj (Opposite.op (CompHausLike.of (fun X ↦ TotallyDisconnectedSpace ↑X) PUnit.{u + 1})))
x : Function.Fiber ⇑f
⊢ (ConcreteCategory.hom (X.map (sigmaIncl f x).op))
      ((ConcreteCategory.hom (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj)).inv) ⇑f) =
    counitAppAppImage f x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)

Tactic:
constructor <;> intros <;>
    simp [bitraverse, Bicompr.bitraverse, bitraverse_id_id, functor_norm]

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ traverse (bitraverse (pure ∘ f✝) (pure ∘ f'✝)) x✝ = pure (bimap f✝ f'✝ x✝)

case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ⋯.fix (fixAux f) z x = Fix.approx f (k + 1) x

Tactic:
suffices ∀ x' hwf,
    WellFounded.fix hwf (fixAux f) z x' = Fix.approx f (succ k) x'
    from this _ _

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
z : Upto p
_this : p (k + ↑z)
hk : Nat.find h' = k + ↑z
⊢ ∀ (x' : α) (hwf : WellFounded fun y x ↦ x < y), hwf.fix (fixAux f) z x' = Fix.approx f k.succ x'
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p ↑z
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z

Tactic:
simpa only [not_not, Coe]

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

Goal state before:
pp: case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) none = Comp.mk (Option.traverse f <$> Option.traverse g none)

Tactic:
simp [Option.traverse, Option.mapM, functor_norm]

Goal state after:
case none
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
⊢ pure none = Comp.mk (pure (pure none))
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case some
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Option.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (some val✝) =
    Comp.mk (Option.traverse f <$> Option.traverse g (some val✝))

Tactic:
simp [Option.traverse, Option.mapM, functor_norm]

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p

Tactic:
by
  induction i with
  | fz => rfl
  | fs _ ih =>
    rw [TypeVec.const]
    exact ih

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
m : α → β
f : Filter α
F : f.Realizer
x✝ : Set β
⊢ (∃ b, F.F.f b ⊆ m ⁻¹' x✝) ↔ m ⁻¹' x✝ ∈ f

Tactic:
rw [F.mem_sets]

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

Goal state before:
pp: S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')

Tactic:
let π' := pullback.snd π (y' ▷ ℕ∪{∞})

Goal state after:
S T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
inst✝ : Epi π
this : CompactSpace ↑(S' ⇑(ConcreteCategory.hom π))
S'π : (n : ↑ℕ∪{∞}.toTop) →
  LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ LightProfinite.fibre n (π ≫ snd S ℕ∪{∞}) :=
  fun n ↦ { hom := TopCat.ofHom { toFun := fun x ↦ ↑x n, continuous_toFun := ⋯ } }
y' : LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⟶ S :=
  ConcreteCategory.ofHom { toFun := y ⇑(ConcreteCategory.hom π), continuous_toFun := ⋯ }
π' : pullback π (y' ▷ ℕ∪{∞}) ⟶ LightProfinite.of ↑(S' ⇑(ConcreteCategory.hom π)) ⊗ ℕ∪{∞} := pullback.snd π (y' ▷ ℕ∪{∞})
⊢ ∃ S' T' y' π' g',
    Epi π' ∧
      Epi y' ∧
        π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π ∧
          IsSplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞}) ∧ Epi (cover π')
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ ¬2 < _root_.Set.univ.ncard

Tactic:
Set.two_lt_ncard_iff

Goal state after:
α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ ¬∃ a b c, a ∈ _root_.Set.univ ∧ b ∈ _root_.Set.univ ∧ c ∈ _root_.Set.univ ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
a : α
b b' : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
h' : ⟨a, b'⟩ ∈ l
⊢ b = b'

Tactic:
grind [NodupKeys.eq_of_fst_eq]

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

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
⊢ ∀ (a b : List α'),
    a ≈ b → (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b

Tactic:
introv p

Goal state after:
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
p : a ≈ b
⊢ (Functor.map ofList ∘ Traversable.traverse f) a = (Functor.map ofList ∘ Traversable.traverse f) b
Module: Mathlib.Data.Finmap

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ b, ⟨a, b⟩ ∈ xs) ↔ (a = fst_i ∧ ∃ x, x ≍ snd_i) ∨ ∃ x, ⟨a, x⟩ ∈ xs

Tactic:
refine (or_congr_left <| and_iff_left_of_imp ?_).symm

Goal state after:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a = fst_i → ∃ x, x ≍ snd_i
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₁ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
this : dm₁ = dm₂
⊢ (dm₁, dn₁).2 = (dm₂, dn₂).2

Tactic:
this,

Goal state after:
m n : ℕ
hmn : m.Coprime n
dm₁ dn₁ dm₂ dn₂ : ℕ
hd : dm₂ * dn₁ = dm₂ * dn₂
h₁ : (dm₁ ∣ m ∧ m ≠ 0) ∧ dn₁ ∣ n ∧ n ≠ 0
h₂ : (dm₂ ∣ m ∧ m ≠ 0) ∧ dn₂ ∣ n ∧ n ≠ 0
this : dm₁ = dm₂
⊢ (dm₁, dn₁).2 = (dm₂, dn₂).2
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd :: tl).sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
hd : ι →₀ M
tl : List (ι →₀ M)
IH : x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ tl ↔ ∃ f ∈ tl, f x ≠ 0
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ (hd :: tl) ↔ ∃ f ∈ hd :: tl, f x ≠ 0

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.pairwise_cons] at hl

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ (hd + tl.sum).support = hd.support ⊔ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl

Tactic:
rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]

Goal state after:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : (∀ a' ∈ tl, (_root_.Disjoint on Finsupp.support) hd a') ∧ Pairwise (_root_.Disjoint on Finsupp.support) tl
⊢ _root_.Disjoint hd.support tl.sum.support
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : Pairwise (_root_.Disjoint on Finsupp.support) tl → tl.sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ tl
hl : Pairwise (_root_.Disjoint on Finsupp.support) (hd :: tl)
⊢ (hd :: tl).sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: m n : ℤ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

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

Goal state after:
case ofNat.ofNat
m n : ℕ
⊢ (ofNat m + ofNat n).bodd = ((ofNat m).bodd ^^ (ofNat n).bodd)

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

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

case negSucc.negSucc
m n : ℕ
⊢ (-[m+1] + -[n+1]).bodd = (-[m+1].bodd ^^ -[n+1].bodd)
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
hd : α
tl : List α
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p ((dropWhile p tl).get ⟨0, hl⟩) = true
hl : 0 < (dropWhile p (hd :: tl)).length
⊢ ¬p ((dropWhile p (hd :: tl)).get ⟨0, hl⟩) = true

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
⊢ p x = true

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case cons
α : Type u_1
p q : α → Bool
hd : α
tl : List α
IH : takeWhile p (takeWhile q tl) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) tl
⊢ takeWhile p (takeWhile q (hd :: tl)) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) (hd :: tl)

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case inr
n m l : ℕ
hnl : n ≤ l
hml : m ≤ l
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n m) = Ico l m

Tactic:
rw [eq_nil_of_le hml, filter_le_of_top_le hml]

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

Goal state before:
pp: case cons
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x ∈ hd :: tl
n : ℕ
hn : n ∈ {n | n ≤ (hd :: tl).length}
m : ℕ
hm : m ∈ {n | n ≤ (hd :: tl).length}
h : (fun k ↦ (hd :: tl).insertIdx k x) n = (fun k ↦ (hd :: tl).insertIdx k x) m
⊢ n = m

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α}, (splitBy.loop r l a g []).flatten = g.reverse ++ a :: l
a : α
g : List α
⊢ (splitBy.loop r (b :: l) a g []).flatten = g.reverse ++ a :: b :: l

Tactic:
rw [splitBy.loop, splitByLoop_eq_append [_]]
    split <;> simp [IH]

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈↑x⌉₊ = ⌈x⌉₊

Tactic:
refine (Nat.ceil_eq_iff ?_).2 (mod_cast (Nat.ceil_eq_iff ?_).1 (Eq.refl ⌈x⌉₊))

Goal state after:
case inr.refine_1
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0

case inr.refine_2
K : Type u_1
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
x : ℚ≥0
hx : x ≠ 0
⊢ ⌈x⌉₊ ≠ 0
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac

Tactic:
have : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1 := by
    refine multiplicity_eq_of_dvd_of_not_dvd ?_ (minFac_sq_ndvd_gcd_choose_of_isPrimePow h)
    simpa using minFac_dvd_gcd_choose_of_isPrimePow h

Goal state after:
n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
this : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1
⊢ (Icc 1 (n - 1)).gcd n.choose = n.minFac
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
⊢ Set.range (nth p) = insert 0 (Set.ofPred p)

Tactic:
simpa only [← List.getD_eq_getElem?_getD, ← nth_eq_getD_sort hf, mem_sort,
    Set.Finite.mem_toFinset] using! Set.range_list_getD (hf.toFinset.sort (· ≤ ·)) 0

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

Goal state before:
pp: n : ℕ
h : IsPrimePow n
ne_zero : (Icc 1 (n - 1)).gcd n.choose ≠ 0
isPrime : Nat.Prime n.minFac
this : multiplicity n.minFac ((Icc 1 (n - 1)).gcd n.choose) = 1
⊢ ∏ p, ↑p ^ ((Icc 1 (n - 1)).gcd n.choose).factorization ↑p = n.minFac

Tactic:
simp [← Nat.multiplicity_eq_factorization isPrime ne_zero, this]

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

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

Tactic:
rw [sub', ZNum.cast_bit0, cast_sub' a b]
    have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]
    simpa [sub_eq_add_neg] using this

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ LiftP p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
constructor
  · rintro ⟨y, hy⟩
    rcases h : y with ⟨a, f⟩
    refine ⟨a, fun i j => (f i j).val, ?_, fun i j => (f i j).property⟩
    rw [← hy, h, map_eq]
    rfl
  rintro ⟨a, f, xeq, pf⟩
  use ⟨a, fun i j => ⟨f i j, pf i j⟩⟩
  rw [xeq]; rfl

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

Goal state before:
pp: case inl.succ
l r₁ : ℕ
H : l + r₁ ≤ 1
n✝ : ℕ
h₁ : r₁ ≤ n✝ + 1
h₂ : l + (n✝ + 1) ≤ 1 ∨ n✝ + 1 ≤ delta * l
h : ¬l + (n✝ + 1) ≤ 1
⊢ l ≤ delta * (n✝ + 1)

Tactic:
· exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑↑n = ↑n

Tactic:
to_of_int

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑n = ↑n
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x

Tactic:
· simp only [liftP_iff']
    cases h
    subst x
    tauto

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

Goal state before:
pp: case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d

Tactic:
this,

Goal state after:
case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
h₂ : ↑r₂ + ↑d < 2 * ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : ↑F F.M
i : F.Idx
⊢ ichildren i (M.mk x) = x.iget i

Tactic:
dsimp only [ichildren, PFunctor.Obj.iget]
  congr with h

Goal state after: