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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Ring R
R₂ : Type u_2
inst✝⁶ : Ring R₂
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x y : M
⊢ f (x - y) = f x - f y

Tactic:
exact map_sub f x y

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
f : X ⟶ Y
x✝ : IsIso ((forget Semigrp).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget Semigrp).map f)

Goal state after:
X✝ Y✝ : Type u
X Y : Semigrp
f : X ⟶ Y
x✝ : IsIso ((forget Semigrp).map f)
i : (forget Semigrp).obj X ≅ (forget Semigrp).obj Y := asIso ((forget Semigrp).map f)
⊢ IsIso f
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ e 1 * e.symm 1 = 1

Tactic:
rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ (TensorProduct.lid R S).symm ((Algebra.linearMap R S) (g s)) = (TensorProduct.lid R S).symm s

Tactic:
TensorProduct.lid_symm_apply,

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] (Algebra.linearMap R S) (g s) = (TensorProduct.lid R S).symm s
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] (Algebra.linearMap R S) (g s) = (TensorProduct.lid R S).symm s

Tactic:
TensorProduct.lid_symm_apply,

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] (Algebra.linearMap R S) (g s) = 1 ⊗ₜ[R] s
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : IsEffective R S
⊢ Function.Surjective ⇑(codRestrictEqLocusPushoutCocone R S)

Tactic:
intro ⟨s, hs⟩

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : IsEffective R S
s : ↑(CommRingCat.of S)
hs :
  s ∈
    (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inl).eqLocus
      (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inr)
⊢ ∃ a, (codRestrictEqLocusPushoutCocone R S) a = ⟨s, hs⟩
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid M₂
inst✝ : TopologicalSpace M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
p q : Submodule R M
h : p = q
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (LinearEquiv.ofEq p q h).invFun

Tactic:
by
    have h' : (fun x ↦ x ∈ p) = (fun x ↦ x ∈ q) := by simp [h]
    exact (Homeomorph.ofEqSubtypes h').symm.continuous

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.IsEventuallyConstantFrom i₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map φ)

Tactic:
by
  have := h ι
  have := h (ι ≫ φ)
  exact IsIso.of_isIso_fac_left (F.map_comp ι φ).symm

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsColimit (((const C).obj A).mapCocone c)

Tactic:
have h := isFiltered_of_isCardinalFiltered J κ

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
⊢ IsColimit (((const C).obj A).mapCocone c)
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
by
  obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q
  let f (S : Σ R : Subtype Q', FGAlgCatSkeleton R) : CommRingCat := .of S.2.eval.obj
  refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
  obtain ⟨R, hR, φ, hφ⟩ := hPQ S hS
  wlog hR' : Q' R generalizing R
  · obtain ⟨R', hR', ⟨e⟩⟩ := hQQ' _ hR
    exact this R' (hQ'Q _ hR') (e.inv ≫ φ)
      (hφ.comp e.symm.commRingCatIsoToRingEquiv.finite.finiteType) hR'
  obtain ⟨T, e, he⟩ := hφ.exists_smallRepr
  exact ⟨_, ⟨⟨_, hR'⟩, T⟩, ⟨RingEquiv.toCommRingCatIso e.symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
x✝¹ :
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
h₁ : ∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)
h₂ : ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (i : A), Nonempty (F.obj i ⟶ j)
a : (i : A) → F.obj i ⟶ j := fun i ↦ ⋯.some
l : J
b : j ⟶ l
hb : ∀ (i : Arrow A), (F.map i.hom ≫ a i.right) ≫ b = a i.left ≫ b
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨{
    pt := l
    ι.app i := a i ≫ b
    ι.naturality _ _ f := by simpa using hb (Arrow.mk f) }⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ IsEmbedding fun x ↦ f ≫ x

Tactic:
refine IsEmbedding.of_comp (continuous_precomp _) (IsInducing.induced _).continuous ?_
  suffices IsEmbedding ((· ∘ f.hom) : (B → R) → (A → R)) from
    this.comp (.induced (fun f g e ↦ by ext a; exact congr($e a)))
  exact Function.Surjective.isEmbedding_comp _ hf

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : Algebra R S
inst✝⁶ : Module R M₁
inst✝⁵ : Module S M₁
inst✝⁴ : IsScalarTower R S M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module S M₂
inst✝ : IsScalarTower R S M₂
c : S
x : (M₁ × M₂) ⊗[R] M₃
⊢ ∀ (x : M₁ × M₂) (y : M₃),
    (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
            (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
        (c • x ⊗ₜ[R] y) =
      c •
        (TensorProduct.comm R (M₁ × M₂) M₃ ≪≫ₗ prodRight R R M₃ M₁ M₂ ≪≫ₗ
              (TensorProduct.comm R M₃ M₁).prodCongr (TensorProduct.comm R M₃ M₂)).toAddEquiv
          (x ⊗ₜ[R] y)

Tactic:
simp [TensorProduct.smul_tmul']

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : u * (↑p * r) = u * 0
⊢ False

Tactic:
rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
u : R
hu : u * ↑p = 1
hr₁ : r = 0
⊢ False
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
A : P.Under Q X
⊢ pushout.inl A.hom f ≫ ((pushoutCongr ⋯).hom.app A).right = pushout.inl A.hom f

Tactic:
simp [pushoutCongr]

Goal state after:
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
T : Type u_3
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S T
inst✝⁵ : IsScalarTower R S T
A : Type u_4
B : Type u_5
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
f g : A →ₐ[R] B
inst✝ : Module.Flat R T
h₁ : Function.Surjective ⇑(algebraMap S T)
⊢ ↥(RingHom.ker (TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T))) ≃ₗ[A ⊗[R] S]
    A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T))

Tactic:
let φ : A ⊗[R] S →ₐ[A] A ⊗[R] T :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)
  let ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
    { __ := Algebra.TensorProduct.comm _ _ _, commutes' _ := rfl }
  let e₃ : (RingHom.ker φ) ≃ₗ[R] A ⊗[R] (RingHom.ker (algebraMap S T)) :=
    (LinearMap.kerLTensorEquivOfSurjective (IsScalarTower.toAlgHom R S T).toLinearMap
      h₁ A).restrictScalars R
  let e₄' : (RingHom.ker φ) ≃ₗ[R] (A ⊗[R] S) ⊗[S] (RingHom.ker (algebraMap S T)) :=
    e₃ ≪≫ₗ _root_.TensorProduct.comm _ _ _ ≪≫ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ S _ _).symm.restrictScalars R ≪≫ₗ
      (AlgebraTensorModule.congr (.refl S _) ePp.symm.toLinearEquiv).restrictScalars R ≪≫ₗ
      (_root_.TensorProduct.comm _ _ _).restrictScalars R
  let e₄ : (A ⊗[R] S) ⊗[S] (RingHom.ker (algebraMap S T)) ≃ₗ[A ⊗[R] S] (RingHom.ker φ) :=
    { __ := e₄'.symm, map_smul' r' x := by
        dsimp
        induction x with
        | zero => simp only [smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, LinearEquiv.map_add, *]
        | tmul x y =>
        induction x with
        | zero => simp only [zero_tmul, smul_zero, LinearEquiv.map_zero]
        | add x y _ _ => simp only [smul_add, add_tmul, LinearEquiv.map_add, *]
        | tmul x z =>
        induction r' with
        | zero => simp only [zero_smul, LinearEquiv.map_zero]
        | add x y _ _ => simp only [add_smul, LinearEquiv.map_add, *]
        | tmul r s =>
        rw [smul_tmul']
        ext1
        dsimp [e₄', ePp, φ]
        change ((r * x) ⊗ₜ[R] ((s * z) * y.1)) = (r ⊗ₜ[R] s) * (x ⊗ₜ[R] (z * y.1))
        rw [Algebra.TensorProduct.tmul_mul_tmul, mul_assoc] }
  exact e₄.symm

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

Goal state before:
pp: α : Type u
a : α
l₁ l₂ : List α
s : Stream' α
⊢ a :: l₁ ++ l₂ ++ₛ s = a :: l₁ ++ₛ (l₂ ++ₛ s)

Tactic:
by
    rw [List.cons_append, cons_append_stream, cons_append_stream, append_append_stream l₁]

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

Goal state before:
pp: case cons.succ
α : Type u
a : Stream' α
b : α
x : List α
ih : ∀ (n : ℕ) (h : n < x.length), (x ++ₛ a).get n = x[n]
n : ℕ
h : n + 1 < (b :: x).length
⊢ (b :: x ++ₛ a).get (n + 1) = (b :: x)[n + 1]

Tactic:
simp [ih n (by simpa using h), cons_append_stream]

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ take n nil = []

Tactic:
by
  cases n <;> rfl

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

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match s.destruct with
    | none => []
    | some (x, r) => x :: take l r

Tactic:
head_eq_some h_get

Goal state after:
case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match (cons x s.tail).destruct with
    | none => []
    | some (x, r) => x :: take l r
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
a : ℤ
n : ℕ
⊢ IntFractPair.stream (↑a) (n + 1) = none

Tactic:
induction n with
  | zero =>
    refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_
    simp only [IntFractPair.of, Int.fract_intCast]
  | succ n ih => exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

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

Goal state before:
pp: n : ℕ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))

Tactic:
by
  rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
  have : fib n ≤ 2 * fib (n + 1) :=
    le_trans fib_le_fib_succ (mul_comm 2 _ ▸ Nat.le_mul_of_pos_right _ two_pos)
  zify [this]
  ring

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

Goal state before:
pp: m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1))

Tactic:
rw [← fib_add n.pred _]

Goal state after:
m n : ℕ
h : n.pred.succ = n
⊢ (fib m).gcd (fib (n.pred + 1 + m)) = (fib m).gcd (fib (n.pred + m + 1))
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

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

Tactic:
obtain ⟨b, fr⟩ := ifp_n

Goal state after:
case succ.some
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 }
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
m' n' : ℕ
IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m' + 1 ≤ n' + 1
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)

Tactic:
rcases m' with - | m''

Goal state after:
case succ.succ.zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' : ℕ
IH : ∀ m < 0 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : 0 + 1 ≤ n' + 1
⊢ g.contsAux (0 + 1) = (g.squashGCF (n' + 1)).contsAux (0 + 1)

case succ.succ.succ
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: 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' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → g'.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
intro gp' m m_lt_n s_mth_eq'

Goal state after:
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' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
this : g.convs (n + 1) = g'.convs n
gp' : Pair K
m : ℕ
m_lt_n : m < n
s_mth_eq' : g'.s.get? m = some gp'
⊢ 0 < gp'.a ∧ 0 < gp'.b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x ∈ {z}) ∧ y ∉ {z} ∧ {z}.Nodup

Tactic:
mem_singleton,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ y ∉ {z} ∧ {z}.Nodup
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ e default = 1 → IsIdempotentElem (e default)

Tactic:
exact (· ▸ IsIdempotentElem.one)

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
⊢ x ∈ (f.genEigenspace μ) ↑k ↔ x ∈ ((f - μ • 1) ^ k).ker

Tactic:
by
  rw [mem_genEigenspace]
  constructor
  · rintro ⟨l, hl, hx⟩
    simp only [Nat.cast_le] at hl
    exact (f - μ • 1).iterateKer.monotone hl hx
  · intro hx
    exact ⟨k, le_rfl, hx⟩

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 m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ ⊥

Tactic:
← hk

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ (f.genEigenspace μ) m
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₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this✝ : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
this : ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
⊢ ((l₁ + l₂).choose (i, j).1 • ((f₁ - μ₁ • 1) ^ (i, j).1 * (f₂ - μ₂ • 1) ^ (i, j).2)) m = 0

Tactic:
rw [LinearMap.smul_apply, this, smul_zero]

Goal state after:
Module: Mathlib.Algebra.Exact.Sequence

Goal state before:
pp: case refine_2
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
i : Fin n
⊢ ↑(finrank k (V i.succ.castSucc)) = ↑(finrank k ↥(f i.castSucc).range) + ↑(finrank k ↥(f i.succ).range)

pp: case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)

Tactic:
· #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
      ```
      grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
      ```
      -/
    have hrn := (f i.succ).finrank_range_add_finrank_ker
    have hker : finrank k ↥(LinearMap.ker (f i.succ)) =
        finrank k ↥(LinearMap.range (f i.castSucc)) :=
      congrArg (fun S : Submodule k (V i.succ.castSucc) => finrank k ↥S)
        (h_exact i).linearMap_ker_eq
    omega

Goal state after:
case refine_3
k : Type u_1
inst✝³ : DivisionRing k
n : ℕ
V : Fin (n + 2) → Type u_2
inst✝² : (i : Fin (n + 2)) → AddCommGroup (V i)
inst✝¹ : (i : Fin (n + 2)) → Module k (V i)
inst✝ : ∀ (i : Fin (n + 2)), FiniteDimensional k (V i)
f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ
h_exact : ∀ (i : Fin n), Exact ⇑(f i.castSucc) ⇑(f i.succ)
inj : finrank k ↥(f 0).range = finrank k (V (Fin.castSucc 0))
surj : (f (Fin.last n)).range = ⊤
⊢ ↑(finrank k (V (Fin.last (n + 1)))) = ↑(finrank k ↥(f (Fin.last n)).range)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case pos
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2
⊢ Red (hd1 :: tl1) tl2

Tactic:
cases hd1

Goal state after:
case pos.mk
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
fst✝ : α
snd✝ : Bool
h : (fst✝, snd✝).1 = hd2.1 ∧ (fst✝, snd✝).2 = !hd2.2
⊢ Red ((fst✝, snd✝) :: tl1) tl2
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))

Tactic:
| cons hd1 tl1 ih =>

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
⊢ Function.Injective ⇑i₃

Tactic:
rw [injective_iff_map_eq_one]

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
⊢ ∀ (a : M₃), i₃ a = 1 → a = 1
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀

Tactic:
rw [max_eq_left hα, max_eq_left (hα.trans <| Cardinal.le_mul_right two_ne_zero),
        Cardinal.mul_eq_left hα _ (by simp)]
      exact natCast_le_aleph0.trans hα

Goal state after: