mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f₁ f₂ : X ⟶ Y
h : G.map f₁ = G.map f₂
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨Sieve.equalizer f₁ f₂, ⋯⟩).arrows a
⊢ F.obj.map f₁.op ≫ F.obj.map { Y := W₀, f := a, hf := ha }.f.op =
    F.obj.map f₂.op ≫ F.obj.map { Y := W₀, f := a, hf := ha }.f.op

Tactic:
dsimp at ha ⊢

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f₁ f₂ : X ⟶ Y
h : G.map f₁ = G.map f₂
W₀ : C
a : W₀ ⟶ X
ha : a ≫ f₁ = a ≫ f₂
⊢ F.obj.map f₁.op ≫ F.obj.map a.op = F.obj.map f₂.op ≫ F.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (↑⟨Sieve.pullback p (G.imageSieve f), ⋯⟩).arrows a
⊢ (mapPreimage K G F f ≫ F.obj.map p.op) ≫ F.obj.map { Y := W₀, f := a, hf := ha }.f.op =
    F.obj.map g.op ≫ F.obj.map { Y := W₀, f := a, hf := ha }.f.op

Tactic:
dsimp at ha ⊢

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ (mapPreimage K G F f ≫ F.obj.map p.op) ≫ F.obj.map a.op = F.obj.map g.op ≫ F.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ Z_1 g_1 h, S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1) →
    ∃ Z_1 g_1 h, S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1

Tactic:
rintro ⟨W, a, b, h, rfl⟩
    exact ⟨W, a ≫ f, b, h, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.obj.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
⊢ x = y

Tactic:
ext W
  apply (((isSheaf_iff_isSheaf_of_type _ _).1 F.2).isSeparated _ (hY W.unop)).ext
  rintro T a ⟨i, ⟨b⟩⟩
  simpa using congr_arg (F.1.map b.op) (h i)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPushforward (Over.forget X) (functorPullback (Over.post F) S) ≤
    functorPullback F (functorPushforward (Over.forget (F.obj X)) S)

Tactic:
Sieve.functorPushforward_le_iff_le_functorPullback,

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback (Over.post F) S ≤
    functorPullback (Over.forget X) (functorPullback F (functorPushforward (Over.forget (F.obj X)) S))
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso f

Tactic:
rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology ≤ pretopology T

pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology

Tactic:
· intro X R hR x hx
    rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
    exact ⟨V, g₂, hg₂, g₁.le hU⟩

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
⊢ ∃ U, ∃ (m : x ∈ U), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
by
  obtain ⟨U, s, e⟩ :=
    Types.jointly_surjective.{v, v} _ (isColimitOfPreserves (forget C) (colimit.isColimit _)) t
  revert s e
  induction U with | op U => ?_
  obtain ⟨V, m⟩ := U
  intro s e
  exact ⟨V, m, s, e⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom (F ≫ D₂.ι)) ∘ ⇑(ConcreteCategory.hom D₁.π) =
    ⇑(ConcreteCategory.hom D₂.p) ∘ ⇑(ConcreteCategory.hom D₁.i)

Tactic:
rw [← ContinuousLinearMap.coe_comp, ← ContinuousLinearMap.coe_comp,
        ← hom_comp, ← hom_comp, ShortComplex.π_leftRightHomologyComparison'_ι]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
rw [← cocone_naturality F f]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.mul
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝ y✝ : Prequotient F
j : J
x y : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j (x * y)) = descFunLift F s ((Prequotient.of j x).mul (Prequotient.of j y))

Tactic:
exact map_mul (s.ι.app j).hom x y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
⊢ 𝟙 (F.obj i₀) ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
rw [id_comp]

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: case neg
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : IsEmpty ι
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b

Tactic:
obtain ⟨j', ⟨a⟩⟩ := h₁ j

Goal state after:
case neg
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : IsEmpty ι
j' : J₁
a : j ⟶ F.obj j'
⊢ ∃ l a b, ∀ (i : ι), f i ≫ a = b
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
d : N₁
hd : g₁ d = i₂ (σ (ι₃ x))
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))

Tactic:
rw [← hd, ← ρ.comp_apply, hρ, id_eq]

Goal state after:
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_pos : n ≠ 0
⊢ IsPrimePow q

Tactic:
exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case h.right.intro
R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ CharP (R ⧸ M) p

Tactic:
convert! hr
        have r_dvd_p : r ∣ p := by
          rw [← CharP.cast_eq_zero_iff (R ⧸ M) r p]
          convert! congr_arg (Ideal.Quotient.factor hM_ge) (CharP.cast_eq_zero (R ⧸ I) p)
        symm
        apply (Nat.Prime.eq_one_or_self_of_dvd hp r r_dvd_p).resolve_left
        exact CharP.char_ne_one (R ⧸ M) r

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
h : ¬∃ p > 0, MixedCharZero R p
⊢ P

Tactic:
apply h_equal
    rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h
    exact h.some

Goal state after:
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : (fun x ↦ l[x]?) n = none
⊢ (fun x ↦ l[x]?) (n + 1) = none

Tactic:
rw [List.getElem?_eq_none_iff] at h ⊢

Goal state after:
α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : l.length ≤ n
⊢ l.length ≤ n + 1
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ s.odd.get n = s.get (2 * n + 1)

Tactic:
by
  rw [odd_eq, get_even]; rfl

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.length' = 0 ↔ s = nil

Tactic:
by
  cases s <;> simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.length' ≠ 0 ↔ ∃ x s', s = cons x s'

Tactic:
by
  cases s <;> simp

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ s.tails = s.tail :: s.tail.tails

Tactic:
unfold tails; rw [corec_eq]; rfl

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ Stream'.map (fun o ↦ Option.rec none (fun val ↦ some (g (f val))) o) s =
    Stream'.map
      ((fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o) s

Tactic:
apply congr_arg fun f : _ → Option γ => Stream'.map f s

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
⊢ (fun o ↦ Option.rec none (fun val ↦ some (g (f val))) o) =
    (fun o ↦ Option.rec none (fun val ↦ some (g val)) o) ∘ fun o ↦ Option.rec none (fun val ↦ some (f val)) o
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
⊢ (g.conts (n + 2)).a = gp.b * predConts.a + gp.a * ppredConts.a

Tactic:
conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
⊢ { a := gp.b * predConts.a + gp.a * ppredConts.a, b := gp.b * predConts.b + gp.a * ppredConts.b }.a =
    gp.b * predConts.a + gp.a * ppredConts.a
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
⊢ (g.conts (n + 2)).b = gp.b * predConts.b + gp.a * ppredConts.b

Tactic:
conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
⊢ { a := gp.b * predConts.a + gp.a * ppredConts.a, b := gp.b * predConts.b + gp.a * ppredConts.b }.b =
    gp.b * predConts.b + gp.a * ppredConts.b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons.inr.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

pp: case cons.inr.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
· simp [i1, e']

Goal state after:
case cons.inr.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s

Tactic:
apply congr_arg fun f : _ → Option γ => Stream'.map f s

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
⊢ (map f s).length' = s.length'

Tactic:
by_cases h : (s.map f).Terminates <;> have h' := h <;> rw [terminates_map_iff] at h'

Goal state after:
case pos
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
h' : s.Terminates
⊢ (map f s).length' = s.length'

case neg
α : Type u
β : Type v
s : Seq α
f : α → β
h : ¬(map f s).Terminates
h' : ¬s.Terminates
⊢ (map f s).length' = s.length'
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
cb : Computation β
⊢ LiftRelAux R C (Sum.inl a) cb.destruct ↔ ∃ b, b ∈ cb ∧ R a b

Tactic:
induction cb using recOn with
  | pure b =>
    exact
      ⟨fun h => ⟨_, ret_mem _, h⟩, fun ⟨b', mb, h⟩ => by rw [mem_unique (ret_mem _) mb]; exact h⟩
  | think cb =>
    rw [destruct_think]
    exact ⟨fun ⟨b, h, r⟩ => ⟨b, think_mem h, r⟩, fun ⟨b, h, r⟩ => ⟨b, of_think_mem h, r⟩⟩

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) b a = LiftRelAux R C a b

Tactic:
by
  rcases a with a | ca <;> rcases b with b | cb <;> simp only [LiftRelAux]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
by
  rcases eq_or_ne (fract v) 0 with h | h
  · obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
    rw [fract_intCast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int,
      Stream'.Seq.get?_nil, Stream'.Seq.get?_nil]
  rcases eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ | h₁
  · rwa [h₁, ← terminatedAt_iff_s_none,
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, stream_succ h, ←
      of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none, terminatedAt_iff_s_none]
  · obtain ⟨p, hp⟩ := Option.ne_none_iff_exists'.mp h₁
    obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp
    have Hp := get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁
    rw [← stream_succ h] at hp'₁
    rw [Hp, get?_of_eq_some_of_succ_get?_intFractPair_stream hp'₁]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n.succ ≤ fib n.succ

Tactic:
rw [succ_le_iff]

Goal state after:
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib n.succ
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : n ≤ m
⊢ v = (of v).convs m

Tactic:
rw [convs_stable_of_terminated m_geq_n terminatedAt_n]

Goal state after:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : n ≤ m
⊢ v = (of v).convs n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
β : Type v
f : α → β
S✝ S : Seq (Seq1 α)
a : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    (nil.append (Seq.map f (Seq.cons (a, s) S).join)).destruct
    (nil.append (Seq.map (map f) (Seq.cons (a, s) S)).join).destruct

Tactic:
simpa [map] using ⟨_, _, rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
cases s_succ_nth_eq : s.get? (n + 1) with
  | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
  | some =>
    obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
      s.ge_stable n.le_succ s_succ_nth_eq
    simp [*, squashSeq, m_lt_n.ne]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.some.inl
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_zero : fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

pp: case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
· simp [IntFractPair.stream, IH.symm, v_eq_q, stream_q_nth_eq, fr_zero]

Goal state after:
case succ.some.inr
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream (↑q) n
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
fr_ne_zero : ¬fr = 0
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
⊢ a = 1

Tactic:
by
  obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a :=
    exists_s_a_of_partNum nth_partNum_eq
  have : gp.a = 1 := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).left
  rwa [gp_a_eq_a_n] at this

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq I
V : I → Ideal R
inst✝ : Decomposition V
x : R
i : I
⊢ ↑(((decompose V) x) i) = x * idempotent V i

Tactic:
rw [← smul_eq_mul (a := x), idempotent, ← Submodule.coe_smul, ← smul_apply, ← decompose_smul,
    smul_eq_mul, mul_one]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ (fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) ((fun P ↦ ⟨P.toPoly, ⋯⟩) P) =
    P

Tactic:
ext <;> simp only [coeffs]

Goal state after: