mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).map
      ((constantSheafAdj (coherentTopology LightProfinite) (ModuleCat R) isTerminalPUnit).counit.app
        ((functor R).obj M)))

Tactic:
← constantSheafAdj_counit_w

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
⊢ IsIso
    ((constantCommuteCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).hom.app
        (((functor R).obj M).obj.obj (op (LightProfinite.of PUnit.{u + 1}))) ≫
      (constantSheafAdj (coherentTopology LightProfinite) (Type u) isTerminalPUnit).counit.app
        ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj
          ((functor R).obj M)))
Module: Mathlib.Condensed.Discrete.Module

Goal state before:
pp: P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
⊢ IsIso
    ((constantSheafAdj (coherentTopology LightProfinite) (Type u) isTerminalPUnit).counit.app
      ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M)))

Tactic:
have : (constantSheaf (coherentTopology LightProfinite.{u}) (Type u)).Full :=
    inferInstanceAs (discrete (Type u)).Full

Goal state after:
P : TopCat → Prop
R : Type u
inst✝ : Ring R
M : ModuleCat R
this✝ : (constantSheaf (coherentTopology LightProfinite) (Type u)).Faithful
this : (constantSheaf (coherentTopology LightProfinite) (Type u)).Full
⊢ IsIso
    ((constantSheafAdj (coherentTopology LightProfinite) (Type u) isTerminalPUnit).counit.app
      ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M)))
Module: Mathlib.Condensed.Epi

Goal state before:
pp: A : Type u'
inst✝⁸ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁷ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁶ : ConcreteCategory A FA
inst✝⁵ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁴ : (coherentTopology CompHaus).WEqualsLocallyBijective A
inst✝³ : HasSheafify (coherentTopology CompHaus) A
inst✝² : (coherentTopology CompHaus).HasSheafCompose (CategoryTheory.forget A)
inst✝¹ : Balanced (Sheaf (coherentTopology CompHaus) A)
inst✝ : PreservesFiniteProducts (CategoryTheory.forget A)
⊢ (∀ (X_1 : CompHaus) (y : ToType (Y.obj.obj (op X_1))),
      ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (hom (f.hom.app (op X'))) x = (hom (Y.obj.map (op φ))) y) ↔
    ∀ (S : CompHaus) (y : ToType (Y.obj.obj (op S))),
      ∃ S' φ, ∃ (_ : Function.Surjective ⇑(hom φ)), ∃ x, (hom (f.hom.app (op S'))) x = (hom (Y.obj.map (op φ))) y

Tactic:
((CompHaus.effectiveEpi_tfae _).out 0 2 :)

Goal state after:
Module: Mathlib.Topology.Category.Sequential

Goal state before:
pp: X✝ : Type u
inst✝¹ : TopologicalSpace X✝
inst✝ : SequentialSpace X✝
X Y : Sequential
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ }) ≫
      InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) =
    𝟙 Y

Tactic:
by
    ext x
    exact f.apply_symm_apply x

Goal state after:
Module: Mathlib.Topology.Category.CompactlyGenerated

Goal state before:
pp: X✝ : Type w
inst✝¹ : TopologicalSpace X✝
inst✝ : UCompactlyGeneratedSpace X✝
X Y : CompactlyGenerated
f : ↑X.toTop ≃ₜ ↑Y.toTop
⊢ ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ } ≫ ofHom { toFun := ⇑f, continuous_toFun := ⋯ } = 𝟙 Y

Tactic:
by
    ext x
    exact f.apply_symm_apply x

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

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

Tactic:
(simp! [Sum.traverse, map_id, functor_norm] <;> rfl)

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

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

Tactic:
(simp! [Sum.traverse, map_id, functor_norm] <;> rfl)

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case nil
α : Type u
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) []) = []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case nil
α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
n : ℕ
⊢ (List.foldl (fun l x ↦ { down := l.down + 1 }) { down := n } []).down = [].length + n

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : α → γ → m α
a : α
l : t β
⊢ foldlm f a (g <$> l) = foldlm (fun x y ↦ f x (g y)) a l

Tactic:
by
  simp only [foldlm, foldMap_map, Function.comp_def, Function.flip_def]

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

Goal state before:
pp: n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) ↔ ∃ u, q u

Tactic:
by
  constructor <;> rintro ⟨u, h₂⟩
  · refine ⟨f <$$> u, ?_⟩
    apply (h₁ u).mp h₂
  · refine ⟨g <$$> u, ?_⟩
    rw [h₁]
    simp only [MvFunctor.map_map, h₀, LawfulMvFunctor.id_map, h₂]

Goal state after:
Module: Mathlib.Control.Monad.Cont

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

Tactic:
by intros; ext; simp [callCC, OptionT.callCC, @callCC_dummy m _]

Goal state after:
Module: Mathlib.Data.Bool.Count

Goal state before:
pp: l : List Bool
hl : IsChain (fun x1 x2 ↦ x1 ≠ x2) l
h2 : Even l.length
b : Bool
⊢ 2 * count b l = l.length

Tactic:
rw [← count_not_add_count l b, hl.count_not_eq_count h2, two_mul]

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: case nil
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ s ∈ enum [] ↔ ∀ x ∈ s, x ∈ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
f : α → Option α
acc : Array α
⊢ go f [] acc = acc.toListAppend (lookmap f [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
f : α → Option α
l₁ l₂ : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) []
⊢ lookmap f [] ~ lookmap f []

Tactic:
| nil =>

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

Goal state before:
pp: case swap.some.none
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
h₂ : f b = none
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

pp: case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)

Tactic:
· simpa [lookmap_cons_some _ _ h₁, h₂] using Perm.swap _ _ _

Goal state after:
case swap.some.some
α : Type u_1
f : α → Option α
l₁ l₂ : List α
a b : α
l : List α
H : Pairwise (fun a b ↦ ∀ (c : α), c ∈ f a → ∀ (d : α), d ∈ f b → a = b ∧ c = d) (b :: a :: l)
c : α
h₁ : f a = some c
d : α
h₂ : f b = some d
⊢ lookmap f (b :: a :: l) ~ lookmap f (a :: b :: l)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ (dlookup a []).isSome = true ↔ a ∈ [].keys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
⊢ b ∈ dlookup a [] → ⟨a, b⟩ ∈ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ Option.map (Sigma.mk a) (dlookup a []) = find? (fun s ↦ decide (a = s.fst)) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (f a) (map (Sigma.map f g) []) = Option.map (g a) (dlookup a [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
nd : [].NodupKeys
⊢ (map (Sigma.map f fun x ↦ id) []).NodupKeys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
a : α
⊢ dlookup a ([] ++ l₂) = (dlookup a []).or (dlookup a l₂)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
⊢ ofList <$> Traversable.traverse f [] = ofList <$> Traversable.traverse f []

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ a ∈ [].toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬⟨a, b⟩ ∈ l
⊢ ∀ (a_1 : Sigma β), a_1 ∈ l → (if a = a_1.fst then some ⟨a, b⟩ else none) = none

Tactic:
by
    grind

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
h : ¬a ∈ [].keys
⊢ kerase a [] = []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
h : a ∈ [].keys
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ [] = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a [] = l₁ ++ l₂

Tactic:
| nil =>

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

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ a ∈ s ↔ a ∈ (image (const β✝) s).sup fun f ↦ image f t

Tactic:
mem_sup

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ a ∈ s ↔ ∃ i ∈ image (const β✝) s, a ∈ image i t
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ a ∈ s ↔ ∃ i ∈ image (const β✝) s, a ∈ image i t

Tactic:
refine ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, ?_⟩

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
ht : t.Nonempty
a : α✝
⊢ (∃ i ∈ image (const β✝) s, a ∈ image i t) → a ∈ s
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ a ∈ t ↔ a ∈ (image (const α✝ id) s).sup fun f ↦ image f t

Tactic:
mem_sup

Goal state after:
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
hs : s.Nonempty
a : β✝
⊢ a ∈ t ↔ ∃ i ∈ image (const α✝ id) s, a ∈ image i t
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg.nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
⊢ kerase a (kerase a' []) = kerase a' (kerase a [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
nd : [].NodupKeys
⊢ ¬a ∈ (kerase a []).keys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
⊢ dlookup a (kerase a' []) = dlookup a []

Tactic:
| nil =>

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

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
bh : β a
h₂ : ¬a' = a
⊢ dlookup a (kerase a' (⟨a, bh⟩ :: tl)) = dlookup a (⟨a, bh⟩ :: tl)

Tactic:
simp [h₂]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
l₂ : List (Sigma β)
h₁ : a ∈ (s :: l₁).keys
h₂ : a = s.fst
⊢ kerase a (s :: l₁ ++ l₂) = kerase a (s :: l₁) ++ l₂

Tactic:
simp [h₂]

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
x : α
⊢ sizeOf (kerase x []) ≤ sizeOf []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
⊢ (foldr (fun x ↦ kinsert x.fst x.snd) l' []).NodupKeys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ dlookup a [].dedupKeys = dlookup a []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
inst✝ : SizeOf α
l r : List α
a : α
h : sizeOf l ≤ sizeOf r
⊢ sizeOf (a :: l) ≤ sizeOf (a :: r)

Tactic:
by
  rw [cons.sizeOf_spec, cons.sizeOf_spec]
  exact Nat.add_le_add_iff_left.mpr h

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝¹ : DecidableEq α
inst✝ : SizeOf (Sigma β)
⊢ sizeOf [].dedupKeys ≤ sizeOf []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ ([].kunion l₂).keys ↔ a ∈ [].keys ∨ a ∈ l₂.keys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₂ : List (Sigma β)
nd₁ : [].NodupKeys
nd₂ : l₂.NodupKeys
⊢ ([].kunion l₂).NodupKeys

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ l : List (Sigma β)
⊢ [].kunion l ~ [].kunion l

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : a ∈ [].keys
⊢ dlookup a ([].kunion l₂) = dlookup a []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : ¬a ∈ [].keys
⊢ dlookup a ([].kunion l₂) = dlookup a l₂

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₂ : List (Sigma β)
⊢ b ∈ dlookup a ([].kunion l₂) ↔ b ∈ dlookup a [] ∨ ¬a ∈ [].keys ∧ b ∈ dlookup a l₂

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
⊢ pimage f s = image (fun x ↦ (f ↑x).get ⋯) {x ∈ s | (f x).Dom}.attach

Tactic:
aesop (add simp Part.mem_eq)

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (List.map Prod.toSigma f.graph.toList).NodupKeys

Tactic:
List.NodupKeys,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
⊢ (List.map Prod.toSigma f.graph.toList).keys.Nodup
Module: Mathlib.Data.Finsupp.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
⊢ [].sum.support ⊆ foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
x : ι
⊢ x ∈ foldr (fun x1 x2 ↦ x1.support ∪ x2) ∅ [] ↔ ∃ f ∈ [], f x ≠ 0

Tactic:
| nil =>

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

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddZeroClass M
hl : Pairwise (_root_.Disjoint on Finsupp.support) []
⊢ [].sum.support = foldr (fun x1 x2 ↦ x1.support ⊔ x2) ∅ []

Tactic:
| nil =>

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ Multiset.Pairwise (Disjoint on Finsupp.support) ↑l

Tactic:
Multiset.pairwise_coe_iff_pairwise,

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ List.Pairwise (Disjoint on Finsupp.support) l
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: n : ℤ
⊢ (-n).bodd = n.bodd

Tactic:
cases n <;> simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc]

Goal state after:
case ofNat
a✝ : ℕ
⊢ a✝.bodd = (ofNat a✝).bodd

case negSucc
a✝ : ℕ
⊢ (↑(a✝ + 1)).bodd = -[a✝+1].bodd
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ (a ^^^ b) = b

Tactic:
← xor_assoc,

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ a ^^^ a ^^^ b = b
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ Function.IsFixedPt (fun x ↦ x ^^^ a) b ↔ a = 0

Tactic:
by
  rw [xor_right_eq, isFixedPt_xor_left_iff]

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

Goal state before:
pp: case ofNat
n a✝ : ℕ
⊢ ↑a✝ <<< n = ↑a✝ * 2 ^ n

Tactic:
grind [Int.shiftLeft_eq']

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
hl : 0 < (dropWhile p []).length
⊢ ¬p ((dropWhile p []).get ⟨0, hl⟩) = true

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
⊢ (dropWhile p []).length ≤ [].length

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ dropWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

Tactic:
| nil =>

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

Goal state before:
pp: case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : ¬p hd = true
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
simp [h_p_hd]

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (x : α), x ∈ [] → p x = true

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
⊢ takeWhile p [] = [] ↔ ∀ (hl : 0 < [].length), ¬p ([].get ⟨0, hl⟩) = true

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i ↦ f (↑i) ([].get i)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
f : ℕ → α → m PUnit
arr : Array PUnit
⊢ mapIdxMAux' f arr.size [] = mapIdxM.go f [] arr *> pure PUnit.unit

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
p q : α → Bool
⊢ takeWhile p (takeWhile q []) = takeWhile (fun a ↦ decide (p a = true ∧ q a = true)) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
⊢ take ([].length - n) [] = (drop n [].reverse).reverse

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
n : ℕ
⊢ drop ([].length - n) [] = (take n [].reverse).reverse

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ ((l₁ ++ l₂).rdrop l₂.length).rdrop k = l₁.rdrop k

Tactic:
rdrop_append_length

Goal state after:
α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ l₁.rdrop k = l₁.rdrop k
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case e'_2.e'_6
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ range' m (l - m) = range' (n + 1 * (m - n)) ?convert_3

pp: case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + ?convert_3

pp: case convert_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ ℕ

Tactic:
· rw [Nat.one_mul, Nat.add_sub_cancel' hnm]

Goal state after:
case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)
Module: Mathlib.Data.List.ModifyLast

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
r : Array α
⊢ go f ([] ++ [a]) r = r.toListAppend (go f ([] ++ [a]) #[])

Tactic:
| nil =>

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

Goal state before:
pp: case cons
α : Type u_1
f : α → α
a : α
r : Array α
hd : α
tl : List α
⊢ (r.push hd).toListAppend (go f (tl ++ [a]) #[]) = r.toListAppend ((#[].push hd).toListAppend (go f (tl ++ [a]) #[]))

Tactic:
simp only [Array.toListAppend_eq, Array.toList_push, nil_append,
      append_assoc]

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

Goal state before:
pp: case nil
α : Type u_1
f : α → α
a : α
⊢ modifyLast f ([] ++ [a]) = [] ++ [f a]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
f : α → α
l₁ : List α
x✝ : [] ≠ []
⊢ modifyLast f (l₁ ++ []) = l₁ ++ modifyLast f []

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u_1
f : α → α
l₁ : List α
hd : α
x✝ : [hd] ≠ []
⊢ modifyLast f (l₁ ++ [hd]) = l₁ ++ modifyLast f [hd]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u
β : Type v
bs : List β
⊢ zipWithLeft Prod.mk [] bs = (zipWithLeft' Prod.mk [] bs).fst

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
x : α
hx : ¬x ∈ []
n : ℕ
hn : n ∈ {n | n ≤ [].length}
m : ℕ
hm : m ∈ {n | n ≤ [].length}
h : (fun k ↦ [].insertIdx k x) n = (fun k ↦ [].insertIdx k x) m
⊢ n = m

Tactic:
| nil =>

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

Goal state before:
pp: case cons.nil
α : Type u
β : Type v
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) [] = (zipWithLeft' Prod.mk (head✝ :: atl) []).fst

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α → α
g : γ → α → α
hfg : Set.range f ⊆ Set.range g
a : α
⊢ foldr f a [] ∈ Set.range (foldr g a)

Tactic:
| nil =>

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

Goal state before:
pp: case refine_2.nil
α : Type u_1
L : List (List α)
f : List α
⊢ [] ∈ [].sections

Tactic:
| nil =>

Goal state after: