mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
a : ↑((forget₂ (TopModuleCat R) TopCat).obj X)
⊢ (↑(hom
            ((forget₂ (TopModuleCat R) TopCat ⋙ free R).map f ≫
              ConcreteCategory.ofHom
                { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj Y).toModuleCat) R ↑Y.toModuleCat) id,
                  cont := ⋯ })) ∘ₗ
        Finsupp.lsingle a)
      1 =
    (↑(hom
            (ConcreteCategory.ofHom
                { toLinearMap := (Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id,
                  cont := ⋯ } ≫
              (𝟭 (TopModuleCat R)).map f)) ∘ₗ
        Finsupp.lsingle a)
      1

Tactic:
dsimp [freeObj, freeMap]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
f : X ⟶ Y
a : ↑((forget₂ (TopModuleCat R) TopCat).obj X)
⊢ ((Finsupp.mapDomain (⇑(Hom.hom f)) (Finsupp.single a 1)).sum fun x r ↦ r • x) =
    (Hom.hom f) ((Finsupp.single a 1).sum fun x r ↦ r • x)
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)))

Tactic:
suffices PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) from
    ⟨fun {c} hc ↦ ⟨isColimitOfReflects uliftFunctor.{v₁}
        (isColimitOfPreserves (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) hc)⟩⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
inst✝ : IsCardinalPresentable X κ
e : C ≌ C'
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
Y : J ⥤ C'
this : PreservesColimitsOfShape J (coyoneda.obj (op X))
⊢ PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
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 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₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ π₂ (i₂ (σ (ι₃ x))) = 0

Tactic:
hπ₂.apply_apply_eq_zero

Goal state after:
case mpr
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
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 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₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePushouts C
⊢ HasColimitsOfSize.{w, w, v, max u v} (Under B)

Tactic:
rw [← hasLimitsOfSize_opposite_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasWidePushouts C
⊢ HasLimitsOfSize.{w, w, v, max u v} (Under B)ᵒᵖ
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: K : Type u_3
L : Type u_4
inst✝² : DivisionRing K
inst✝¹ : NonAssocSemiring L
inst✝ : Nontrivial L
f : K →+* L
p : ℕ
⊢ CharP K p ↔ CharP L p

Tactic:
by
  simp only [charP_iff, ← f.injective.eq_iff, map_natCast f, map_zero f]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ¬↑t = 0

Tactic:
← Ne

Goal state after:
R : Type u_1
inst✝² : Ring R
t : ℕ
inst✝¹ : Invertible ↑t
inst✝ : Nontrivial R
⊢ ↑t ≠ 0
Module: Mathlib.Algebra.CharP.Pi

Goal state before:
pp: ι : Type u
hi : Nonempty ι
R : Type v
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
x : ℕ
i : ι
h : ↑x = 0
⊢ ↑x = 0

Tactic:
by rw [← map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x, h, map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
by
  constructor
  · intro g
    rcases g with ⟨I, ⟨hI_not_top, _⟩⟩
    -- Krull's Thm: There exists a prime ideal `M` such that `I ≤ M`.
    rcases Ideal.exists_le_maximal I hI_not_top with ⟨M, ⟨hM_max, hM_ge⟩⟩
    use M
    constructor
    · exact hM_max
    · cases CharP.exists (R ⧸ M) with
      | intro r hr =>
        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
  · intro ⟨I, hI_max, h_charP⟩
    use I
    exact ⟨Ideal.IsMaximal.ne_top hI_max, h_charP⟩

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ corec' (Corec.f f) o (n + 1) = none → corec' (Corec.f f) (Corec.f f o).snd (n + 1) = none

Tactic:
| succ n IH =>

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

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

Tactic:
tail_map,

Goal state after:
α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ (map f s).head :: map f s.tail = f s.head :: map f s.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ (iterate f a).tail = iterate f (f a)

Tactic:
ext n
  rw [get_tail]
  induction n with
  | zero => rfl
  | succ n ih => rw [get_succ_iterate', ih, get_succ_iterate']

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

Goal state before:
pp: case some.succ
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
IH : s.val n = (pure a).val n
⊢ s.val (n + 1) = (pure a).val (n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ iterate f (f a) (n + 1) = map f (iterate f a) (n + 1)

Tactic:
unfold map iterate get

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : iterate f (f a) n = map f (iterate f a) n
⊢ f (iterate f (f a) n) = f (iterate f a (n + 1))
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → α ⊕ β
b : β
a' : α
n : ℕ
IH : ∀ (o : α ⊕ β), Stream'.corec' (Corec.f f) o n = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd n = some a'
o : α ⊕ β
⊢ Stream'.corec' (Corec.f f) o (n + 1) = some a' → Stream'.corec' (Corec.f f) (Corec.f f o).snd (n + 1) = some a'

Tactic:
| succ n IH =>

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

Goal state before:
pp: α : Type u
s : Computation α
x✝ : s.Terminates
a : α
n : ℕ
h : (fun b ↦ some a = b) (s.val.get n)
⊢ (s.val n).isSome = true

Tactic:
by
      dsimp [Stream'.get] at h
      rw [← h]
      exact rfl

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
n : ℕ
IH : C ((pure a).thinkN n)
⊢ C ((pure a).thinkN (n + 1))

Tactic:
| succ n IH =>

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

Goal state before:
pp: case neg
α : Type u
x : α
s : Seq α
h : ¬(cons x s).Terminates
h' : ¬s.Terminates
⊢ (cons x s).length' = s.length' + 1

Tactic:
simp [length'_of_not_terminates h, length'_of_not_terminates h']

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ (∀ (h : s.Terminates), n < s.length h) ↔ ∃ a, a ∈ s.get? n

Tactic:
simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
    ← Option.ne_none_iff_exists', ne_eq]
  refine ⟨?_, ?_⟩
  · intro h hn
    exact h n hn n le_rfl hn
  · intro hn _ _ k hkn hk
    exact hn <| le_stable s hkn hk

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

Goal state before:
pp: case succ
K : Type u_1
n✝ : ℕ
inst✝ : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)}, s.get? n = none → convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
      ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
⊢ (g.contsAux (n + 1)).a * (g.contsAux (n + 1 + 1)).b - (g.contsAux (n + 1)).b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.drop (n + 1)).head = s.get? (n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
⊢ IntFractPair.of v = ifp_zero

Tactic:
simpa only [IntFractPair.stream, Option.some.injEq] using stream_zero_eq

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ 0 ≠ 1

Tactic:
change (0 : Ring.DirectLimit G (f' · · ·)) ≠ 1

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : Nonempty ι
inst✝² : IsDirectedOrder ι
inst✝¹ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
f' : (i j : ι) → i ≤ j → G i →+* G j
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)
i : ι
⊢ 0 ≠ 1
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) ((of v).contsAux (n + 1)) ifp_n.fr
⊢ ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v (n + 1) = some ifp_n →
      v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_n.fr

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
n : ℕ
IH : IntFractPair.stream v n = none → v = (of v).convs (n - 1)
nth_stream_eq_none : IntFractPair.stream v (n + 1) = none
⊢ v = (of v).convs (n + 1 - 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ SS.join.join = (Seq.map join SS).join

Tactic:
apply
    Seq.eq_of_bisim fun s1 s2 =>
      ∃ s SS,
        s1 = Seq.append s (Seq.join (Seq.join SS)) ∧ s2 = Seq.append s (Seq.join (Seq.map join SS))

Goal state after:
case bisim
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join

case r
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ ∃ s SS_1, SS.join.join = s.append SS_1.join.join ∧ (Seq.map join SS).join = s.append (Seq.map join SS_1).join
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ
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 v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
q : ℚ
n✝ n : ℕ
IH : ∀ {ifp_n : IntFractPair ℚ}, IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑n
⊢ ∀ {ifp_n : IntFractPair ℚ},
    IntFractPair.stream q (n + 1) = some ifp_n → ifp_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(n + 1)

Tactic:
| succ n IH =>

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

Goal state before:

Tactic:
1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'
      _ ≤ ε * (B * nB) := ?_

Goal state after:
case inr
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ ε * ↑N' ≤ ε * (B * nB)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ g.convs (n + 1) = g.convs' (n + 1)

Tactic:
| succ n IH =>

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

Goal state before:
pp: case succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
| succ n IH =>

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ gp_n.b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
n : ℕ
IH :
  ∀ {e : Fin n → S},
    OrthogonalIdempotents e → (∀ (i : Fin n), e i ∈ f.range) → ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
e : Fin (n + 1) → S
he : OrthogonalIdempotents e
he' : ∀ (i : Fin (n + 1)), e i ∈ f.range
⊢ ∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e

Tactic:
| succ n IH =>

Goal state after:
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod

Tactic:
| cons x xs ih =>

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
simp_rw [genEigenspace, OrderHom.coe_mk, LinearMap.mem_ker, iSup_subtype',
    Submodule.mem_iSup_of_directed _ this, LinearMap.mem_ker, Subtype.exists, exists_prop]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
by
  calc f.genEigenspace μ k
      ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
    _ ≤ f.genEigenspace μ (finrank K V) := by
      rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
      exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ 1 ≤ ↑k

Tactic:
simpa using Nat.succ_le_of_lt hk

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.fst + inr x.snd ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
inr_eq_smul_eps,

Goal state after:
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.fst + x.snd • ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case insert
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ μ₁ ∉ insert μ₂ s → Disjoint ((f.genEigenspace μ₁) k) ((insert μ₂ s).sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
intro hμ₁₂
  obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
  specialize ih hμ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  let g := f - μ₂ • 1
  simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
  peel hy with l hlk hl
  simp only [LinearMap.mem_ker] at hl
  have hyz : (g ^ l) (y + z) ∈
      (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k := by
    refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
    · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
    · rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
  rwa [ih.eq_bot, Submodule.mem_bot] at hyz

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
have := Module.Finite.of_basis b

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this : Module.Finite R M
⊢ (trace R N) (e.conj f) = (trace R M) f
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ ((f - μ • 1) ^ finrank K V).range ⊓ (f.genEigenspace μ) ↑(finrank K V) ≤ ⊥

Tactic:
LinearMap.range_eq_map,

Goal state after:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h :
  Submodule.comap ((f - μ • 1) ^ finrank K V) ((f.genEigenspace μ) ↑(finrank K V)) = (f.genEigenspace μ) ↑(finrank K V)
⊢ Submodule.map ((f - μ • 1) ^ finrank K V) ⊤ ⊓ (f.genEigenspace μ) ↑(finrank K V) ≤ ⊥
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
k : ℕ
μ : K
hx : f.HasEigenvalue μ
hk : 0 < k
⊢ 1 ≤ ↑k

Tactic:
simpa using Nat.succ_le_of_lt hk

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (-f - μ • 1).ker ≠ ⊥ ↔ (f - -μ • 1).ker ≠ ⊥

Tactic:
rw [← LinearMap.ker_neg]

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (-(-f - μ • 1)).ker ≠ ⊥ ↔ (f - -μ • 1).ker ≠ ⊥