mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y : M
⊢ { toFun := fun a ↦ ⟨(x + y) ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun a ↦ ⟨x ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun a ↦ ⟨y ⊗ₜ[R] ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp [add_tmul]

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

Goal state before:
pp: case zero
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 : N →ₗ[R] P
⊢ ↑((tensorKer S M f) 0) = (lTensor M f.ker.subtype) 0

pp: case tmul
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 : N →ₗ[R] P
x✝ : M
y✝ : ↥f.ker
⊢ ↑((tensorKer S M f) (x✝ ⊗ₜ[R] y✝)) = (lTensor M f.ker.subtype) (x✝ ⊗ₜ[R] y✝)

pp: case add
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 : N →ₗ[R] P
x✝ y✝ : M ⊗[R] ↥f.ker
a✝¹ : ↑((tensorKer S M f) x✝) = (lTensor M f.ker.subtype) x✝
a✝ : ↑((tensorKer S M f) y✝) = (lTensor M f.ker.subtype) y✝
⊢ ↑((tensorKer S M f) (x✝ + y✝)) = (lTensor M f.ker.subtype) (x✝ + y✝)

Tactic:
<;>

Goal state after:
case zero
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 : N →ₗ[R] P
⊢ ↑((tensorKer S M f) 0) = (lTensor M f.ker.subtype) 0

case tmul
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 : N →ₗ[R] P
x✝ : M
y✝ : ↥f.ker
⊢ ↑((tensorKer S M f) (x✝ ⊗ₜ[R] y✝)) = (lTensor M f.ker.subtype) (x✝ ⊗ₜ[R] y✝)

case add
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 : N →ₗ[R] P
x✝ y✝ : M ⊗[R] ↥f.ker
a✝¹ : ↑((tensorKer S M f) x✝) = (lTensor M f.ker.subtype) x✝
a✝ : ↑((tensorKer S M f) y✝) = (lTensor M f.ker.subtype) y✝
⊢ ↑((tensorKer S M f) (x✝ + y✝)) = (lTensor M f.ker.subtype) (x✝ + y✝)
Module: Mathlib.RingTheory.Flat.Equalizer

Goal state before:
pp: case zero
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
⊢ ↑((tensorEqLocus S M f g) 0) = (lTensor M (f.eqLocus g).subtype) 0

pp: case tmul
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
x✝ : M
y✝ : ↥(f.eqLocus g)
⊢ ↑((tensorEqLocus S M f g) (x✝ ⊗ₜ[R] y✝)) = (lTensor M (f.eqLocus g).subtype) (x✝ ⊗ₜ[R] y✝)

pp: case add
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
x✝ y✝ : M ⊗[R] ↥(f.eqLocus g)
a✝¹ : ↑((tensorEqLocus S M f g) x✝) = (lTensor M (f.eqLocus g).subtype) x✝
a✝ : ↑((tensorEqLocus S M f g) y✝) = (lTensor M (f.eqLocus g).subtype) y✝
⊢ ↑((tensorEqLocus S M f g) (x✝ + y✝)) = (lTensor M (f.eqLocus g).subtype) (x✝ + y✝)

Tactic:
<;>

Goal state after:
case zero
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
⊢ ↑((tensorEqLocus S M f g) 0) = (lTensor M (f.eqLocus g).subtype) 0

case tmul
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
x✝ : M
y✝ : ↥(f.eqLocus g)
⊢ ↑((tensorEqLocus S M f g) (x✝ ⊗ₜ[R] y✝)) = (lTensor M (f.eqLocus g).subtype) (x✝ ⊗ₜ[R] y✝)

case add
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
x✝ y✝ : M ⊗[R] ↥(f.eqLocus g)
a✝¹ : ↑((tensorEqLocus S M f g) x✝) = (lTensor M (f.eqLocus g).subtype) x✝
a✝ : ↑((tensorEqLocus S M f g) y✝) = (lTensor M (f.eqLocus g).subtype) y✝
⊢ ↑((tensorEqLocus S M f g) (x✝ + y✝)) = (lTensor M (f.eqLocus g).subtype) (x✝ + y✝)
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h₀
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

pp: case h₁
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

Tactic:
<;>

Goal state after:
case h₀
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inl X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right

case h₁
T : Type u_1
inst✝⁴ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝³ : Q.IsMultiplicative
X Y Z : T
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.IsStableUnderCobaseChange
X✝ Y✝ Z✝ : P.Under Q X
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc ((x✝¹ ≫ x✝).right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right =
    pushout.inr X✝.hom f ≫
      (Under.homMk (pushout.desc (x✝¹.right ≫ pushout.inl Y✝.hom f) (pushout.inr Y✝.hom f) ⋯) ⋯ ⋯ ≫
          Under.homMk (pushout.desc (x✝.right ≫ pushout.inl Z✝.hom f) (pushout.inr Z✝.hom f) ⋯) ⋯ ⋯).right
Module: Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Goal state before:
pp: case h₀
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inl ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inl ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

pp: case h₁
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inr ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inr ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

Tactic:
<;>

Goal state after:
case h₀
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inl ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inl ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right

case h₁
T : Type u_1
inst✝⁶ : Category.{v_1, u_1} T
P Q : MorphismProperty T
inst✝⁵ : Q.IsMultiplicative
X Y Z : T
inst✝⁴ : P.IsStableUnderComposition
inst✝³ : Q.IsStableUnderCobaseChange
f : X ⟶ Y
inst✝² : P.HasPushoutsAlong f
inst✝¹ : P.IsStableUnderCobaseChangeAlong f
inst✝ : Q.HasOfPrecompProperty Q
hPf : P f
hQf : Q f
A B : P.Under Q Y
g : A ⟶ B
⊢ pushout.inr ((map Q hPf).obj A).hom f ≫
      ((map Q hPf ⋙ pushout P Q f).map g ≫
          Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj B).right)) B.hom ⋯) ⋯ ⋯).right =
    pushout.inr ((map Q hPf).obj A).hom f ≫
      (Under.homMk (pushout.desc (𝟙 ((𝟭 T).obj ((map Q hPf).obj A).right)) A.hom ⋯) ⋯ ⋯ ≫ (𝟭 (P.Under Q Y)).map g).right
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
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
x✝ : L
⊢ x✝ ∈ a₁✝ ↔ x✝ ∈ a₂✝

Tactic:
← mem_toSubalgebra,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubalgebra = a₂✝.toSubalgebra
x✝ : L
⊢ x✝ ∈ a₁✝.toSubalgebra ↔ x✝ ∈ a₂✝.toSubalgebra
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:
change ((PNat.isUnit_natCast (R := R) 1).unit : R) = 1

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
⊢ ↑⋯.unit = 1
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case intro
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 : ℕ
p_charP : CharP R p
⊢ P

Tactic:
by_cases h : p = 0
    · rw [h] at p_charP
      have h0 : CharZero R := CharP.charP_to_charZero R
      exact split_equalCharZero_mixedCharZero R h_equal h_mixed
    · exact h_pos p h p_charP

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

Goal state before:
pp: case none
α : Type u
s : Seq α
⊢ none = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> none

pp: case some
α : Type u
s : Seq α
val✝ : α
⊢ some val✝ = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> some val✝

Tactic:
<;>

Goal state after:
case none
α : Type u
s : Seq α
⊢ none = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> none

case some
α : Type u
s : Seq α
val✝ : α
⊢ some val✝ = Prod.fst <$> (fun a' ↦ (a', s.tail)) <$> some val✝
Module: Mathlib.Data.Seq.Defs

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

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

Tactic:
<;>

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

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

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

pp: case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
⊢ (fun a' ↦ (a', s.tail)) <$> some a' = some (a, s') → s = cons a s'

Tactic:
<;>

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

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

Goal state before:
pp: case zero
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = (cons x s.tail).get? 0

pp: case succ
α : Type u
s : Seq α
x : α
h : s.head = some x
n✝ : ℕ
⊢ s.get? (n✝ + 1) = (cons x s.tail).get? (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
s : Seq α
x : α
h : s.head = some x
⊢ s.get? 0 = (cons x s.tail).get? 0

case succ
α : Type u
s : Seq α
x : α
h : s.head = some x
n✝ : ℕ
⊢ s.get? (n✝ + 1) = (cons x s.tail).get? (n✝ + 1)
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
  ext1 n
  cases n <;> simp only [get?_cons_zero, get?_cons_succ, get?_tail]
  exact h

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

Goal state before:
pp: case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ (Corec.f f none).fst = none → (Corec.f f (Corec.f f none).snd).fst = none

pp: case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
⊢ (Corec.f f (some b)).fst = none → (Corec.f f (Corec.f f (some b)).snd).fst = none

Tactic:
<;>

Goal state after:
case zero.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
⊢ (Corec.f f none).fst = none → (Corec.f f (Corec.f f none).snd).fst = none

case zero.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
⊢ (Corec.f f (some b)).fst = none → (Corec.f f (Corec.f f (some b)).snd).fst = none
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
⊢ (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
      none →
    (match
          (match none with
            | none => (none, none)
            | some (a, b') => (some a, some b')).snd with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).fst =
      none

pp: case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
⊢ (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
      none →
    (match
          (match some s with
            | none => (none, none)
            | some (a, b') => (some a, some b')).snd with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).fst =
      none

Tactic:
<;>

Goal state after:
case zero.some.none
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
h₁ : f b = none
⊢ (match none with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
      none →
    (match
          (match none with
            | none => (none, none)
            | some (a, b') => (some a, some b')).snd with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).fst =
      none

case zero.some.some
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b✝ b : β
s : α × β
h₁ : f b = some s
⊢ (match some s with
        | none => (none, none)
        | some (a, b') => (some a, some b')).fst =
      none →
    (match
          (match some s with
            | none => (none, none)
            | some (a, b') => (some a, some b')).snd with
        | none => (none, none)
        | some b =>
          match f b with
          | none => (none, none)
          | some (a, b') => (some a, some b')).fst =
      none
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
s : Stream' α
⊢ (s.head :: s.tail) 0 = s 0

pp: case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ (s.head :: s.tail) (n✝ + 1) = s (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
s : Stream' α
⊢ (s.head :: s.tail) 0 = s 0

case succ
α : Type u
s : Stream' α
n✝ : ℕ
⊢ (s.head :: s.tail) (n✝ + 1) = s (n✝ + 1)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case nil
α : 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' : Seq α
⊢ R nil s' → BisimO R nil.destruct s'.destruct → nil.head = s'.head ∧ R nil.tail s'.tail

pp: case 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'
s' : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝ s✝) s' →
    BisimO R (cons x✝ s✝).destruct s'.destruct → (cons x✝ s✝).head = s'.head ∧ R (cons x✝ s✝).tail s'.tail

Tactic:
<;>

Goal state after:
case nil
α : 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' : Seq α
⊢ R nil s' → BisimO R nil.destruct s'.destruct → nil.head = s'.head ∧ R nil.tail s'.tail

case 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'
s' : Seq α
x✝ : α
s✝ : Seq α
⊢ R (cons x✝ s✝) s' →
    BisimO R (cons x✝ s✝).destruct s'.destruct → (cons x✝ s✝).head = s'.head ∧ R (cons x✝ s✝).tail s'.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: case zero
α : Type u
a : α
⊢ (const a).get 0 = (a :: const a).get 0

pp: case succ
α : Type u
a : α
n✝ : ℕ
⊢ (const a).get (n✝ + 1) = (a :: const a).get (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
⊢ (const a).get 0 = (a :: const a).get 0

case succ
α : Type u
a : α
n✝ : ℕ
⊢ (const a).get (n✝ + 1) = (a :: const a).get (n✝ + 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
⊢ (match none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a

pp: case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
⊢ (match some val✝ with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a

Tactic:
<;>

Goal state after:
case none
α : Type u
s : Computation α
a : α
f0 : s.val 0 = none
⊢ (match none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a

case some
α : Type u
s : Computation α
a val✝ : α
f0 : s.val 0 = some val✝
⊢ (match some val✝ with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
⊢ (match none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

pp: case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
⊢ (match some a' with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

Tactic:
<;>

Goal state after:
case none
α : Type u
s s' : Computation α
f0 : s.val 0 = none
⊢ (match none with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

case some
α : Type u
s s' : Computation α
a' : α
f0 : s.val 0 = some a'
⊢ (match some a' with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case inl.nil
α : 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₂
⊢ nil = nil ∧ nil = nil ∨ ∃ x s₁' s₂', nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

pp: case inl.cons
α : 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₂
x✝ : α
s✝ : Seq α
⊢ cons x✝ s✝ = nil ∧ cons x✝ s✝ = nil ∨
    ∃ x s₁' s₂', cons x✝ s✝ = cons x s₁' ∧ cons x✝ s✝ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

Tactic:
<;>

Goal state after:
case inl.nil
α : 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₂
⊢ nil = nil ∧ nil = nil ∨ ∃ x s₁' s₂', nil = cons x s₁' ∧ nil = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')

case inl.cons
α : 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₂
x✝ : α
s✝ : Seq α
⊢ cons x✝ s✝ = nil ∧ cons x✝ s✝ = nil ∨
    ∃ x s₁' s₂', cons x✝ s✝ = cons x s₁' ∧ cons x✝ s✝ = cons x s₂' ∧ (s₁' = s₂' ∨ motive s₁' s₂')