mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
⊢ (piRightHom R S A B) (0 * y) = (piRightHom R S A B) 0 * (piRightHom R S A B) y

pp: case tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * y) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) y

pp: case add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝ * y) = (piRightHom R S A B) x✝ * (piRightHom R S A B) y
a✝ : (piRightHom R S A B) (y✝ * y) = (piRightHom R S A B) y✝ * (piRightHom R S A B) y
⊢ (piRightHom R S A B) ((x✝ + y✝) * y) = (piRightHom R S A B) (x✝ + y✝) * (piRightHom R S A B) y

Tactic:
· simp

Goal state after:
case tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y : A ⊗[R] ((i : ι) → B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * y) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) y

case add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
y x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝ * y) = (piRightHom R S A B) x✝ * (piRightHom R S A B) y
a✝ : (piRightHom R S A B) (y✝ * y) = (piRightHom R S A B) y✝ * (piRightHom R S A B) y
⊢ (piRightHom R S A B) ((x✝ + y✝) * y) = (piRightHom R S A B) (x✝ + y✝) * (piRightHom R S A B) y
Module: Mathlib.RingTheory.TensorProduct.Pi

Goal state before:
pp: case tmul.zero
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝ * 0) = (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝) * (piRightHom R S A B) 0

pp: case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)

pp: case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) x✝
a✝ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * y✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) y✝
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * (x✝ + y✝)) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ + y✝)

Tactic:
· simp

Goal state after:
case tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ : A
y✝ : (i : ι) → B i
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝ ⊗ₜ[R] y✝) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ ⊗ₜ[R] y✝)

case tmul.add
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
ι : Type u_4
B : ι → Type u_5
inst✝¹ : (i : ι) → Semiring (B i)
inst✝ : (i : ι) → Algebra R (B i)
x✝¹ : A
y✝¹ : (i : ι) → B i
x✝ y✝ : A ⊗[R] ((i : ι) → B i)
a✝¹ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * x✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) x✝
a✝ : (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * y✝) = (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) y✝
⊢ (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹ * (x✝ + y✝)) =
    (piRightHom R S A B) (x✝¹ ⊗ₜ[R] y✝¹) * (piRightHom R S A B) (x✝ + y✝)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: case none
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app none = (conesEquivInverseObj B F X✝).π.app none

pp: case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app (some j) = (conesEquivInverseObj B F X✝).π.app (some j)

Tactic:
· simp

Goal state after:
case some
J✝ : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over B
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y✝).π.app (some j) = (conesEquivInverseObj B F X✝).π.app (some j)
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 P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ ↥(lTensor A f).ker ≃ₗ[R] A ⊗[R] ↥f.ker

Tactic:
by
  refine .ofEq _ _ ?_ ≪≫ₗ (LinearEquiv.ofInjective _ (LinearMap.lTensor_injective_of_exact_of_flat
    f hf _ (LinearMap.ker f).subtype_injective (LinearMap.exact_subtype_ker_map _) _)).symm
  rw [LinearMap.exact_iff.mp (lTensor_exact _ (LinearMap.exact_subtype_ker_map _) hf)]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Tactic:
· simp

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
hz' : ↑z ≠ 0
k : ℤ
h : k • p = z • r
⊢ k % z < ↑z.natAbs

Tactic:
exact (Int.emod_lt_abs _ hz).trans_eq (Int.abs_eq_natAbs _)

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

Goal state before:
pp: α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ some x = some y

Tactic:
← get?_cons_zero,

Goal state after:
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ (cons x ?s).get? 0 = some y

case s
α : Type u
x y : α
s t : Seq α
h : cons x s = cons y t
⊢ Seq α
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case cons.cons
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝¹ s✝¹) (cons x✝ s✝) →
    BisimO R (cons x✝¹ s✝¹).destruct (cons x✝ s✝).destruct →
      (cons x✝¹ s✝¹).head = (cons x✝ s✝).head ∧ R (cons x✝¹ s✝¹).tail (cons x✝ s✝).tail

Tactic:
· simp

Goal state after:
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₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
motive' : Seq α → Seq α → Prop := fun s₁ s₂ ↦ s₁ = s₂ ∨ motive s₁ s₂
⊢ motive' s₁ s₂

Tactic:
by grind

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

Goal state before:
pp: α : Type u
s₁✝ s₂✝ : Stream' α
hh : s₁✝.head = s₂✝.head
ht₁ : s₁✝ = s₁✝.tail
ht₂ : s₂✝ = s₂✝.tail
s₁ s₂ : Stream' α
x✝ : (fun s₁ s₂ ↦ s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁ s₂
h₁ : s₁.head = s₂.head
h₂ : s₁ = s₁.tail
h₃ : s₂ = s₂.tail
⊢ s₁.head = s₂.head ∧ (fun s₁ s₂ ↦ s₁.head = s₂.head ∧ s₁ = s₁.tail ∧ s₂ = s₂.tail) s₁.tail s₂.tail

Tactic:
by grind

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

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

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

Goal state after:
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]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
n : ℕ
⊢ take (n + 1 + 1) s = take (n + 1) s ++ [s.get (n + 1)]

Tactic:
by rw [take_succ, take_succ' n, ← List.cons_append, ← take_succ, get_tail]

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

Goal state before:
pp: case succ
α : Type u
xs : Stream' α
n : ℕ
⊢ (take (n + 1) xs).dropLast = take (n + 1 - 1) xs

Tactic:
| succ n =>

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

Goal state before:
pp: case succ
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
n : ℕ
a✝ : s₁.get n = s₂.get n
⊢ s₁.get (n + 1) = s₂.get (n + 1)

Tactic:
| succ n =>

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

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ↑n < s.length' ↔ ∃ a, a ∈ s.get? n

Tactic:
simp only [length'_of_not_terminates h, ENat.natCast_lt_top, Option.mem_def, true_iff]
    rw [not_terminates_iff] at h
    rw [← Option.isSome_iff_exists]
    exact h n

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

Goal state before:
pp: case r
α : Type u
β : Type v
a : α
f : α → Computation β
⊢ (pure a).bind f = (pure a).bind f ∧ f a = f a ∨ (pure a).bind f = corec (Bind.f f) (Sum.inr (f a))

Tactic:
· simp

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

Goal state before:
pp: 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
⊢ s.tail.TerminatedAt n

Tactic:
simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]

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

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
⊢ (IntFractPair.stream v).IsSeq

Tactic:
by
  intro _ hyp
  simp [IntFractPair.stream, hyp]

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

Goal state before:
pp: case succ
α : Type u
s : Seq α
n : ℕ
⊢ (s.drop (n + 1)).length' = s.length' - ↑(n + 1)

Tactic:
| succ n =>

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

Goal state before:
pp: case zero
α : Type u
s : Seq α
x : α
⊢ (cons x s).enum.get? 0 = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? 0

pp: case succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ (cons x s).enum.get? (n✝ + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n✝ + 1)

Tactic:
· simp

Goal state after:
case succ
α : Type u
s : Seq α
x : α
n✝ : ℕ
⊢ (cons x s).enum.get? (n✝ + 1) = (cons (0, x) (map (Prod.map Nat.succ id) s.enum)).get? (n✝ + 1)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr
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:
· rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]
    exact congr_arg (1 / ·) (by rw [convs', of_h_eq_floor, add_right_inj, of_s_tail])

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

Goal state before:
pp: case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
⊢ p x✝

Tactic:
· obtain ⟨_, _, hx'⟩ := exists_of_mem_map hx
    rw [← hx']
    solve_by_elim

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
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
ifp_succ_n_fr_ne_zero : ifp_succ_n.fr ≠ 0
this : compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts ifp_succ_n.fr
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
by grind

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

Goal state before:
pp: case succ.succ
α : 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
x y : α
k : ℕ
hy : y ∈ tl.get? k
n : ℕ
hx : x ∈ (Seq.cons hd tl).get? (n + 1)
h_ij : n + 1 < k + 1
⊢ R x y

Tactic:
| succ n =>

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

Goal state before:
pp: case zero
⊢ fib (2 * 0) = fib 0 * (2 * fib (0 + 1) - fib 0)

pp: case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))

Tactic:
· simp

Goal state after:
case succ
n✝ : ℕ
⊢ fib (2 * (n✝ + 1)) = fib (n✝ + 1) * (2 * fib (n✝ + 1 + 1) - fib (n✝ + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → false = true)

Tactic:
· simp

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

Goal state before:
pp: case nil
α : Type u
R : α → α → Prop
h : Pairwise R nil
⊢ Pairwise R nil.tail

pp: case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail

Tactic:
· simp

Goal state after:
case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case h
n : ℕ
⊢ (if false = true then
        ((fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2, (fib 0, fib 1).2 * (2 * (fib 0, fib 1).1 + (fib 0, fib 1).2))
      else
        ((fib 0, fib 1).1 * (2 * (fib 0, fib 1).2 - (fib 0, fib 1).1), (fib 0, fib 1).2 ^ 2 + (fib 0, fib 1).1 ^ 2)) =
      (fib 0, fib 1) ∨
    (n = 0 → true = true)

Tactic:
· simp

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

Goal state before:
pp: case inl
m : ℕ
⊢ (fib m).gcd (fib (0 + m)) = (fib m).gcd (fib 0)

pp: case inr
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)

Tactic:
· simp

Goal state after:
case inr
m n : ℕ
h : n > 0
⊢ (fib m).gcd (fib (n + m)) = (fib m).gcd (fib n)
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
⊢ g.convs (n + 1) = g'.convs' n

Tactic:
← IH

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
⊢ g.convs (n + 1) = g'.convs n

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
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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

Tactic:
obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n

Goal state after:
case refl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
⊢ 0 < gp'.a ∧ 0 < gp'.b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.zero
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
IH : ∀ m < 0 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : 0 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (0 + 1 - 2)
⊢ ↑(fib (0 + 1)) ≤ ((of v).contsAux (0 + 1)).b

pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
· simp

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
hyp : n + 1 = 0 ∨ ¬(of v).TerminatedAt (n + 1 - 1)
⊢ n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 - 1)

Tactic:
| succ n =>

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

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ (∑ i, (decompose V) (idempotent V i)) i = ((decompose V) 1) i

Tactic:
DFinsupp.finsetSum_apply

Goal state after:
R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i : I
⊢ ∑ a, ((decompose V) (idempotent V a)) i = ((decompose V) 1) i
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

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

pp: case succ.inl.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 + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
· simp

Goal state after:
case succ.inl.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 + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b
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
⊢ 0 ≤ ((of v).contsAux n).b

Tactic:
let g := of v
  induction n with
  | zero => rfl
  | succ n IH =>
    rcases Decidable.em <| g.TerminatedAt (n - 1) with terminated | not_terminated
    · -- terminating case
      rcases n with - | n
      · simp
      · have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
        simp only [g, this, IH]
    · -- non-terminating case
      calc
        (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: