mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
⊢ ∀ (s : Computation α),
    R r'.think s.think →
      BisimO R r'.think.destruct s.think.destruct → r'.think.head = s.think.head ∧ R r'.think.tail s.think.tail

Tactic:
intro a' r h

Goal state after:
case refine_2.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R r'.think a'.think
h : BisimO R r'.think.destruct a'.think.destruct
⊢ r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
⊢ (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail

Tactic:
constructor

Goal state after:
case refine_1.refine_1.left
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
⊢ (pure r').head = (pure a').head

case refine_1.refine_1.right
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (pure r').destruct (pure a').destruct
⊢ R (pure r').tail (pure a').tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
⊢ s.Results a n

Tactic:
let ⟨n', r, e⟩ := of_results_think h

Goal state after:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
e : n + 1 = n' + 1
⊢ s.Results a n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
s : Stream' α
⊢ zip appendStream' s.inits s.tails = const s

Tactic:
ext

Goal state after:
α : Type u
s : Stream' α
n✝¹ n✝ : ℕ
⊢ ((zip appendStream' s.inits s.tails).get n✝¹).get n✝ = ((const s).get n✝¹).get n✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
⊢ nil.toList ⋯ = []

Tactic:
ext

Goal state after:
α : Type u
i✝ : ℕ
a✝ : α
⊢ (nil.toList ⋯)[i✝]? = some a✝ ↔ [][i✝]? = some a✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).TerminatedAt = s.TerminatedAt

Tactic:
ext

Goal state after:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
x✝ : ℕ
⊢ (map f s).TerminatedAt x✝ ↔ s.TerminatedAt x✝
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
⊢ LiftRel R ca cb.think ↔ LiftRel R ca cb

Tactic:
rw [← LiftRel.swap R, ← LiftRel.swap R]; apply liftRel_think_left

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

Goal state before:
pp: α : Type u
β : Type v
s1 s2 : Computation α
f : α → β
h1 : s1 ~ s2
⊢ map f s1 ~ map f s2

Tactic:
by
  rw [← lift_eq_iff_equiv]
  exact liftRel_map Eq _ ((lift_eq_iff_equiv _ _).2 h1) fun {a} b => congr_arg _

Goal state after:
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
F : DirectLimit G f →+* P
⊢ lift G f P (fun i ↦ F.comp (of G f i)) ⋯ = F

Tactic:
ext

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
F : DirectLimit G f →+* P
i✝ : ι
x✝ : G i✝
⊢ ((lift G f P (fun i ↦ F.comp (of G f i)) ⋯).comp (of G f i✝)) x✝ = (F.comp (of G f i✝)) x✝
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
⊢ lift G f (DirectLimit G f) (of G f) ⋯ = RingHom.id (DirectLimit G f)

Tactic:
ext

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
i✝ : ι
x✝ : G i✝
⊢ ((lift G f (DirectLimit G f) (of G f) ⋯).comp (of G f i✝)) x✝ = ((RingHom.id (DirectLimit G f)).comp (of G f i✝)) x✝
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' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
⊢ (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯).comp
      (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯) =
    RingHom.id (_root_.DirectLimit G f')

Tactic:
ext

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' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i✝ : ι
x✝ : G i✝
⊢ (((lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯).comp
            (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯)).comp
        (Ring.of G f' i✝))
      x✝ =
    ((RingHom.id (_root_.DirectLimit G f')).comp (Ring.of G f' i✝)) x✝
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' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
⊢ (Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯).comp
      (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯) =
    RingHom.id (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3))

Tactic:
ext

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' : (i j : ι) → i ≤ j → G i →+* G j
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f' i j h)
inst✝¹ : IsDirectedOrder ι
inst✝ : Nonempty ι
i✝ : ι
x✝ : G i✝
⊢ (((Ring.lift G f' (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (of G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) ⋯).comp
            (lift G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) (_root_.DirectLimit G f') (Ring.of G f') ⋯)).comp
        (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i✝))
      x✝ =
    ((RingHom.id (DirectLimit G fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3))).comp (of G (fun x1 x2 x3 ↦ ⇑(f' x1 x2 x3)) i✝)) x✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
S T : Seq (Seq1 α)
⊢ (S.append T).join = S.join.append T.join

Tactic:
apply
    eq_of_bisim fun s1 s2 =>
      ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
  · rintro s1 s2 ⟨s, S, T, rfl, rfl⟩
    cases s with
    | nil =>
      cases S with
      | nil =>
        cases T with
        | nil => simp
        | cons s T =>
          obtain ⟨a, s⟩ := s
          simpa using ⟨s, nil, T, by simp, by simp⟩
      | cons s S =>
        obtain ⟨a, s⟩ := s
        simpa using ⟨s, S, T, rfl, rfl⟩
    | cons _ s => simpa using ⟨s, S, T, rfl, rfl⟩
  · exact ⟨nil, S, T, by simp, by simp⟩

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

Goal state before:
pp: α : Type u
s : Seq α
n m : ℕ
⊢ List.drop m (take n s) = take (n - m) (s.drop m)

Tactic:
ext

Goal state after:
α : Type u
s : Seq α
n m i✝ : ℕ
a✝ : α
⊢ (List.drop m (take n s))[i✝]? = some a✝ ↔ (take (n - m) (s.drop m))[i✝]? = some a✝
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
⊢ map (fun x ↦ RingHom.id (G x)) ⋯ = RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))

Tactic:
ext

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
i✝ : ι
x✝ : G i✝
⊢ ((map (fun x ↦ RingHom.id (G x)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((RingHom.id (DirectLimit G fun x x_1 h ↦ ⇑(f x x_1 h))).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝
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
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
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)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
⊢ (map g₂ hg₂).comp (map g₁ hg₁) = map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯

Tactic:
ext

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
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
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)
hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)
i✝ : ι
x✝ : G i✝
⊢ (((map g₂ hg₂).comp (map g₁ hg₁)).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝ =
    ((map (fun i ↦ (g₂ i).comp (g₁ i)) ⋯).comp (of G (fun x x_1 h ↦ ⇑(f x x_1 h)) i✝)) x✝
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
⊢ ↑⌊v⌋ + convs'Aux (of v).s (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
add_right_inj,

Goal state after:
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
⊢ convs'Aux (of v).s (n + 1) = 1 / (of (fract v)⁻¹).convs' n
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 : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n = ↑⌊(fract v)⁻¹⌋ + convs'Aux (of (fract v)⁻¹).s n

Tactic:
add_right_inj,

Goal state after:
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
n : ℕ
inst✝ : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ convs'Aux (of v).s.tail n = convs'Aux (of (fract v)⁻¹).s n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : cons b_hd b_tl ≠ nil
a_hd : α
a_tl : Seq α
ha' : a.drop (a.length ha) = cons a_hd a_tl
right✝ : motive a_tl b_tl
⊢ False

Tactic:
apply_fun length' at ha'

Goal state after:
case pos.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
ha : a.Terminates
hb : ¬b.TerminatedAt (a.length ha)
b_hd : β
b_tl : Seq β
this : motive (a.drop (a.length ha)) (cons b_hd b_tl)
hb_cons : cons b_hd b_tl ≠ nil
a_hd : α
a_tl : Seq α
right✝ : motive a_tl b_tl
ha' : (a.drop (a.length ha)).length' = (cons a_hd a_tl).length'
⊢ False
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case refine_1
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))

pp: case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))

Tactic:
· simp [fastFibAux]

Goal state after:
case refine_2
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), n.fastFibAux = (fib n, fib (n + 1)) → (bit b n).fastFibAux = (fib (bit b n), fib (bit b n + 1))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: ⊢ fib = fastFib

Tactic:
ext

Goal state after:
x✝ : ℕ
⊢ fib x✝ = x✝.fastFib
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
x✝ : Option (Pair K)
s_succ_nth_eq : s.get? (n + 1) = x✝
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
cases s_succ_nth_eq : s.get? (n + 1) with

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
v : K
q : ℚ
v_eq_q : v = ↑q
n : ℕ
⊢ Option.map (Pair.map Rat.cast) ((of q).s.get? n) = (of v).s.get? n

Tactic:
simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]
  simp only [Stream'.Seq.get?]
  rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]
  rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
    simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

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

Goal state before:
pp: q : ℚ
n : ℕ
ifp_n ifp_succ_n : IntFractPair ℚ
stream_nth_eq : IntFractPair.stream q n = some ifp_n
stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n
⊢ ifp_succ_n.fr.num < ifp_n.fr.num

Tactic:
by
  obtain ⟨ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n⟩ :
    ∃ ifp_n',
      IntFractPair.stream q n = some ifp_n' ∧
        ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
  have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
  cases this
  rw [← IntFractPair.of_eq_ifp_succ_n]
  obtain ⟨zero_le_ifp_n_fract, _⟩ := nth_stream_fr_nonneg_lt_one stream_nth_eq
  have : 0 < ifp_n.fr := lt_of_le_of_ne zero_le_ifp_n_fract <| ifp_n_fract_ne_zero.symm
  exact of_inv_fr_num_lt_num_of_pos this

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ Q.toPoly.coeff 0 = Q.d

Tactic:
coeff_eq_d

Goal state after:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ Q.d = Q.d
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ (C P.c * X + C P.d).leadingCoeff = P.c

Tactic:
leadingCoeff_linear hc

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.c = P.c
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ (fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) ((fun P ↦ ⟨P.toPoly, ⋯⟩) P) =
    P

Tactic:
ext

Goal state after:
case a
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).a =
    P.a

case b
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).b =
    P.b

case c
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).c =
    P.c

case d
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).d =
    P.d
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
⊢ (map φ P).roots.card = 3 ↔ ∃ x y z, (map φ P).roots = {x, y, z}

Tactic:
card_eq_three

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
⊢ (∃ x y z, (map φ P).roots = {x, y, z}) ↔ ∃ x y z, (map φ P).roots = {x, y, z}
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
inst✝ : DecidableEq K
ha : P.a ≠ 0
h3 : (Polynomial.map φ P.toPoly).Splits
hd : P.discr ≠ 0
⊢ (map φ P).roots.toFinset.card = 3

Tactic:
by
  rwa [toFinset_card_of_nodup <| (discr_ne_zero_iff_roots_nodup ha h3).mp hd,
    ← splits_iff_card_roots ha]

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 0 < den ∧ den ≤ den'

Tactic:
constructor

Goal state after:
case left
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := ⋯
nextConts : Pair K := ⋯
conts : Pair K := ⋯
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := ⋯
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := ⋯
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := ⋯
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 0 < den

case right
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := ⋯
nextConts : Pair K := ⋯
conts : Pair K := ⋯
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := ⋯
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := ⋯
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := ⋯
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ den ≤ den'
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
m : M
⊢ (basisAux A b) (a ⊗ₜ[R] m) = a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
a : A
m : M
a✝ : ι
⊢ ((basisAux A b) (a ⊗ₜ[R] m)) a✝ = (a • Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)) a✝
Module: Mathlib.RingTheory.TensorProduct.Free

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst✝⁹ : Fintype ι
inst✝⁸ : Finite ι₂
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
⊢ (toMatrix (basis A b₁) (basis A b₂)) (baseChange A f) = ((toMatrix b₁ b₂) f).map ⇑(algebraMap R A)

Tactic:
ext

Goal state after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst✝⁹ : Fintype ι
inst✝⁸ : Finite ι₂
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
i✝ : ι₂
j✝ : ι
⊢ (toMatrix (basis A b₁) (basis A b₂)) (baseChange A f) i✝ j✝ = ((toMatrix b₁ b₂) f).map (⇑(algebraMap R A)) i✝ j✝