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
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)))

Tactic:
rw [← Sheaf.isConstant_iff_isIso_counit_app]

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
⊢ Sheaf.IsConstant (coherentTopology LightProfinite)
    ((sheafCompose (coherentTopology LightProfinite) (CategoryTheory.forget (ModuleCat R))).obj ((functor R).obj M))
Module: Mathlib.Topology.Category.CompHausLike.Cartesian

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
inst✝ : HasProp P (↑X.toTop ⊕ ↑Y.toTop)
⊢ IsColimit (X.coproductCocone Y)

Tactic:
refine BinaryCofan.isColimitMk (fun s ↦ ofHom _ { toFun := Sum.elim s.inl s.inr })
    (by rfl_cat) (by rfl_cat) fun _ _ h₁ h₂ ↦ ?_
  ext ⟨⟩
  exacts [ConcreteCategory.congr_hom h₁ _, ConcreteCategory.congr_hom h₂ _]

Goal state after:
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
hh :
  ∀ (S : LightProfinite) (y : ↑((P ⟹ B).obj.obj (Opposite.op S))),
    ∃ S' φ,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
        ∃ x,
          (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
            (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) y
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e

Tactic:
specialize hh S ((ihomPoints R P B S).symm g)

Goal state after:
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
hh :
  ∃ S' φ,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
      ∃ x,
        (ConcreteCategory.hom (((ihom P).map e).hom.app (Opposite.op S'))) x =
          (ConcreteCategory.hom ((P ⟹ B).obj.map (Opposite.op φ))) ((ihomPoints R P B S).symm g)
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ 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 : (free R).obj S.toCondensed ⊗ P ⟶ B),
    ∃ S' π,
      ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
        ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ P ≫ g = g' ≫ e
A B : LightCondMod R
e : A ⟶ B
he : 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

Tactic:
specialize h e S ((β_ _ _).inv ≫ g)

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
P A B : LightCondMod R
e : A ⟶ B
he : Epi e
S : LightProfinite
g : P ⊗ (free R).obj S.toCondensed ⟶ B
h :
  ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (lightProfiniteToLightCondSet ⋙ free R).map π ▷ P ≫ (β_ P ((free R).obj S.toCondensed)).inv ≫ g = g' ≫ e
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', P ◁ (lightProfiniteToLightCondSet ⋙ free R).map π ≫ g = g' ≫ e
Module: Mathlib.Control.Traversable.Lemmas

Goal state before:
pp: t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
⊢ traverse ((fun {α} ↦ η.app α) ∘ f) = (fun {α} ↦ η.app α) ∘ traverse f

Tactic:
by
  ext
  rw [comp_apply, naturality]

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)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) (n✝ + 1) i✝ ≤ approx (⇑f) (n✝ + 1).succ i✝

Tactic:
apply f.monotone

Goal state after:
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (⇑f) n✝ ≤ approx (⇑f) n✝.succ
i✝ : α
⊢ approx (⇑f) n✝ ≤ approx (⇑f) (n✝ + 1)
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : StateT σ m α) (next : Label ω (StateT σ m) γ → α → StateT σ m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
by
    intros
    simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]; ext; rfl

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

Goal state before:
pp: case refine_1
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
i : X
⊢ IsOpen (Set.range (σ (Option.some i)))ᶜ

pp: case refine_2
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
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
· simpa using IsCompact.isClosed (isCompact_range (hσ i))

Goal state after:
case refine_2
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
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ toSubtype p ⊚ ofSubtype p ⊚ f = f

Tactic:
← comp_assoc,

Goal state after:
n : ℕ
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
p : α ⟹ «repeat» n Prop
f : β ⟹ Subtype_ p
⊢ (toSubtype p ⊚ ofSubtype p) ⊚ f = f
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s

Tactic:
have := @mem_nhds_toTopsp _ _ F.F s a

Goal state after:
α : Type u_1
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
Module: Mathlib.Data.DFinsupp.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : t.support ⊆ s
⊢ f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
by
  refine mem_dfinsupp_iff.trans (forall_and.symm.trans <| forall_congr' fun i =>
      ⟨ fun h => ?_,
        fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)
  · by_cases hi : i ∈ s
    · exact h.2 hi
    · rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 (notMem_mono ht hi)]
      exact zero_mem_zero
  · rwa [H, mem_zero] at h

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (x✝ *> y✝).out = (Function.const α✝ id <$> x✝ <*> y✝).out

Tactic:
simp [Seq.seq, SeqRight.seqRight]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (g : α → β) (x : Erased α), pure g <*> x = g <$> x

Tactic:
by intros; ext; simp [Seq.seq]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : Erased (α → β)) (x : Erased α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      f <*> x

Tactic:
by intros; ext; simp [Seq.seq]

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

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

Tactic:
by
      by_cases hi : i = 0
      · by_cases hj : j = 0
        · simp [hi, hj]
        · simp only [if_pos hi, eq_one_of_ne_zero j hj,
          if_neg (Ne.symm Fin.zero_ne_one)] at hij
          apply (h hij).elim
      · rw [eq_one_of_ne_zero i hi] at hij ⊢
        by_cases hj : j = 0
        · simp [hj] at hij; exact False.elim (h hij.symm)
        · rw [eq_one_of_ne_zero j hj]

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

Goal state before:
pp: n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
⊢ (take (n + m) ⋯ fun i ↦ addCases u v i) = fun i ↦ addCases u (take m h v) i

Tactic:
ext i
  simp only [take, addCases, val_castLE]
  by_cases h' : i < n
  · simp only [h', ↓reduceDIte]
    congr
  · simp only [h', ↓reduceDIte, subNat, castLE, Fin.cast, eqRec_eq_cast]

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

Goal state before:
pp: case cons.none
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match none with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend
      (match none with
      | some b => #[].toListAppend (b :: tl)
      | none => go f tl (#[].push hd))

Tactic:
| none =>

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

Goal state before:
pp: α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : ⟨k, (lookup k s₁).get ⋯⟩ ∈ s₂.entries
⊢ k ∈ s₂.keys

Tactic:
rw [← mem_lookup_iff, Option.mem_def] at this

Goal state after:
α : Type u
β : α → Type v
s₁ s₂ : AList β
h : s₁.entries ⊆ s₂.entries
k : α
hk : k ∈ s₁.keys
this✝ : DecidableEq α := Classical.decEq α
this : lookup k s₂ = some ((lookup k s₁).get ⋯)
⊢ k ∈ s₂.keys
Module: Mathlib.Data.Finmap

Goal state before:
pp: case refine_1
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
l₁ l₂ : List (Sigma β)
p : l₁ ≈ l₂
⊢ ∀ (h₁ : { Dom := l₁.NodupKeys, get := fun nd ↦ f { entries := l₁, nodupKeys := nd } }.Dom)
    (h₂ : { Dom := l₂.NodupKeys, get := fun nd ↦ f { entries := l₂, nodupKeys := nd } }.Dom),
    { Dom := l₁.NodupKeys, get := fun nd ↦ f { entries := l₁, nodupKeys := nd } }.get h₁ =
      { Dom := l₂.NodupKeys, get := fun nd ↦ f { entries := l₂, nodupKeys := nd } }.get h₂

pp: case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
      ⋯).Dom

Tactic:
· exact fun h1 h2 => H _ _ p

Goal state after:
case refine_2
α : Type u
β : α → Type v
γ : Type ?u.32
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ (Quotient.liftOn s.entries (fun l ↦ { Dom := l.NodupKeys, get := fun nd ↦ f { entries := l, nodupKeys := nd } })
      ⋯).Dom
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
a' : α
b' : β a'
h' : ⟨a', b'⟩ ∈ l
h✝¹ : a = a'
h✝ : decide (a = a') = true
⊢ some ⟨a, b⟩ = some ⟨a', b'⟩

Tactic:
subst a'
      simp [nd.eq_of_mk_mem h h']

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x y z : Finmap β
⊢ (x ∪ y).Disjoint z ↔ x.Disjoint z ∧ y.Disjoint z

Tactic:
simp [Disjoint, Finmap.mem_union, or_imp, forall_and]

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

Goal state before:
pp: case intro.a
ι : 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
⊢ p f

Tactic:
rcases eq_empty_or_nonempty (univ.sigma f) with he | hne

Goal state after:
case intro.a.inl
ι : 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
he : univ.sigma f = ∅
⊢ p f

case intro.a.inr
ι : 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
⊢ p f
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a = b

Tactic:
← sq_eq_sq₀ ha hb,

Goal state after:
a b : ℤ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔
    ∃ a_1, ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ { toFun := fun x ↦ x + v, inj' := ⋯ } a_1 = x

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ x ≡ v [ZMOD r] ↔ ∃ a_1, ((a - v ≤ a_1 ∧ a_1 < b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔
    ∃ a_1, ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ { toFun := fun x ↦ x + v, inj' := ⋯ } a_1 = x

Tactic:
Function.Embedding.coeFn_mk,

Goal state after:
a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ x ≡ v [ZMOD r] ↔ ∃ a_1, ((a - v < a_1 ∧ a_1 ≤ b - v) ∧ r ∣ a_1) ∧ a_1 + v = x
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ (dropWhile p l).length ≤ l.length

Tactic:
induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [dropWhile, length_cons]
    split
    · lia
    · simp

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

Goal state before:
pp: case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ ↑(b % r - v % r) ≤ 1 * ↑r

Tactic:
one_mul,

Goal state after:
case pos
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : v % r < b % r
⊢ v % r < b % r ∧ ↑(b % r - v % r) ≤ ↑r
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ Ico n (m + 1) = Ico n m ++ [m]

Tactic:
rwa [← succ_singleton, append_consecutive]
  exact Nat.le_succ _

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 (go f (tl ++ [a]) (#[].push hd))

Tactic:
modifyLast.go_concat _ _ tl (Array.push #[] hd)

Goal state after:
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]) #[]))
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: case nil
α : Type u_1
l : List α
i : ℕ
hi : i < ([].splitLengths l).length
⊢ ([].splitLengths l)[i].length ≤ [][i]

Tactic:
simp at hi

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

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
a : List α
len_a : a.length = n.succ
⊢ Acc (Shortlex r) a

Tactic:
| ind n ih =>

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

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst (diagonal (fun i ↦ (algebraMap R (DualNumber R)) r) i j),
      of fun i j ↦ snd (diagonal (fun i ↦ (algebraMap R (DualNumber R)) r) i j)) =
    inl (diagonal fun i ↦ (algebraMap R R) r)

Tactic:
Algebra.algebraMap_self_apply,

Goal state after:
R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst (diagonal (fun i ↦ (algebraMap R (DualNumber R)) r) i j),
      of fun i j ↦ snd (diagonal (fun i ↦ (algebraMap R (DualNumber R)) r) i j)) =
    inl (diagonal fun i ↦ r)
Module: Mathlib.Data.Nat.Prime.Factorial

Goal state before:
pp: case mp
m n : ℕ
hm : m ≠ 1
⊢ m.minFac ≤ n → ∃ p, Prime p ∧ p ∣ m ∧ p ∣ n !

Tactic:
intro h
    exact ⟨m.minFac, minFac_prime hm, minFac_dvd m, Nat.dvd_factorial (minFac_pos m) h⟩

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: n : ℕ
t : ↑n ≡ ofDigits (-1) (digits 10 n) [ZMOD ↑11]
⊢ ↑n ≡ (List.map (fun n ↦ ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Tactic:
rwa [ofDigits_neg_one] at t

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

Goal state before:
pp: case h₁
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) ≡
    ↑((n / (p ^ a * p)).choose (k / (p ^ a * p))) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]

Tactic:
mul_comm,

Goal state after:
case h₁
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) ≡
    ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ 1 * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
one_mul,

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ multiplicity p n + 1 ≤ multiplicity p n

Tactic:
rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ n

case hf
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ FiniteMultiplicity p n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
x : ℕ
⊢ x ∈ nth p '' Set.Iio #hf.toFinset ↔ x ∈ Set.range ⇑(hf.toFinset.orderEmbOfFin ⋯)

Tactic:
simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf,
        Set.mem_Iio, exists_prop]

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

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : n.choose 1 ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n

Tactic:
choose_one_right,

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : n ≡ 0 [MOD q]
this✝ : Fact (Nat.Prime q)
this : n = q ^ multiplicity q n
⊢ q ∣ n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n

Tactic:
induction n using Nat.strong_induction_on with | _ n ih =>
    rw [nth_eq_sInf]
    refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩
    have : f k < f n := by apply hmono <;> grind
    grind

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

Goal state before:
pp: case bit0
a✝ : PosNum
⊢ ↑2 = if 2 ∣ ↑a✝.bit0 then 2 else (↑a✝.bit0).minFacAux 3

Tactic:
if_pos

Goal state after:
case bit0
a✝ : PosNum
⊢ ↑2 = 2

case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(neg a) = neg a

Tactic:
by
    rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl

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

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
by simpa using! PosNum.cmp_to_nat a b

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

Tactic:
← dual_dual (rotateL _ _ _),

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = (r.dual.rotateL x l.dual).dual.dual
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(d.divMod n.bit1).2 + ↑d * ↑(d.divMod n.bit1).1 = ↑n.bit1 ∧ ↑(d.divMod n.bit1).2 < ↑d

Tactic:
unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
    · lia

Goal state after: