mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.FinitePresentation

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i : J
⊢ ∀ (j : J) (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj

Tactic:
j

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
⊢ ∀ (xi : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj i))
    (xj : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op S)).obj j)),
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) xi =
        (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) xi =
          (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) xj
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
⊢ PreservesLimit (parallelPair f g) (R.tensorProd S) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
let c : Fork f g := Under.equalizerFork f g
  let hc : IsLimit c := Under.equalizerForkIsLimit f g
  let ι : R.mkUnder (AlgHom.equalizer (toAlgHom f) (toAlgHom g)) ⟶ A :=
    (AlgHom.equalizer (toAlgHom f) (toAlgHom g)).val.toUnder
  let h' := (R.tensorProd S).map ι
  have w' : h' ≫ (tensorProd R S).map f = h' ≫ (tensorProd R S).map g := by
    simpa using! congr((R.tensorProd S).map $(CommRingCat.Under.equalizer_comp f g))
  let e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') :=
    isLimitMapConeForkEquiv (tensorProd R S) (Under.equalizer_comp f g)
  rw [preservesLimit_iff_isLimit_mapCone hc, e.nonempty_congr,
    (Under.equalizerForkIsLimit _ _).nonempty_isLimit_iff_isIso_lift]
  have heq : (Under.equalizerForkIsLimit _ _).lift (Fork.ofι h' w') =
      (AlgHom.tensorEqualizer S S (toAlgHom f) (toAlgHom g)).toUnder ≫
        Under.homMk (CommRingCat.ofHom (.id _)) := by
    refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
    rw [Fork.IsLimit.lift_ι]
    ext : 2
    dsimp
    ext x <;> rfl
  rw [heq, ← isIso_iff_of_reflects_iso _ (CategoryTheory.Under.forget S),
    ConcreteCategory.isIso_iff_bijective]
  rfl

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
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
m : M
x : ↥f.ker
⊢ ((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f)) m) x = ((AlgebraTensorModule.curry id) m) x

Tactic:
apply (Module.Flat.lTensor_preserves_injective_linearMap (ker f).subtype
        (ker f).injective_subtype)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f g : N →ₗ[R] P
inst✝ : Module.Flat R M
m : M
x : ↥f.ker
⊢ (lTensor M f.ker.subtype) (((AlgebraTensorModule.curry (tensorKerInv S M f ∘ₗ tensorKer S M f)) m) x) =
    (lTensor M f.ker.subtype) (((AlgebraTensorModule.curry id) m) x)
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ p > 0, MixedCharZero R p → P) → ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P

pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P

Tactic:
· intro h q q_prime q_mixedChar
    exact h q (Nat.Prime.pos q_prime) q_mixedChar

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑↑n = ↑↑n

Tactic:
change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n
  simp only [IsUnit.unit_spec]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Nonempty (Algebra ℚ R)

Tactic:
apply Nonempty.intro

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Algebra ℚ R
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p : R
ψ θ : R ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
⊢ z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))

Tactic:
induction ψ using Quotient.inductionOn
  induction θ using Quotient.inductionOn
  simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
    QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]
  exact AddSubgroup.zsmul_mem_zmultiples_iff_exists_sub_div hz

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

Goal state before:
pp: α : Type u
n : ℕ
s : Stream' α
⊢ (take n s).length = n

Tactic:
induction n generalizing s

Goal state after:
case zero
α : Type u
s : Stream' α
⊢ (take 0 s).length = 0

case succ
α : Type u
n✝ : ℕ
a✝ : ∀ (s : Stream' α), (take n✝ s).length = n✝
s : Stream' α
⊢ (take (n✝ + 1) s).length = n✝ + 1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ⟨f, al⟩.val m = some a → ⟨f, al⟩.val n = some a

Tactic:
induction h with
  | refl => exact id
  | step _ IH => exact fun h2 ↦ al (IH h2)

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

Goal state before:
pp: case succ.some
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
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)

Tactic:
have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]

Goal state after:
case succ.some
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
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : s.tail.TerminatedAt n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
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
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_eq_zero : ifp_n.fr = 0
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
by
  grind [IntFractPair.stream]

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

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i : ℕ
⊢ ∀ (j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y

Tactic:
j

Goal state after:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
i j : ℕ
⊢ i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i : ℕ
⊢ ∀ (j : ℕ), i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y

Tactic:
j

Goal state after:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
⊢ i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i : ℕ
⊢ ∀ (j : ℕ), i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y

Tactic:
j

Goal state after:
α : Type u
R : α → α → Prop
inst✝ : IsTrans α R
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl
h_succ : ∀ {n : ℕ} {x y : α}, s.get? n = some x → s.get? (n + 1) = some y → R x y
i j : ℕ
⊢ i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ.none
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

pp: case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
· use pred_conts
          have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
            contsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
          simp only [g, this, pred_conts_eq]

Goal state after:
case succ.succ.some
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: 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, ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
rcases (exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩

Goal state after:
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, ∀ n ≥ N, |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ ∃ q, (of v).dens n = ↑q

Tactic:
by
  rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩
  use b
  simp [den_eq_conts_b, nth_cont_eq]

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

Goal state before:
pp: case zero
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' (0 + 1) = (g.squashGCF 0).convs' 0

Tactic:
cases g_s_head_eq : g.s.get? 0 <;>
      simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]

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

Goal state before:
pp: q : ℚ
fract_q_num : ℤ := (Int.fract q).num
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
let n := fract_q_num.natAbs + 1

Goal state after:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
⊢ ∃ n, IntFractPair.stream q n = none
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
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
⊢ ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
intro _ _ 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
terminatedAt_n : g.TerminatedAt n
g'_eq_g : g' = g
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.ContinuedFractions.Computation.Approximations

Goal state before:

Tactic:
(0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
        _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

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

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this : g.TerminatedAt n
⊢ (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
have : g.dens (n + 1) = g.dens n :=
      dens_stable_of_terminated n.le_succ this

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
g : GenContFract K := of v
terminated : g.partDens.TerminatedAt n
this✝ : g.TerminatedAt n
this : g.dens (n + 1) = g.dens n
⊢ (of v).dens n ≤ (of v).dens (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
n_eq_zero : n = 0
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
simp [n_eq_zero]

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

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
n_eq_zero : n = 0
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
simp [n_eq_zero]

Goal state after:
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
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.a * φ P.a * (x - y) * (x - z) * (y - z) * (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i : I
⊢ ∀ ⦃j : I⦄, i ≠ j → (fun x1 x2 ↦ Pi.single x1 1 * Pi.single x2 1 = 0) i j

Tactic:
j

Goal state after:
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
⊢ i ≠ j → (fun x1 x2 ↦ Pi.single x1 1 * Pi.single x2 1 = 0) i j
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
⊢ ¬f (smulRight v u) = 0

Tactic:
EmbeddingLike.map_eq_zero_iff,

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
⊢ ¬smulRight v u = 0
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
⊢ ∃ T, f = conjAlgEquiv K T

Tactic:
by_cases! hV : Subsingleton V
  · nontriviality W
    simpa using congr(f $(Subsingleton.allEq 0 1))
  simp_rw [AlgEquiv.ext_iff, conjAlgEquiv_apply, ← comp_assoc, eq_comp_toLinearMap_symm]
  obtain ⟨u, hu⟩ := exists_ne (0 : V)
  obtain ⟨v, huv⟩ := Projective.exists_dual_ne_zero K hu
  obtain ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : End K W) z := by
    rw [← not_forall, ← LinearMap.ext_iff, EmbeddingLike.map_eq_zero_iff, LinearMap.ext_iff]
    exact not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩
  set T := applyₗ z ∘ₗ f.toLinearMap ∘ₗ smulRightₗ v
  have hT x : T x = f (smulRight v x) z := rfl
  have this A x : T (A x) = f A (T x) := by
    simp only [hT, ← End.mul_apply, ← map_mul]
    congr; ext; simp
  have surj : Function.Surjective T := fun w ↦ by
    obtain ⟨d, hd⟩ := Projective.exists_dual_eq_one K hz
    exact ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
  have inj : Function.Injective T := fun x y hxy ↦ by
    have h_smul : smulRightₗ v x = smulRightₗ v y := by
      apply f.injective <| LinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)
  exact ⟨.ofBijective T ⟨inj, surj⟩, fun A ↦ (LinearMap.ext <| this A).symm⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₁ : S
he : e₁ ∈ f.range
he₁ : IsIdempotentElem e₁
e₂ : R
he₂ : IsIdempotentElem e₂
he₁e₂ : e₁ * f e₂ = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0

Tactic:
obtain ⟨e₁, rfl⟩ := he
  cases subsingleton_or_nontrivial R
  · exact ⟨_, Subsingleton.elim _ _, rfl, Subsingleton.elim _ _⟩
  let a := e₁ - e₁ * e₂
  have ha : f a = f e₁ := by rw [map_sub, map_mul, he₁e₂, sub_zero]
  have ha' : a * e₂ = 0 := by rw [sub_mul, mul_assoc, he₂.eq, sub_self]
  have hx' : a - a ^ 2 ∈ RingHom.ker f := by
    simp [RingHom.mem_ker, pow_two, ha, he₁.eq]
  obtain ⟨n, hn⟩ := h _ hx'
  refine ⟨_, isIdempotentElem_one_sub_one_sub_pow_pow _ _ hn, ?_, ?_⟩
  · rcases n with - | n
    · simp at hn
    simp only [map_sub, map_one, map_pow, ha, he₁.pow_succ_eq,
      he₁.one_sub.pow_succ_eq, sub_sub_cancel]
  · obtain ⟨k, hk⟩ := (Commute.one_left (MulOpposite.op <| 1 - a ^ n)).sub_dvd_pow_sub_pow n
    apply_fun MulOpposite.unop at hk
    have : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n := by simpa using hk
    rw [this, mul_assoc]
    rcases n with - | n
    · simp at hn
    rw [pow_succ, mul_assoc, ha', mul_zero, mul_zero]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i : n
⊢ ∀ (j : n), (M • N) i j ∈ ↑I.toAddSubmonoid

Tactic:
j

Goal state after:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ (M • N) i j ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
i : n
⊢ ∀ (j : n), (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid

Tactic:
j

Goal state after:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
i j : n
⊢ (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i : I
⊢ ∀ ⦃j : I⦄, i ≠ j → (fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})) i j

Tactic:
j

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
i j : I
⊢ i ≠ j → (fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})) i j
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case inr.inl
R : Type u_1
n : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon R
i j : n
x y : R
h : c x y
j' : n
hj : j ≠ j'
⊢ c (Matrix.single i j x i j') (Matrix.single i j y i j')

Tactic:
simpa [hj] using c.refl _

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

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
i : n
⊢ ∀ (j : n), (matrix n c) (single i j x) (single i j y)

Tactic:
j

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : c x y
i j : n
⊢ (matrix n c) (single i j x) (single i j y)