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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
I : Ideal R
hI_not_top : I ≠ ⊤
right✝ : CharP (R ⧸ I) p
M : Ideal R
hM_max : M.IsMaximal
hM_ge : I ≤ M
r : ℕ
hr : CharP (R ⧸ M) r
⊢ r ∣ p

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
⊢ (S.toIntermediateField inv_mem).toSubalgebra = S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
⊢ S.toIntermediateField ⋯ = S

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : ℕ
inst✝ : CharP R p
S : Subsemiring R
x : ℕ
h : ↑x = 0
⊢ S.subtype ↑x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
⊢ RingHom.ker (algebraMap ℤ R) = Ideal.span {↑p}

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
S : Subring R
x : ℕ
h : ↑x = 0
⊢ S.subtype ↑x = 0

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : AddCommMonoidWithOne M
inst✝¹ : AddCommMonoidWithOne N
inst✝ : CharZero M
e : M →+ N
he : e 1 = 1
he' : Function.Injective ⇑e
n m : ℕ
h : ↑n = ↑m
⊢ n = m

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
S : Subalgebra K L
hS : IsField ↥S
x : L
hx : x ∈ S
⊢ x⁻¹ ∈ S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
hp : Nat.Prime p
⊢ (∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
hS : IsField ↥S
⊢ (S.toIntermediateField' hS).toSubalgebra = S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
⊢ S.toIntermediateField' ⋯ = S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : CharP R n
I : Ideal R
⊢ CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : ℕ
I : Ideal R
inst✝ : CharP (R ⧸ I) p
⊢ (Quotient.mk I) ↑p = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S✝ : IntermediateField K L
X : ?m.8
Y : ?m.9
f : L →ₐ[K] L'
S : IntermediateField K L
⊢ ∀ x ∈ (Subalgebra.map f S.toSubalgebra).carrier, x⁻¹ ∈ (Subalgebra.map f S.toSubalgebra).carrier

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
f : L →ₐ[K] L'
x : L
⊢ f x ∈ ↑(map f S) ↔ x ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
inst✝¹ : Algebra L L'
inst✝ : IsScalarTower K L L'
⊢ ↑(toAlgHom K L L').fieldRange = Set.range ⇑(algebraMap L L')

Tactic:
by

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

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Function.Injective toSubalgebra

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Function.Injective toSubfield

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑(Rat.num 1) /ₚ ↑(Rat.pnatDen 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
⊢ Function.Injective (map f)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ (algebraMap K L).fieldRange
⊢ x ∈ Set.range ⇑(algebraMap K L)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
E : IntermediateField K ↥F
⊢ lift E ≤ F

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
inst✝¹ : Algebra L' L
inst✝ : IsScalarTower K L' L
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ U ↔ x ∈ V

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F✝ E✝ F : IntermediateField K L
E : IntermediateField (↥F) L
⊢ Algebra K ↥E

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: F : Type u_4
inst✝⁴ : Field F
E : Type u_5
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_6
inst✝¹ : Field K
inst✝ : Algebra F K
L : IntermediateField F E
f : E →ₐ[F] K
⊢ (f.comp L.val).fieldRange.toSubalgebra = (map f L).toSubalgebra

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S : IntermediateField K L
F E✝ E'✝ : Subfield L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨E.toSubfield, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E ≤
      { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨E.toSubfield, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E' ↔
    E ≤ E'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ∀ (x y : ℚ), ↑(x * y).num /ₚ ↑(x * y).pnatDen = ↑x.num /ₚ ↑x.pnatDen * (↑y.num /ₚ ↑y.pnatDen)

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
S F E✝ E'✝ : IntermediateField K L
h : F ≤ E✝
h' : F ≤ E'✝
x : L
E E' : { E // F ≤ E }
⊢ { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨restrictScalars K E, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } E ≤
      { toFun := fun E ↦ extendScalars ⋯, invFun := fun E ↦ ⟨restrictScalars K E, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
        E' ↔
    E ≤ E'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑(Rat.num 0) /ₚ ↑(Rat.pnatDen 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: 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
⊢ lift (restrict h) = F

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ∀ (x y : ℚ), ↑(x + y).num /ₚ ↑(x + y).pnatDen = ↑x.num /ₚ ↑x.pnatDen + ↑y.num /ₚ ↑y.pnatDen

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
h : ∀ p > 0, ¬MixedCharZero R p
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ ∀ p > 0, ¬MixedCharZero R p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
⊢ IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : CharZero R
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Prop
h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsDomain R
h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : ∀ (a : Algebra ℚ R), P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
by

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
z : ℤ
hz : z ≠ 0
⊢ z • r ∈ zmultiples p ↔ ∃ k, r - ↑k • (p / ↑z) ∈ zmultiples p

Tactic:
by

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

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 ⧸ AddSubgroup.zmultiples p
z : ℤ
hz : z ≠ 0
⊢ z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))

Tactic:
by

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 ⧸ AddSubgroup.zmultiples p
n : ℕ
hz : n ≠ 0
⊢ n • ψ = n • θ ↔ ∃ k, ψ = θ + ↑k • ↑(p / ↑n)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
m n : ℕ
h : m ≤ n
⊢ s.get? m = none → s.get? n = none

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
aₙ : α
n m : ℕ
m_le_n : m ≤ n
s_nth_eq_some : s.get? n = some aₙ
⊢ s.get? n ≠ none

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
⊢ (some a :: ↑s).IsSeq

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.get? 0 = none ↔ s = nil

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
s : Seq α
⊢ cons x s ≠ nil

Tactic:
by

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
⊢ x = y

Tactic:
by

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
n : ℕ
⊢ s.get? n = t.get? n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n✝ : ℕ
n' : (↑s).tail n✝ = none
⊢ (↑s).tail (n✝ + 1) = none

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.head = Prod.fst <$> s.destruct

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ (cons a ⟨f, al⟩).destruct = some (a, ⟨f, al⟩)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.destruct = none → s = nil

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
a : α
s' : Seq α
⊢ s.destruct = some (a, s') → s = cons a s'

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ (cons a s).head = some a

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s = cons x s.tail

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Seq α
⊢ s.head = none ↔ s = nil

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
motive : Seq α → Sort v
s : Seq α
nil : motive Seq.nil
cons : (x : α) → (s : Seq α) → motive (Seq.cons x s)
⊢ motive s

Tactic:
by

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

Goal state before:
pp: case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ corec' (Corec.f f) o (n + 1) = none →
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none

Tactic:
Stream'.corec'_eq (Corec.f f) o

Goal state after:
case succ
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
n : ℕ
IH : ∀ (o : Option β), corec' (Corec.f f) o n = none → corec' (Corec.f f) (Corec.f f o).snd n = none
o : Option β
⊢ ((Corec.f f o).fst :: corec' (Corec.f f) (Corec.f f o).snd) (n + 1) = none →
    ((Corec.f f (Corec.f f o).snd).fst :: corec' (Corec.f f) (Corec.f f (Corec.f f o).snd).snd) (n + 1) = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ Seq α

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Stream' α
i : ℕ
⊢ (s.head :: s.tail) i = s i

Tactic:
by

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

Goal state before:
pp: α : Type u
n m : ℕ
s : Stream' α
⊢ (drop m s).get n = s.get (m + n)

Tactic:
by

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

Goal state before:
pp: α : Type u
n m : ℕ
s : Stream' α
⊢ drop n (drop m s) = drop (m + n) s

Tactic:
by

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

Goal state before:
pp: α : Type u
i : ℕ
s : Stream' α
⊢ (drop i s).tail = drop (i + 1) s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Option (α × β)
b : β
⊢ (corec f b).destruct = omap (corec f) (f b)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Option (α × β)
b : β
h : f b = none
⊢ corec f b = nil

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Option (α × β)
b : β
x : α
s : β
h : f b = some (x, s)
⊢ corec f b = cons x (corec f s)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : Stream' α
n : ℕ
⊢ (drop n a).head = a.get n

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
⊢ x = y

Tactic:
by

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

Goal state before:
pp: α : 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'
s s' : Seq α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ ↑s.tail = (↑s).tail

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
s t : Stream' α
h : x :: s = y :: t
n : ℕ
⊢ s.get n = t.get n

Tactic:
by

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

Goal state before:
pp: α : 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'
s s' : Seq α
r✝ : R s s'
this : s.head = s'.head ∧ R s.tail s'.tail
r : R s.tail s'.tail
⊢ ↑s'.tail = (↑s').tail

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
s : Stream' α
b : α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ a = b) ((b :: s).get n.succ)

Tactic:
by

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

Goal state before:
pp: α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n : ℕ
h : (fun b ↦ a = b) ((b :: s).get n)
⊢ a = b ∨ a ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Stream' α
a : α
⊢ a ∈ s → ∃ n, a = s.get n

Tactic:
by

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

Goal state before:
pp: α : 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'
s s' : Seq α
r : R s s'
⊢ (↑s).head = (↑s').head ∧ ∃ s_1 s'_1, ↑s_1 = (↑s).tail ∧ ↑s'_1 = (↑s').tail ∧ R s_1 s'_1

Tactic:
by

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

Goal state before:
pp: α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ s₁ = s₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Stream' α
⊢ map f s = f s.head :: map f s.tail

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
⊢ map f (a :: s) = f a :: map f s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b ↦ a = b) (s.get n)
⊢ (fun b ↦ f a = b) ((map f s).get n)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
c : Computation α
n : ℕ
a : α
h : Stream'.cons none c.val n = some a
⊢ Stream'.cons none c.val (n + 1) = some a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ zip f s₁ s₂ = f s₁.head s₂.head :: zip f s₁.tail s₂.tail

Tactic:
by

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₁ = nil ∧ s₂ = nil ∨ ∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂'
⊢ s₁ = s₂

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
⊢ const a = a :: const a

Tactic:
by

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

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

Goal state before:
pp: α : Type u
a : α
this : (a :: const a).tail = const a
⊢ (const a).tail = const a

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ (iterate f a).tail = iterate f (f a)

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ iterate f a = a :: iterate f (f a)

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u
s : Computation α
a : α
⊢ s.destruct = Sum.inl a → s = pure a

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (iterate id a) = fr (const a)
⊢ fr (iterate id a).tail = fr (const a).tail

Tactic:
by

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

Goal state before:
pp: α : Type u
f : α → α
a : α
⊢ iterate f (f a) = map f (iterate f a)

Tactic:
by

Goal state after: