mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.Profinite

Goal state before:
pp: case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C

Tactic:
have U_open : IsOpen U := IsOpen.sdiff (D_clopen none).2
      (isClosed_iUnion_of_finite (fun i ↦ Z_closed (some i)))

Goal state after:
case h_option
X : Type u_4
I✝ : Type u_5
inst✝⁵ : TopologicalSpace X
inst✝⁴ : CompactSpace X
inst✝³ : T2Space X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : Finite I✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
⊢ ∃ C,
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧ (∀ (i : Option I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
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✝
I : Type u_5
inst✝ : Fintype I
IH :
  ∀ {Z D : I → Set X},
    (∀ (i : I), IsClosed[inst✝⁵] (Z i)) →
      (∀ (i : I), IsClopen (D i)) →
        (∀ (i : I), Z i ⊆ D i) →
          univ.PairwiseDisjoint Z →
            ∃ C,
              (∀ (i : I), IsClopen (C i)) ∧
                (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ univ.PairwiseDisjoint C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst✝⁵] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : univ.PairwiseDisjoint Z
Z' : I → Set X := fun i ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst✝⁵] (Z (some i))
Z'_disj : univ.PairwiseDisjoint (Z ∘ some)
U : Set X := D none \ ⋃ i, Z (some i)
U_open : IsOpen[inst✝⁵] U
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
V_subset_D0 : V ⊆ D none
D' : I → Set X := fun i ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : ⋃ i, D' i ⊆ ⋃ i, C' i
C'_disj : univ.PairwiseDisjoint C'
C0 : Set X := D none \ ⋃ i, C' i
this : IsClopen C0
⊢ Disjoint V (⋃ i, C' i)

Tactic:
simp; grind

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

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ Profinite
⊢ TotallyDisconnectedSpace ↑(CompHaus.limitCone (F ⋙ profiniteToCompHaus)).pt.toTop

Tactic:
change TotallyDisconnectedSpace ({ u : ∀ j : J, F.obj j | _ } : Type _)
        exact Subtype.totallyDisconnectedSpace

Goal state after:
Module: Mathlib.Topology.ExtremallyDisconnected

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
⊢ IsTotallySeparated univ

Tactic:
intro x _ y _ hxy

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : ExtremallyDisconnected X
inst✝ : T2Space X
x : X
a✝¹ : x ∈ univ
y : X
a✝ : y ∈ univ
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ l₁' l₂' s',
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step tr)
          { l := some (q₁.pred q₂), var := s, stk := elim (trPosNum m.succ ++ Γ'.cons :: trList v) l₁ c d }
          { l := some (unrev q₂), var := s', stk := elim (l₂' ++ Γ'.cons :: trList v) l₁' c d }
s : Option Γ'
l₁ : List Γ'
⊢ ∃ a l, trPosNum m = a :: l ∧ natEnd a = false

Tactic:
by
      cases m <;> refine ⟨_, _, rfl, rfl⟩

Goal state after:
Module: Mathlib.Topology.Category.LightProfinite.Limits

Goal state before:
pp: X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h : Epi f
⊢ Epi (CompHausLike.pullback.snd f g)

Tactic:
rw [LightProfinite.epi_iff_surjective] at h ⊢
  intro y
  obtain ⟨x, hx⟩ := h (g y)
  exact ⟨⟨⟨x, y⟩, hx⟩, rfl⟩

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

Goal state before:
pp: case case
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Supports (codeSupp' f k) S
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Supports (codeSupp' g k) S
k : Cont'
H : codeSupp (f.case g) k ⊆ S
⊢ Supports (codeSupp' (f.case g) k) S

Tactic:
have H' := H; simp only [codeSupp_case, Finset.union_subset_iff] at H'
    refine trStmts₁_supports' (trNormal_supports H) (Finset.union_subset_left H) fun _ => ?_
    exact supports_union.2 ⟨IHf H'.2.1, IHg H'.2.2⟩

Goal state after:
Module: Mathlib.Condensed.Discrete.Characterization

Goal state before:
pp: X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    functor.essImage X
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE

Tactic:
tfae_have 4 → 6 := fun ⟨Y, ⟨i⟩⟩ S ↦
    ⟨IsColimit.mapCoconeEquiv ((sheafToPresheaf _ _).mapIso i)
      (LightCondensed.isColimitLocallyConstantPresheafDiagram Y S)⟩

Goal state after:
X : LightCondSet
tfae_1_iff_2 : LightCondensed.IsDiscrete X ↔ IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X)
tfae_1_iff_3 : LightCondensed.IsDiscrete X ↔ (LightCondensed.discrete (Type u)).essImage X
tfae_1_iff_4 : LightCondensed.IsDiscrete X ↔ functor.essImage X
tfae_1_iff_5 : LightCondensed.IsDiscrete X ↔ IsIso (LocallyConstant.adjunction.counit.app X)
tfae_6_to_4 :
  (∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))) →
    functor.essImage X
tfae_4_to_6 :
  functor.essImage X →
    ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))
⊢ [LightCondensed.IsDiscrete X, IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, functor.essImage X,
      IsIso (LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite), Nonempty (IsColimit (X.obj.mapCocone (coconeRightOpOfCone S.asLimitCone)))].TFAE
Module: Mathlib.Condensed.Light.InternallyProjective

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

pp: case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
⊢ Epi ((ihom P).map e)

Tactic:
· have hh := h.1 e
    rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite] at hh
    specialize hh S ((ihomPoints R P B S).symm g)
    obtain ⟨S', π, hπ, g', hh⟩ := hh
    refine ⟨S', π, hπ, (ihomPoints _ _ _ _) g', ?_⟩
    rw [ihom_map_val_app] at hh
    apply (ihomPoints R P B S').symm.injective
    rw [hh]
    exact ihomPoints_symm_comp R B P S' S π g

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P : LightCondMod R
h :
  ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : P ⊗ (free R).obj S.toCondensed ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : Epi e
⊢ Epi ((ihom P).map e)
Module: Mathlib.Condensed.Light.InternallyProjective

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

Tactic:
· rw [LightCondMod.epi_iff_locallySurjective_on_lightProfinite]
    intro S g
    specialize h e S ((ihomPoints _ _ _ _) g)
    obtain ⟨S', π, hπ, g', hh⟩ := h
    refine ⟨S', π, hπ, (ihomPoints _ _ _ _).symm g', ?_⟩
    rw [ihom_map_val_app]
    have := ihomPoints_symm_comp R B P S' S π ((ihomPoints R P B S) g)
    dsimp at hh
    rw [hh] at this
    simp [this, Quiver.Hom.op]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ InternallyProjective ((free R).obj P.toCondensed) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e

Tactic:
rw [free_internallyProjective_iff_tensor_condition']

Goal state after:
R : Type u
inst✝ : CommRing R
P : LightProfinite
⊢ (∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite)
      (g : (free R).obj (S.toCondensed ⊗ P.toCondensed) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map π ▷ P.toCondensed) ≫ g = g' ≫ e) ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [Epi e] (S : LightProfinite) (g : (free R).obj (S ⊗ P).toCondensed ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
          ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ P)) ≫ g = g' ≫ e
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case id_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ β✝ : Type u
x✝ : bicompl t F G α✝ β✝
⊢ bitraverse pure pure x✝ = pure x✝

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

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

Goal state before:
pp: case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
g✝ : α✝ → G✝ β✝
g'✝ : α'✝ → G✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (Functor.Comp.mk ∘ Functor.map f✝ ∘ g✝) (Functor.Comp.mk ∘ Functor.map f'✝ ∘ g'✝) x✝ =
    Functor.Comp.mk (bitraverse f✝ f'✝ <$> bitraverse g✝ g'✝ x✝)

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

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

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (pure ∘ f✝) (pure ∘ f'✝) x✝ = pure (bimap f✝ f'✝ x✝)

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ bitraverse (traverse (pure ∘ f✝)) (traverse (pure ∘ f'✝)) x✝ = pure (bimap (Functor.map f✝) (Functor.map f'✝) x✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
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✝ : bicompl t F G α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝

Tactic:
simp [bitraverse, Bicompl.bitraverse, bimap, traverse_id, bitraverse_id_id, comp_bitraverse,
      functor_norm]

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
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✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.Fold

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

Tactic:
induction xs with

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ X

Tactic:
trans f X

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ { toFun := approx ⇑f, monotone' := ⋯ } (n✝ + 1) ≤ f X

α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
X : (a : α) → Part (β a)
hX : f X ≤ X
n✝ : ℕ
i_ih : { toFun := approx ⇑f, monotone' := ⋯ } n✝ ≤ X
⊢ f X ≤ X
Module: Mathlib.Data.BitVec

Goal state before:
pp: w n : ℕ
x : BitVec w
⊢ (↑n).toFin * x.toFin = n • x.toFin

Tactic:
by
    open scoped Fin.CommRing in
    simp only [natCast_eq_ofNat, toFin_ofNat, Fin.ofNat_eq_cast, nsmul_eq_mul]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Type u_2
n' m : ℕ
h : m ≤ n
a : Fin n' → α
⊢ take (m * n') ⋯ («repeat» n a) = «repeat» m a

Tactic:
by
  ext i
  simp only [take, repeat_apply, modNat, val_castLE]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: n : ℕ
α : Fin n → Sort u_1
m : ℕ
h : m ≤ n
v : (i : Fin n) → α i
i : Fin n
hi : ↑i ≥ m
x : α i
⊢ take m h (update v i x) = take m h v

Tactic:
by
  ext j
  have : castLE h j ≠ i := by
    refine ne_of_val_ne ?_
    simp only [val_castLE]
    exact Nat.ne_of_lt (lt_of_lt_of_le j.isLt hi)
  simp only [take, update_of_ne this]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s : AList β
⊢ a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s

Tactic:
rw [mem_keys, keys_erase, s.keys_nodup.mem_erase_iff, ← mem_keys]

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

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

Tactic:
by
  induction l with
  | nil => grind
  | cons s _ _ =>
    have (h : a ≠ s.fst) : ¬ f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
    by_cases a = s.fst <;> grind [Sigma.map]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
⊢ a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs

Tactic:
induction xs with

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a (s₁ ∪ s₂) = lookup a s₁

Tactic:
lookup_union_right h',

Goal state after:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
h' : a ∉ s₁
⊢ lookup a s₂ = lookup a s₁
Module: Mathlib.Data.List.Sigma

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

Tactic:
simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]

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

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

Tactic:
induction xs with

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

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

Tactic:
induction xs with

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

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

Tactic:
induction p generalizing l with
  | nil => rfl
  | cons hd _ ih =>
    simp [ih (List.kerase _ _)]
  | swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
  | trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
⊢ x ∉ g i

Tactic:
hg,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
⊢ x ∉ update f i ((f i).erase x) i
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update g i (insert x (g i))

Tactic:
hg,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
i : ι
hi : (f i).Nonempty
x : α i
x_mem : x ∈ f i
hr : r i x ((f i).erase x)
g : (a : ι) → Finset (α a)
hg : g = update f i ((f i).erase x)
hx' : x ∉ g i
⊢ f = update (update f i ((f i).erase x)) i (insert x (update f i ((f i).erase x) i))