mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
⊢ τB' = moduleTopology S B'

Tactic:
by
    -- get these in before I start putting new topologies on A and B and have to use `@`
    let g : A →ₛₗ[σ] B' := e
    let g' : B' →ₛₗ[σ'] A := e.symm
    let h : A →+ B' := e
    let h' : B' →+ A := e.symm
    simp_rw [e.toHomeomorph.symm.isInducing.1, eq_moduleTopology R A, moduleTopology, induced_sInf]
    apply congr_arg
    ext τ -- from this point on the definitions of `g`, `g'` etc. above don't work without `@`.
    rw [Set.mem_image]
    constructor
    · rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩
      exact ⟨continuousSMul_inducedₛₗ g' hσ', continuousAdd_induced h'⟩
    · rintro ⟨h1, h2⟩
      use τ.induced e
      rw [induced_compose]
      refine ⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩
      nth_rw 2 [← induced_id (t := τ)]
      simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousSMul S B'

pp: case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousAdd B'

Tactic:
· -- In this branch, we prove that `• : S × B → B` is continuous for the coinduced topology.
      apply ContinuousSMul.mk
      -- We know that `• : R × A → A` is continuous, by assumption.
      obtain ⟨hA⟩ : ContinuousSMul R A := inferInstance
      /- By linearity of φ, this diagram commutes:
        R × A --(•)--> A
          |            |
          |σ × φ      |φ
          |            |
         \/            \/
        S × B --(•)--> B
      -/
      have hφ2 : (fun p ↦ p.1 • p.2 : S × B' → B') ∘ (Prod.map σ φ) =
        φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) := by ext; simp
      -- Furthermore, `σ` is an open quotient map as is `φ`,
      -- so the product `σ × φ` is an open quotient map, by a result in the library.
      have hoq : IsOpenQuotientMap (_ : R × A → S × B') := IsOpenQuotientMap.prodMap hσ hφo
      -- This is the left map in the diagram. So by a standard fact about open quotient maps,
      -- to prove that the bottom map is continuous, it suffices to prove
      -- that the diagonal map is continuous.
      rw [← hoq.continuous_comp_iff]
      -- but the diagonal is the composite of the continuous maps `φ` and `• : R × A → A`
      rw [hφ2]
      -- so we're done
      exact Continuous.comp hφo.continuous hA

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousAdd B'
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁷ : Semiring R₁
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁴ : TopologicalSpace M₁
inst✝¹³ : AddCommMonoid M₁
M'₁ : Type u_5
inst✝¹² : TopologicalSpace M'₁
inst✝¹¹ : AddCommMonoid M'₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : AddCommMonoid M₃
M₄ : Type u_8
inst✝⁶ : TopologicalSpace M₄
inst✝⁵ : AddCommMonoid M₄
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₁ M'₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
T : (M₁ →L[R₁] M₁)ˣ
x : M₁
⊢ ↑T⁻¹ (↑T x) = x

Tactic:
rw [← mul_apply_eq_comp, Units.inv_mul, one_apply_eq_self]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
s : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (cokerπ φ) ⋯) ≫ m = Cofork.π s
⊢ m =
    ofHom
      (let __LinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯;
      { toLinearMap := __LinearMap, cont := ⋯ })

Tactic:
by dsimp at h ⊢; rw [← cancel_epi (cokerπ φ), h]; rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
a : WithOne α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a

Tactic:
by simp_rw [inv_comp_inv, Option.map_id, id]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.mul_2
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝¹ y✝ x y y' : Prequotient F
x✝ : Relation F y y'
h : descFunLift F s y = descFunLift F s y'
⊢ descFunLift F s (x.mul y) = descFunLift F s (x.mul y')

Tactic:
| mul_2 x y y' _ h =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.snd a ≫ eqToHom ⋯) = ?m.560

Tactic:
subst h₂; simp only [eqToHom_refl, f]

Goal state after:
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₁ : J.fst a = J.snd a
f : (left a ⟶ right (J.snd a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ R, Q R ∧ ∃ f, (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (R : Subtype Q') × FGAlgCatSkeleton ↑↑R → CommRingCat := fun S ↦ of ↑(FGAlgCatSkeleton.eval (↑↑S.fst) S.snd).obj
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
T : FGAlgCatSkeleton ↑R
e : ↑(FGAlgCatSkeleton.eval (↑R) T).obj ≃+* ↑S
he : Hom.hom φ = e.toRingHom.comp (algebraMap ↑R ↑(FGAlgCatSkeleton.eval (↑R) T).obj)
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
exact ⟨_, ⟨⟨_, hR'⟩, T⟩, ⟨RingEquiv.toCommRingCatIso e.symm⟩⟩

Goal state after:
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R M₁
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₃ : K₃ →ₗ[R] M₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
x : K₃
y₁ : M₂
hy₁ : f₂ y₁ = ι₃ x
z₁ : N₁
y₂ : M₂
hy₂ : f₂ y₂ = ι₃ x
z₂ : N₁
hz₂ : g₁ z₂ = i₂ y₂
d : M₁
hz₁ : z₁ - z₂ = i₁ d
hd : f₁ d = y₁ - y₂
⊢ i₁ d ∈ Set.range ⇑i₁

Tactic:
exact ⟨_, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
⊢ (MorphismProperty.costructuredArrowObj L P).colimitsOfShape J Y ≤ MorphismProperty.costructuredArrowObj L P Y

Tactic:
intro ⟨d⟩

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesColimitsOfShape J L
inst✝ : HasColimitsOfShape J A
c : (D : J ⥤ T) → [HasColimit D] → Cocone D
hc : (D : J ⥤ T) → [inst : HasColimit D] → IsColimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasColimit D] {X : T} (s : D ⟶ (Functor.const J).obj X),
    (∀ (j : J), P (s.app j)) → P ((hc D).desc { pt := X, ι := s })
X : T
Y : CostructuredArrow L X
d : (MorphismProperty.costructuredArrowObj L P).ColimitOfShape J Y
⊢ MorphismProperty.costructuredArrowObj L P Y
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
⊢ (MorphismProperty.structuredArrowObj L P).limitsOfShape J Y ≤ MorphismProperty.structuredArrowObj L P Y

Tactic:
intro ⟨d⟩

Goal state after:
T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
J : Type u_3
inst✝³ : Category.{v_3, u_3} J
P : MorphismProperty T
inst✝² : P.RespectsIso
inst✝¹ : PreservesLimitsOfShape J L
inst✝ : HasLimitsOfShape J A
c : (D : J ⥤ T) → [HasLimit D] → Cone D
hc : (D : J ⥤ T) → [inst : HasLimit D] → IsLimit (c D)
H :
  ∀ (D : J ⥤ T) [inst : HasLimit D] {X : T} (s : (Functor.const J).obj X ⟶ D),
    (∀ (j : J), P (s.app j)) → P ((hc D).lift { pt := X, π := s })
X : T
Y : StructuredArrow X L
d : (MorphismProperty.structuredArrowObj L P).LimitOfShape J Y
⊢ MorphismProperty.structuredArrowObj L P Y
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P : MorphismProperty T
X : T
inst✝ : P.ContainsIdentities
Y : P.Under ⊤ X
a : Under.mk ⊤ (𝟙 X) ⋯ ⟶ Y
⊢ a = Under.homMk Y.hom ⋯ ⋯

Tactic:
ext; simp [← Under.w a]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑a * ↑p + ↑b * ↑(ringChar R) = 1
⊢ IsUnit ↑p

Tactic:
rw [hch, mul_zero, add_zero, mul_comm] at hab

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h : ¬p ∣ ringChar R
a b : ℤ
hab : ↑p * ↑a = 1
⊢ IsUnit ↑p
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 : N →ₗ[R] P
inst✝ : Flat R M
⊢ ((AlgebraTensorModule.lTensor S M) f).ker = ((AlgebraTensorModule.lTensor S M) f.ker.subtype).range

Tactic:
rw [← LinearMap.exact_iff]
  exact Module.Flat.lTensor_exact M (LinearMap.exact_subtype_ker_map f)

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPe : HasEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
hPse : HasStableEqualizers fun {R S} [CommRing R] [CommRing S] ↦ P
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
⊢ PreservesLimitsOfShape WalkingParallelPair
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P) ⊤ f)

Tactic:
by
  refine ⟨fun {K} ↦ ?_⟩
  have := hPe.createsLimitsWalkingParallelPair hPi R
  algebraize [f.hom]
  have : PreservesLimit (K ⋙ Under.forget (toMorphismProperty P) ⊤ R)
      (CategoryTheory.Under.pushout f) := by
    rw [← CommRingCat.ofHom_hom f,
      ← preservesLimit_iff_of_natIso _ (CommRingCat.tensorProdIsoPushout R S),
      ← preservesLimit_iff_of_iso_diagram _ (diagramIsoParallelPair _).symm]
    exact hPse.preservesLimit_parallelPair_tensorProd _ _ ((K.obj _).prop) ((K.obj _).prop)
  have : PreservesLimit K (Under.pushout (toMorphismProperty P) ⊤ f ⋙
        Under.forget (toMorphismProperty P) ⊤ S) := by
    rw [preservesLimit_iff_of_natIso _ (Under.pushoutCompForgetIso _)]
    infer_instance
  exact preservesLimit_of_reflects_of_preserves _ (Under.forget _ ⊤ S)

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:
← map_natCast' _ he,

Goal state after:
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 : e ↑n = ↑m
⊢ n = m
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 : e ↑n = ↑m
⊢ n = m

Tactic:
← map_natCast' _ he,

Goal state after:
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 : e ↑n = e ↑m
⊢ n = m
Module: Mathlib.Data.Seq.Defs

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

Tactic:
intro h
  simpa using congrArg (·.get? 0) h

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:
rw [← Stream'.eta (zip f s₁ s₂)]

Goal state after:
α : Type u
β : Type v
δ : Type w
f : α → β → δ
s₁ : Stream' α
s₂ : Stream' β
⊢ (zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
⊢ IsSeq (Function.update (↑s) n (Option.map f (↑s n)))

Tactic:
by
    have (i : ℕ) : Function.update s.val n ((s.get? n).map f) i = none ↔ s.get? i = none := by
      by_cases hi : i = n <;> simp [Function.update, hi]
    simp only [IsSeq, val_eq_get, this]
    exact @s.prop

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

Goal state before:
pp: α : Type u
x : List α
a b : Stream' α
h : x ++ₛ a = x ++ₛ b
⊢ a = b

Tactic:
ext n; replace h := congr_arg (fun a ↦ a.get (x.length + n)) h; simpa using h

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
s : Computation α
inst✝ : s.Terminates
⊢ (s.bind (pure ∘ f)).Terminates

Tactic:
exact terminates_of_mem (mem_bind (get_mem s) (get_mem (α := β) (f (get s))))

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a' b

Tactic:
rw [mem_unique ma' ma]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
a' : α
ma' : a' ∈ ca
⊢ ∃ b, b ∈ cb ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b'

Tactic:
mem_unique mb' mb

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b'

Tactic:
mem_unique mb' mb

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
a : α
cb : Computation β
x✝ : ∃ b, b ∈ cb ∧ R a b
b : β
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ R a b
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ (s.drop k).get? (m + 1) = s.get? (k + 1 + m)

Tactic:
convert! ih using 2

Goal state after:
case e'_3
α : Type u
s : Seq α
k : ℕ
ih : ∀ {m : ℕ}, (s.drop k).get? m = s.get? (k + m)
m : ℕ
⊢ k + 1 + m = k + (m + 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
f : α → α
s : Seq α
n m : ℕ
⊢ (s.update n f).get? m = if m = n then Option.map f (s.get? m) else s.get? m

Tactic:
by
  simp [update, Function.update]
  split_ifs with h_if
  · simp [h_if]
  · rfl

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

Goal state before:
pp: case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

Tactic:
have s_nth_eq : g.s.get? n = some ⟨1, (⌊ifp_n.fr⁻¹⌋ : K)⟩ :=
        get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero nth_stream_eq ifp_n_fract_ne_zero

Goal state after:
case succ.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
⊢ compExactValue ppconts pconts ifp_n.fr = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
hy : y ∈ s.get? j
k : ℕ
hj : j = i + k + 1
⊢ R x y

Tactic:
rw [hj, ← head_dropn, Nat.add_assoc, dropn_add, head_dropn] at hy

Goal state after:
α : Type u
R : α → α → Prop
s : Seq α
motive : Seq α → Prop
base : motive s
step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl
i j : ℕ
h_ij : i < j
x : α
hx : x ∈ (s.drop i).head
y : α
k : ℕ
hy : y ∈ (s.drop i).get? (k + 1)
hj : j = i + k + 1
⊢ R x y
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
⊢ compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)

Tactic:
grind [compExactValue, nextConts, nextNum, nextDen]

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
⊢ Stream'.Seq.map (Pair.map Rat.cast) (of q).s = (of v).s

Tactic:
by
  ext n; rw [← coe_of_s_get?_rat_eq v_eq_q]; rfl

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✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b✝ : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b✝, fr := ifp_n_fr }
this✝¹ : ↑⌊{ b := b✝, fr := ifp_n_fr }.fr⁻¹⌋ ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹
this✝ : ifp_n_fr ≠ 0
this : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n
⊢ ↑ifp_succ_n.b ≤ { b := b✝, fr := ifp_n_fr }.fr⁻¹

Tactic:
rwa [← this]

Goal state after: