mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : NoZeroDivisors R
inst✝² : NonAssocSemiring A
inst✝¹ : Nontrivial A
f : R →+* A
p : ℕ
hp : p ≠ 0
inst✝ : CharP R p
⊢ CharP A p

Tactic:
by
  have := f.domain_nontrivial
  have H := (CharP.char_is_prime_or_zero R p).resolve_right hp
  obtain ⟨q, hq⟩ := CharP.exists A
  obtain ⟨k, e⟩ := dvd_of_ringHom f p q
  have := Nat.isUnit_iff.mp ((H.2 e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))
  rw [this, mul_one] at e
  exact e ▸ hq

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

Goal state before:
pp: case prime
R : Type u_1
A : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
this : CharP R p
⊢ ExpChar R p

Tactic:
exact .prime hp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Tactic:
nth_rw 1 [← mul_one (ringChar R)] at hq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul.zero
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)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
r' : A ⊗[R] S
y : ↥(RingHom.ker (algebraMap S T))
⊢ e₄'.symm (r' • 0 ⊗ₜ[S] y) = r' • e₄'.symm (0 ⊗ₜ[S] y)

Tactic:
simp only [zero_tmul, smul_zero, LinearEquiv.map_zero]

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

Goal state before:
pp: case tmul.add
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)
φ : A ⊗[R] S →ₐ[A] A ⊗[R] T := TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S T)
ePp : A ⊗[R] S ≃ₐ[S] S ⊗[R] A :=
  let __spread.0 := TensorProduct.comm R A S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₃ : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] ↥(RingHom.ker (algebraMap S T)) :=
  LinearEquiv.restrictScalars R ((IsScalarTower.toAlgHom R S T).toLinearMap.kerLTensorEquivOfSurjective h₁ A)
e₄' : ↥(RingHom.ker φ) ≃ₗ[R] A ⊗[R] S ⊗[S] ↥(RingHom.ker (algebraMap S T)) :=
  e₃ ≪≫ₗ _root_.TensorProduct.comm R A ↥(RingHom.ker (algebraMap S T)) ≪≫ₗ
        LinearEquiv.restrictScalars R
          (AlgebraTensorModule.cancelBaseChange R S S (↥(RingHom.ker (algebraMap S T))) A).symm ≪≫ₗ
      LinearEquiv.restrictScalars R
        (AlgebraTensorModule.congr (LinearEquiv.refl S ↥(RingHom.ker (algebraMap S T))) ↑ePp.symm) ≪≫ₗ
    LinearEquiv.restrictScalars R (_root_.TensorProduct.comm S (↥(RingHom.ker (algebraMap S T))) (A ⊗[R] S))
r' : A ⊗[R] S
y✝ : ↥(RingHom.ker (algebraMap S T))
x y : A ⊗[R] S
a✝¹ : e₄'.symm (r' • x ⊗ₜ[S] y✝) = r' • e₄'.symm (x ⊗ₜ[S] y✝)
a✝ : e₄'.symm (r' • y ⊗ₜ[S] y✝) = r' • e₄'.symm (y ⊗ₜ[S] y✝)
⊢ e₄'.symm (r' • (x + y) ⊗ₜ[S] y✝) = r' • e₄'.symm ((x + y) ⊗ₜ[S] y✝)

Tactic:
simp only [smul_add, add_tmul, LinearEquiv.map_add, *]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(Submodule.toAddSubgroup I).index = 0

Tactic:
by
  rw [AddSubgroup.index, Nat.card_eq]
  split_ifs with hq; swap
  · simp
  let : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq
  exact Nat.cast_card_eq_zero (R ⧸ I)

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ (fun a' ↦ (a', s.tail)) <$> s.get? 0 = none → s = nil

Tactic:
rcases f0 : get? s 0

Goal state after:
case none
α : Type u
s : Seq α
f0 : s.get? 0 = none
⊢ (fun a' ↦ (a', s.tail)) <$> none = none → s = nil

case some
α : Type u
s : Seq α
val✝ : α
f0 : s.get? 0 = some val✝
⊢ (fun a' ↦ (a', s.tail)) <$> some val✝ = none → s = nil
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁ s₂
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ IsBisimulation motive

Tactic:
intro s₁ s₂ h

Goal state after:
α : Type u
s₁✝ s₂✝ : Seq α
motive : Seq α → Seq α → Prop
base : motive s₁✝ s₂✝
step :
  ∀ (s₁ s₂ : Seq α),
    motive s₁ s₂ → s₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
s₁ s₂ : Seq α
h : motive s₁ s₂
⊢ BisimO motive s₁.destruct s₂.destruct
Module: Mathlib.Algebra.ContinuedFractions.Basic

Goal state before:
pp: α : Type u_1
inst✝ : One α
a : α
n : ℕ
aₙ : α
h : (GenContFract.ofInteger a).partNums.get? n = some aₙ
⊢ aₙ = 1

Tactic:
by cases h

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

Goal state before:
pp: α : Type u_1
inst✝² : One α
inst✝¹ : Zero α
inst✝ : LT α
a : α
n : ℕ
bₙ : α
h : (↑(SimpContFract.ofInteger a)).partDens.get? n = some bₙ
⊢ 0 < bₙ

Tactic:
by cases h

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

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
⊢ a = b → x ++ₛ a = x ++ₛ b

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u
n : ℕ
x : List α
a : Stream' α
⊢ x ++ take n a = take (x.length + n) (x ++ₛ a)

Tactic:
by
  induction x <;> simp [take, Nat.add_comm, cons_append_stream, *]

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

Goal state before:
pp: case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
h✝ : s.get? x✝ = none
k : ℕ
⊢ k ≤ n → ¬s.get? k = none

Tactic:
hkn

Goal state after:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
h✝ : s.get? x✝ = none
k : ℕ
hkn : k ≤ n
⊢ ¬s.get? k = none
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
z : FreeCommRing ((i : ι) × G i)
x' y' : FreeCommRing ((i : ι) × G i)
i : ι
x : G i
hx :
  (of G f i) x =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      x'
j : ι
y : G j
hy :
  (of G f j) y =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      y'
k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ (of G f k) (f i k hik x + f j k hjk y) =
    (Ideal.Quotient.mk
        (Ideal.span
          {a |
            (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
              (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
                (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
                  ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
      (x' + y')

Tactic:
by rw [map_add, of_f, of_f, hx, hy]; rfl

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

Goal state before:
pp: case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (initsCore l s).tail.get n = (initsCore (a :: l) s).get (n + 1)

Tactic:
inits_core_eq,

Goal state after:
case succ
α : Type u
a : α
n : ℕ
ih : ∀ (l : List α) (s : Stream' α), a :: (initsCore l s).get n = (initsCore (a :: l) s).get n
l : List α
s : Stream' α
⊢ a :: (l :: initsCore (l ++ [s.head]) s.tail).tail.get n = (initsCore (a :: l) s).get (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ g.contsAux (n + 1 + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
contsAux_recurrence nth_s_eq nth_contsAux_eq succ_nth_contsAux_eq

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b } =
    { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
n : ℕ
h2 : (f a).Results b n
this : a ∈ s
⊢ ∀ {m : ℕ}, (pure a).Results a m → ((pure a).bind f).Results b (n + m)

Tactic:
intro _ h1
    rw [ret_bind]
    rw [h1.len_unique (results_pure _)]
    exact h2

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

Goal state before:
pp: α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ s'✝.append s₂
⊢ a ∈ (cons b✝ s'✝).append s₂

Tactic:
simp [*]

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

Goal state before:
pp: case nil
α : Type u
l' : List α
⊢ ↑([] ++ l') = (↑[]).append ↑l'

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u
l' : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ↑(tail✝ ++ l') = (↑tail✝).append ↑l'
⊢ ↑(head✝ :: tail✝ ++ l') = (↑(head✝ :: tail✝)).append ↑l'

Tactic:
simp [*]

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
⊢ Option.map (fun p ↦ { a := 1, b := ↑p.b }) ((IntFractPair.stream v).tail.get 0) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })

Tactic:
rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (match IntFractPair.stream v (Nat.succ 0) with
    | some x => some { a := 1, b := ↑x.b }
    | none => none) =
    (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b })
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝¹ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) (f✝ i j hij x) = (g✝¹ i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g✝ : (i : ι) → G i →+* G' i
hg : ∀ (i j : ι) (h : i ≤ j), (g✝ j).comp (f i j h) = (f' i j h).comp (g✝ i)
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j) ((f i j h) g) = (f' i j h) ((g✝ i) g)
⊢ (of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) j) ((g✝ j) ((f i j h) g)) = (of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) i) ((g✝ i) g)

Tactic:
eq1,

Goal state after:
ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f✝ : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g✝¹ : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝¹ j) (f✝ i j hij x) = (g✝¹ i) x
f'✝ f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst✝ : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g✝ : (i : ι) → G i →+* G' i
hg : ∀ (i j : ι) (h : i ≤ j), (g✝ j).comp (f i j h) = (f' i j h).comp (g✝ i)
i j : ι
h : i ≤ j
g : G i
eq1 : (g✝ j) ((f i j h) g) = (f' i j h) ((g✝ i) g)
⊢ (of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) j) ((f' i j h) ((g✝ i) g)) = (of G' (fun x x_1 h ↦ ⇑(f' x x_1 h)) i) ((g✝ i) g)
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:
intro ifp_succ_n

Goal state after:
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_succ_n : IntFractPair K
⊢ IntFractPair.stream v (n + 1) = some ifp_succ_n →
    v = compExactValue ((of v).contsAux (n + 1)) ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v = 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
    rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }

Tactic:
obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
q : ℚ
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := ↑⌊↑q⌋, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := ↑⌊↑q⌋, s := s }
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:
intro ifp_succ_n

Goal state after:
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_succ_n : IntFractPair ℚ
⊢ IntFractPair.stream q (n + 1) = some ifp_succ_n → ifp_succ_n.fr.num ≤ (IntFractPair.of q).fr.num - ↑(n + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case some
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
n : ℕ := fract_q_num.natAbs + 1
ifp : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n :=
      stream_nth_fr_num_le_fr_num_sub_n_rat stream_nth_eq
    have : fract_q_num - n = -1 := by
      have : 0 ≤ fract_q_num := Rat.num_nonneg.mpr (Int.fract_nonneg q)
      simp only [n, Nat.cast_add, Int.natAbs_of_nonneg this, Nat.cast_one,
        sub_add_eq_sub_sub_swap, sub_right_comm, sub_self, zero_sub]
    have : 0 ≤ ifp.fr := (nth_stream_fr_nonneg_lt_one stream_nth_eq).left
    have : 0 ≤ ifp.fr.num := Rat.num_nonneg.mpr this
    lia

Goal state after:
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
b✝ : K
⊢ g.partDens.get? n = some b✝ → b✝ ≠ 0

Tactic:
nth_partDen_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
b✝ : K
nth_partDen_eq : g.partDens.get? n = some b✝
⊢ b✝ ≠ 0
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
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b

Tactic:
have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by
    cases n with
    | zero => exact Or.inl <| le_refl 1
    | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ ↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_4
inst✝ : CommSemiring R
x y : R
⊢ CompleteOrthogonalIdempotents ![x, y] ↔ x * y = 0 ∧ x + y = 1

Tactic:
by
  rw [pair_iff'ₛ, and_left_comm, and_iff_right_of_imp]; exact (mul_comm x y ▸ ·.1)

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

Goal state before:
pp: case inr
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
· apply one_div_le_one_div_of_le
    · have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)
      apply_rules [mul_pos]
    · conv_rhs => rw [mul_comm]
      gcongr
      exact le_of_succ_get?_den nth_partDen_eq

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ.none
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' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm none) =
    e ((finSuccEquiv n).symm none)

Tactic:
simp [*]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case succ.some
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' : Fin n → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fin.succEmb n)
h₂' : ∀ (i : Fin n), f (e' i) = e i.succ
e₀ : R
h₃ : IsIdempotentElem e₀
h₄ : f e₀ = e 0
h₅ : e₀ * ∑ i, e' i = 0
h₆ : (∑ i, e' i) * e₀ = 0
i : Fin n
⊢ (⇑f ∘ (fun x ↦ x.elim e₀ e') ∘ ⇑(finSuccEquiv n).toEmbedding) ((finSuccEquiv n).symm (some i)) =
    e ((finSuccEquiv n).symm (some i))

Tactic:
simp [*]

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

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
c : Con M
f : ι → M
⊢ ↑(List.map f []).prod = (List.map (fun i ↦ ↑(f i)) []).prod

Tactic:
simp [*]

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 : ι → M
head✝ : ι
tail✝ : List ι
tail_ih✝ : ↑(List.map f tail✝).prod = (List.map (fun i ↦ ↑(f i)) tail✝).prod
⊢ ↑(List.map f (head✝ :: tail✝)).prod = (List.map (fun i ↦ ↑(f i)) (head✝ :: tail✝)).prod

Tactic:
simp [*]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective
    (⇑(piFinTwoEquiv fun i ↦ R ⧸ Ideal.span {o i}) ∘ ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {o i})))

Tactic:
rw [(Equiv.bijective _).of_comp_iff']

Goal state after:
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {o i}))