mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) →
    ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj X_1 ⟶
      ((Pairwise.diagram ι).op ⋙ F.presheaf).obj X_1

Tactic:
rintro ((_ | _) | (_ | _))

Goal state after:
case refine_1.single.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.single { down := WalkingPair.left })) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left }))

case refine_1.single.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.single { down := WalkingPair.right })) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right }))

case refine_1.pair.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
a✝ : ULift.{w, 0} WalkingPair
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.pair { down := WalkingPair.left } a✝)) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.left } a✝))

case refine_1.pair.right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := fun j ↦ WalkingPair.casesOn j.down U V
hι : U ⊔ V = iSup ι
a✝ : ULift.{w, 0} WalkingPair
⊢ ((Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ).obj s.pt).obj
      (op (Pairwise.pair { down := WalkingPair.right } a✝)) ⟶
    ((Pairwise.diagram ι).op ⋙ F.presheaf).obj (op (Pairwise.pair { down := WalkingPair.right } a✝))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
n : ℕ
⊢ toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n)

Tactic:
induction n with
  | zero => ext; simp
  | succ n ihn =>
    rw [pow_succ, ihn, mul_def, toSpanSingleton_comp_toSpanSingleton, smul_eq_mul, pow_succ']

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
x : M
y : M₂
hf : f.IsInvertible
⊢ f.inverse y = x ↔ y = f x

Tactic:
rcases hf with ⟨M, rfl⟩
  simp only [inverse_equiv, ContinuousLinearEquiv.coe_coe]
  exact ContinuousLinearEquiv.symm_apply_eq M

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : ↑A = ↑e ∘SL f
this : f = ↑e.symm ∘SL ↑e ∘SL f
⊢ f.IsInvertible

Tactic:
rw [this, ← hA]

Goal state after:
case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : ↑A = ↑e ∘SL f
this : f = ↑e.symm ∘SL ↑e ∘SL f
⊢ (↑e.symm ∘SL ↑A).IsInvertible
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : ↑A = f ∘SL ↑e
this : f = (f ∘SL ↑e) ∘SL ↑e.symm
⊢ f.IsInvertible

Tactic:
rw [this, ← hA]

Goal state after:
case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : ↑A = f ∘SL ↑e
this : f = (f ∘SL ↑e) ∘SL ↑e.symm
⊢ (↑A ∘SL ↑e.symm).IsInvertible
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : IsEffective R S
t : R
hs :
  (algebraMap R S) t ∈
    (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inl).eqLocus
      (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inr)
⊢ ∃ a, (codRestrictEqLocusPushoutCocone R S) a = ⟨(algebraMap R S) t, hs⟩

Tactic:
exact ⟨t, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
c : Cone F
hc : IsLimit c
⊢ IsIso (c.π.app i₀)

Tactic:
by
  simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀,
    cone_π_app, coneπApp_eq_id, cone_pt, comp_id]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (leftToMax i₀ j) ≫ F.map γ =
    F.map (rightToMax i₀ j) ≫ F.map γ

Tactic:
isoMap_inv_hom_id_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ F.map γ = F.map (rightToMax i₀ j) ≫ F.map γ
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
s : Cocone F
j : J
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv ≫ F.map (leftToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j) =
    F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j)

Tactic:
isoMap_inv_hom_id_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
s : Cocone F
j : J
⊢ F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j) = F.map (rightToMax i₀ j) ≫ s.ι.app (IsFiltered.max i₀ j)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j

Tactic:
let β : j ⟶ i := IsFiltered.rightToMax _ _

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ F.map β ≫ (h.isoMap α ⋯).inv ≫ F.map α ≫ c.ι.app i = F.map β ≫ c.ι.app i

Tactic:
isoMap_inv_hom_id_assoc

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ F.map β ≫ c.ι.app i = F.map β ≫ c.ι.app i
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
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₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ i₂ (σ (ι₃ x)) ∈ g₁.range

Tactic:
← hg.linearMap_ker_eq,

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
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₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ i₂ (σ (ι₃ x)) ∈ g₂.ker
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
⊢ ExpChar R 1

Tactic:
have := f.charZero; exact .zero

Goal state after:
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
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ (lTensor A f).ker = (lTensor A f.ker.subtype).range

Tactic:
LinearMap.exact_iff.mp (lTensor_exact _ (LinearMap.exact_subtype_ker_map _) hf)

Goal state after:
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
inst✝² : Module.Flat R P
f : N →ₗ[R] P
hf : Function.Surjective ⇑f
A : Type u_6
inst✝¹ : AddCommGroup A
inst✝ : Module R A
⊢ (lTensor A f.ker.subtype).range = (lTensor A f.ker.subtype).range
Module: Mathlib.Algebra.CharP.LocalRing

Goal state before:
pp: case inl
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 = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
⊢ IsPrimePow q

Tactic:
have rn_dvd_q : r ^ n ∣ q := ⟨a, q_eq_a_mul_rn⟩

Goal state after:
case inl
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 = r ^ n * a
r_ne_dvd_a : ¬r ∣ q / r ^ q.factorization r
rn_dvd_q : r ^ n ∣ q
⊢ IsPrimePow q
Module: Mathlib.FieldTheory.IntermediateField.Basic

Goal state before:
pp: case neg
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
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : ⟨x, hx⟩ * y = 1
⊢ x⁻¹ ∈ S

Tactic:
rw [Subtype.ext_iff, S.coe_mul, S.coe_one, Subtype.coe_mk, mul_eq_one_iff_inv_eq₀ hx0] at hy

Goal state after:
case neg
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
hx0 : ¬x = 0
hS' : Field ↥S := hS.toField
y : ↥S
hy : x⁻¹ = ↑y
⊢ x⁻¹ ∈ S
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))
a b : ℚ
⊢ ↑(a * b).num /ₚ ↑(a * b).pnatDen = ↑a.num /ₚ ↑a.pnatDen * (↑b.num /ₚ ↑b.pnatDen)

Tactic:
simp only [← divp_assoc, divp_mul_eq_mul_divp, divp_divp_eq_divp_mul, divp_eq_iff_mul_eq,
        pnatCast_eq_natCast, Rat.coe_pnatDen, Units.val_mul]

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
this : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
a b : ℚ
⊢ ↑(a * b).num * (↑b.den * ↑a.den) = ↑a.num * ↑b.num * ↑(a * b).den
Module: Mathlib.Data.Seq.Defs

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

Tactic:
by
    rintro (n | _) h
    · contradiction
    · exact s.2 h

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

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

pp: case mpr
α : Type u
s : Seq α
⊢ s = nil → s.head = none

Tactic:
· apply head_eq_none

Goal state after:
case mpr
α : Type u
s : Seq α
⊢ s = nil → s.head = none
Module: Mathlib.Data.Seq.Defs

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

Tactic:
change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
f : β → Option (α × β)
b : β
o : Option β
⊢ (Corec.f f o).fst = none → (Corec.f f (Corec.f f o).snd).fst = none
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:
rcases n with - | n

Goal state after:
case zero
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
h : Stream'.cons none c.val 0 = some a
⊢ Stream'.cons none c.val (0 + 1) = some a

case succ
α : Type u
β : Type v
γ : Type w
c : Computation α
a : α
n : ℕ
h : Stream'.cons none c.val (n + 1) = some a
⊢ Stream'.cons none c.val (n + 1 + 1) = some a
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
a✝ : Option.map f none = none
⊢ Option.map f (s (n + 1)) = none

Tactic:
rw [al e]

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : s.IsSeq
n : ℕ
e : s n = none
a✝ : Option.map f none = none
⊢ Option.map f none = none
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (s (n + 1)) = some b

Tactic:
rw [al e]

Goal state after:
case some
α : Type u
β : Type v
γ : Type w
f : α → β
s : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a
n : ℕ
b : β
a : α
e : s n = some a
h : Option.rec none (fun val ↦ some (f val)) (some a) = some b
⊢ Option.rec none (fun val ↦ some (f val)) (some a) = some b
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
a : α
l : List α
h : l ≠ []
ainl : a ∈ l
⊢ a ∈ cycle l h

Tactic:
by
  rw [cycle_eq]; exact mem_append_stream_left _ ainl

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Preorder ι
G : ι → Type u_2
inst✝³ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝² : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
injective : ∀ (i : ι) (a : G i), (g i) a = 0 → a = 0
z : DirectLimit G f
hz : (lift G f P g Hg) z = 0
⊢ z = 0

Tactic:
induction z using DirectLimit.induction_on with

Goal state after:
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
h : fract v ≠ 0
⊢ (IntFractPair.stream v 1).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b }) = some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }

Tactic:
stream_succ_of_some (stream_zero v) h,

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
h : fract v ≠ 0
⊢ (some (IntFractPair.of (IntFractPair.of v).fr⁻¹)).bind (some ∘ fun p ↦ { a := 1, b := ↑p.b }) =
    some { a := 1, b := ↑⌊(fract v)⁻¹⌋ }
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of v).TerminatedAt (n + 1)

Tactic:
of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none,

Goal state after:
case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ IntFractPair.stream v (n + 1 + 1) = none
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
x : α
s : Seq α
n : ℕ
h_not_terminated : ¬s.TerminatedAt n
⊢ (s.set n x).get? n = some x

Tactic:
simpa [set, update, ← Option.ne_none_iff_exists'] using! h_not_terminated

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
⊢ (Ring.DirectLimit.of G f i) (x * x⁻¹) = 1

Tactic:
mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
i : ι
x : G i
H : (Ring.DirectLimit.of G f i) x ≠ 0
⊢ (Ring.DirectLimit.of G f i) 1 = 1
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case some.zero
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)

Tactic:
obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq

Goal state after:
case some.zero
K : Type u_1
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (0 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (0 + 2) = convs'Aux (squashSeq s 0) (0 + 1)
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
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = of v

Tactic:
rcases gcf_v_eq : of v with ⟨h, s⟩

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
inst✝ : IsStrictOrderedRing K
v : K
q : ℚ
v_eq_q : v = ↑q
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of v = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝⁶ : Field K
inst✝⁵ : LinearOrder K
inst✝⁴ : IsStrictOrderedRing K
inst✝³ : FloorRing K
inst✝² : Archimedean K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
⊢ Filter.Tendsto (of v).convs Filter.atTop (𝓝 v)

Tactic:
by
  simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v

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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ 1 ≤ ifp_succ_n.b

Tactic:
obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
        ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ 1 ≤ (IntFractPair.of ifp_n.fr⁻¹).b