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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_zero : n = 0
⊢ q = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
q : ℕ
char_R_q : CharP R q
q_pos : ¬q = 0
K : Type u_1 := IsLocalRing.ResidueField R
RM_char : CharP K (ringChar K)
r : ℕ := ringChar K
n : ℕ := q.factorization r
r_prime : Nat.Prime r
a : ℕ := q / r ^ n
q_eq_a_mul_rn : q = a * r ^ n
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
a_unit : IsUnit ↑a
rn_cast_zero : ↑(r ^ n) = 0
q_eq_rn : q = r ^ n
n_zero : n = 0
⊢ q = 1
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case tmul.tmul
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 : A
z : S
⊢ e₄'.symm (r' • x ⊗ₜ[R] z ⊗ₜ[S] y) = r' • e₄'.symm (x ⊗ₜ[R] z ⊗ₜ[S] y)

Tactic:
| tmul x z =>

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑a - ↑b ≠ 0

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ¬↑a = ↑b
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case refine_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : L
hx : x ∈ lift (restrict h)
⊢ x ∈ F

Tactic:
let y : E := ⟨x, lift_le (restrict h) hx⟩
    exact (mem_restrict h y).1 ((mem_lift y).1 hx)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
n : ℕ
hn : n ≠ 0
⊢ n • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑n) ∈ zmultiples p

Tactic:
by
  rw [← natCast_zsmul r, zsmul_mem_zmultiples_iff_exists_sub_div (Int.natCast_ne_zero.mpr hn),
    Int.cast_natCast]
  rfl

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
h : cons x s = nil
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u
x : α
s : Seq α
h : cons x s = nil
⊢ False
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case mpr
α : Type u
x x' : α
s s' : Seq α
⊢ x = x' ∧ s = s' → cons x s = cons x' s'

Tactic:
intro ⟨_, _⟩

Goal state after:
case mpr
α : Type u
x x' : α
s s' : Seq α
left✝ : x = x'
right✝ : s = s'
⊢ cons x s = cons x' s'
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ (iterate f a).get (n + 1 + 1) = (iterate f (f a)).get (n + 1)

Tactic:
get_succ_iterate',

Goal state after:
case succ
α : Type u
f : α → α
a : α
n : ℕ
ih : (iterate f a).get (n + 1) = (iterate f (f a)).get n
⊢ f ((iterate f a).get (n + 1)) = (iterate f (f a)).get (n + 1)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero
α : Type u
C : Seq α → Prop
a : α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
s : Seq α
e : some a = ↑s 0
⊢ C s

Tactic:
have TH : s = cons a (tail s) := by
      apply destruct_eq_cons
      unfold destruct get? Functor.map
      rw [← e]
      rfl
    rw [TH]
    apply h1 _ _ (Or.inl rfl)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
l : List α
n : ℕ
h : l.length ≤ n
⊢ l.length ≤ n + 1

Tactic:
exact Nat.le_succ_of_le h

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

Goal state before:
pp: α : 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
⊢ n < x.length

Tactic:
simpa using

Goal state after:
α : 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
⊢ n < x.length
Module: Mathlib.Data.Stream.Init

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

Tactic:
simpa using

Goal state after:
α : Type u
x : List α
a b : Stream' α
n : ℕ
h : (x ++ₛ a).get (x.length + n) = (x ++ₛ b).get (x.length + n)
⊢ a.get n = b.get n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n

Tactic:
simpa using

Goal state after:
α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁.get 0 = s₂.get 0

Tactic:
simpa using

Goal state after:
case zero
α : Type u
s₁ s₂ : Stream' α
h : ∀ (n : ℕ), take n s₁ = take n s₂
⊢ s₁.get 0 = s₂.get 0
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
simpa using

Goal state after:
case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ s.TerminatedAt n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
simpa using

Goal state after:
case neg
α : Type u
s : Seq α
n : ℕ
h : ¬s.Terminates
⊢ ¬s.TerminatedAt n
Module: Mathlib.Data.Seq.Basic

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

Tactic:
simpa using

Goal state after:
case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∃ a, s.get? n = some a
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.s.get? n = none ↔ g.partNums.get? n = none

Tactic:
partNum_none_iff_s_none

Goal state after:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.s.get? n = none ↔ g.s.get? n = none
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
a : α
nth_partNum_eq : g.partNums.get? n = some a
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.a = a

Tactic:
simpa using

Goal state after:
α : Type u_1
g : GenContFract α
n : ℕ
a : α
nth_partNum_eq : g.partNums.get? n = some a
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.a = a
Module: Mathlib.Algebra.ContinuedFractions.Translations

Goal state before:
pp: α : Type u_1
g : GenContFract α
n : ℕ
b : α
nth_partDen_eq : g.partDens.get? n = some b
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.b = b

Tactic:
simpa using

Goal state after:
α : Type u_1
g : GenContFract α
n : ℕ
b : α
nth_partDen_eq : g.partDens.get? n = some b
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.b = b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
β : Type v
f : α → β
s✝ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : Computation α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s) (s.think.bind (pure ∘ f)).destruct
    (map f s.think).destruct

Tactic:
simpa using

Goal state after:
case think
α : Type u
β : Type v
f : α → β
s✝ : Computation α
c₁ c₂ : Computation β
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind (pure ∘ f) ∧ c₂ = map f s
s : Computation α
⊢ s.bind (pure ∘ f) = map f s ∨ ∃ s_1, s.bind (pure ∘ f) = s_1.bind (pure ∘ f) ∧ map f s = map f s_1
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
s : Computation α
⊢ s.bind pure = s

Tactic:
simpa using

Goal state after:
α : Type u
s : Computation α
⊢ s.bind pure = s
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.some
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
x : α
r : Seq α
⊢ (match some (x, r) with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1

Tactic:
simpa using

Goal state after:
case succ.some
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
x : α
r : Seq α
⊢ (take m r).length ≤ m
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case think
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : Computation α
⊢ BisimO (fun c₁ c₂ ↦ c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g)
    ((s.think.bind f).bind g).destruct (s.think.bind fun x ↦ (f x).bind g).destruct

Tactic:
simpa using

Goal state after:
case think
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = (s.bind f).bind g ∧ c₂ = s.bind fun x ↦ (f x).bind g
s : Computation α
⊢ ((s.bind f).bind g = s.bind fun x ↦ (f x).bind g) ∨
    ∃ s_1, (s.bind f).bind g = (s_1.bind f).bind g ∧ (s.bind fun x ↦ (f x).bind g) = s_1.bind fun x ↦ (f x).bind g
Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence

Goal state before:
pp: K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_den_eq : g.dens (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b

Tactic:
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
      ∃ conts, g.conts (n + 1) = conts ∧ conts.b = predB :=
    exists_conts_b_of_den succ_nth_den_eq

Goal state after:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
⊢ g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.nil.cons
α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    ((nil.append nil).append (cons x✝ u)).destruct (nil.append (nil.append (cons x✝ u))).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.nil.cons
α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ ∃ s t u_1, u = (s.append t).append u_1 ∧ u = s.append (t.append u_1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
s t✝ u✝ u : Seq α
x✝ : α
t : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    ((nil.append (cons x✝ t)).append u).destruct (nil.append ((cons x✝ t).append u)).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.cons
α : Type u
s t✝ u✝ u : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1 u_1, t.append u = (s.append t_1).append u_1 ∧ t.append u = s.append (t_1.append u_1)
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s).s.get? i = some gp
⊢ -((↑s).partNums.get? i).getD 0 = -1

Tactic:
rw [partNum_eq_s_a s_ith_eq, s.property i gp.a <| partNum_eq_s_a s_ith_eq, Option.getD_some]

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

Goal state before:
pp: case bisim.cons
α : Type u
s✝ t✝ u✝ t u : Seq α
x✝ : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    (((cons x✝ s).append t).append u).destruct ((cons x✝ s).append (t.append u)).destruct

Tactic:
simpa using

Goal state after:
case bisim.cons
α : Type u
s✝ t✝ u✝ t u : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1 u_1,
    (s.append t).append u = (s_1.append t_1).append u_1 ∧ s.append (t.append u) = s_1.append (t_1.append u_1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ s₂

Tactic:
simpa using

Goal state after:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a = c ∨ a ∈ t₁.append s₂

Tactic:
simpa using

Goal state after:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a = c ∨ a ∈ t₁.append s₂
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ c = b ∧ t₁.append s₂ = s'

Tactic:
simpa using

Goal state after:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ c = b ∧ t₁.append s₂ = s'
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil.cons
α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f (nil.append (cons x✝ t))).destruct ((map f nil).append (map f (cons x✝ t))).destruct

Tactic:
simpa using

Goal state after:
case nil.cons
α : Type u
β : Type v
f : α → β
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1, map f t = map f (s.append t_1) ∧ map f t = (map f s).append (map f t_1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
s✝ t✝ t : Seq α
x✝ : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t))
    (map f ((cons x✝ s).append t)).destruct ((map f (cons x✝ s)).append (map f t)).destruct

Tactic:
simpa using

Goal state after:
case cons
α : Type u
β : Type v
f : α → β
s✝ t✝ t : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1, map f (s.append t) = map f (s_1.append t_1) ∧ (map f s).append (map f t) = (map f s_1).append (map f t_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
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
seq_nth_eq : IntFractPair.stream v n = some ifp_n
left✝ : ifp_n.fr ≠ 0
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
succ_nth_fr_eq_zero : (IntFractPair.of ifp_n.fr⁻¹).fr = 0
⊢ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.pure
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
b : β
Hc : C ca'.think (pure b)
h : LiftRelAux R C ca'.think.destruct (pure b).destruct
⊢ LiftRel R ca' (pure b)

Tactic:
simpa using

Goal state after:
case refine_2.pure
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
b : β
Hc : C ca'.think (pure b)
h : LiftRelAux R C ca'.think.destruct (pure b).destruct
⊢ ∃ a, a ∈ ca' ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb.think
h : LiftRelAux R C ca'.think.destruct cb.think.destruct
⊢ LiftRel R ca' cb.think

Tactic:
simpa using

Goal state after:
case refine_2.think
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb.think
h : LiftRelAux R C ca'.think.destruct cb.think.destruct
⊢ LiftRel R ca' cb
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ BisimO (fun s1 s2 ↦ s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join))
    (cons (a, cons x✝ s✝) S).join.destruct (cons a ((cons x✝ s✝).append S.join)).destruct

Tactic:
simpa using

Goal state after:
case cons
α : Type u
a✝ : α
s : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
a : α
S : Seq (Seq1 α)
x✝ : α
s✝ : Seq α
⊢ (cons (x✝, s✝) S).join = cons x✝ (s✝.append S.join) ∨
    ∃ a s S_1, (cons (x✝, s✝) S).join = (cons (a, s) S_1).join ∧ cons x✝ (s✝.append S.join) = cons a (s.append S_1.join)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.nil.cons
α : Type u
S T✝ T : Seq (Seq1 α)
a : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (nil.append (nil.append (cons (a, s) T)).join).destruct (nil.append (nil.join.append (cons (a, s) T).join)).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.nil.cons
α : Type u
S T✝ T : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S T_1, s.append T.join = s_1.append (S.append T_1).join ∧ s.append T.join = s_1.append (S.join.append T_1.join)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
S✝ T✝ T S : Seq (Seq1 α)
a : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (nil.append ((cons (a, s) S).append T).join).destruct (nil.append ((cons (a, s) S).join.append T.join)).destruct

Tactic:
simpa using

Goal state after:
case bisim.nil.cons
α : Type u
S✝ T✝ T S : Seq (Seq1 α)
a : α
s : Seq α
⊢ ∃ s_1 S_1 T_1,
    s.append (S.append T).join = s_1.append (S_1.append T_1).join ∧
      s.append (S.join.append T.join) = s_1.append (S_1.join.append T_1.join)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
S✝ T✝ S T : Seq (Seq1 α)
x✝ : α
s : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    ((cons x✝ s).append (S.append T).join).destruct ((cons x✝ s).append (S.join.append T.join)).destruct

Tactic:
simpa using

Goal state after:
case bisim.cons
α : Type u
S✝ T✝ S T : Seq (Seq1 α)
x✝ : α
s : Seq α
⊢ ∃ s_1 S_1 T_1,
    s.append (S.append T).join = s_1.append (S_1.append T_1).join ∧
      s.append (S.join.append T.join) = s_1.append (S_1.join.append T_1.join)
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 : ℕ
gp_n : Pair K
s_nth_eq :
  (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      n =
    some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := ↑ifp.b } = gp_n

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
gp_n : Pair K
s_nth_eq :
  (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      n =
    some gp_n
⊢ ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ { a := 1, b := ↑ifp.b } = gp_n
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
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
⊢ IntFractPair.of v = ifp_zero

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
⊢ IntFractPair.of v = ifp_zero