mathlib-initiative/mathlib-tactics huggingface dataset:
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_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (g₁ + g₂) ∘SL f = g₁ ∘SL f + g₂ ∘SL f

Tactic:
by
  ext
  simp

Goal state after:
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_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
⊢ g ∘SL ∑ i ∈ s, f i = ∑ i ∈ s, g ∘SL f i

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
inst✝¹² : Semiring R₁
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₁ M₁
inst✝⁶ : Module R₁ M₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₃
inst✝¹ : TopologicalSpace M₃
inst✝ : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
⊢ f.smulRight x ∘SL g.smulRight y = g.smulRight (f y • x)

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (-g) ∘SL f = -g ∘SL f

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
⊢ g ∘SL (f₁ - f₂) = g ∘SL f₁ - g ∘SL f₂

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (g₁ - g₂) ∘SL f = g₁ ∘SL f - g₂ ∘SL f

Tactic:
by
  ext
  simp

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
s : Cocone F
j : J
⊢ h.cocone.ι.app j ≫ s.ι.app i₀ = s.ι.app j

Tactic:
by
    dsimp [coconeιApp]
    rw [← s.w (IsFiltered.rightToMax i₀ j), ← s.w (IsFiltered.leftToMax i₀ j), assoc,
      isoMap_inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
have := IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
this : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
⊢ PreservesColimitsOfShape J F
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
D : J ⥤ C
inst✝¹ : IsCofiltered J
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
i j : J
f : D.obj i ⟶ X
g : D.obj j ⟶ X
h : c.π.app i ≫ f = c.π.app j ≫ g
⊢ ∃ k u v, D.map u ≫ f = D.map v ≫ g

Tactic:
obtain ⟨k, u, v, huv⟩ :=
    (Types.FilteredColimit.isColimit_eq_iff _ (isColimitOfPreserves (yoneda.obj X) hc.op)).mp h
  exact ⟨k.unop, u.unop, v.unop, huv⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ Function.Surjective ⇑(ConcreteCategory.hom fBC)

Tactic:
← RingHom.range_eq_top,

Goal state after:
R A B C : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : IsTopologicalRing ↑R
φ : A ⟶ B
ψ : A ⟶ C
PB : CommRingCat := of (MvPolynomial ↑B ↑A)
PC : CommRingCat := of (MvPolynomial ↑C ↑A)
fB : PB ⟶ B := ofHom (MvPolynomial.eval₂Hom (Hom.hom φ) id)
hfB : Function.Surjective ⇑(Hom.hom fB)
fC : PC ⟶ C := ofHom (MvPolynomial.eval₂Hom (Hom.hom ψ) id)
hfC : Function.Surjective ⇑(Hom.hom fC)
this : IsEmbedding (Prod.map (fun x ↦ fB ≫ x) fun x ↦ fC ≫ x)
PBC : CommRingCat := of (MvPolynomial (↑B ⊕ ↑C) ↑A)
fBC : PBC ⟶ pushout φ ψ :=
  ofHom
    (MvPolynomial.eval₂Hom (Hom.hom (φ ≫ pushout.inl φ ψ))
      (Sum.elim ⇑(Hom.hom (pushout.inl φ ψ)) ⇑(Hom.hom (pushout.inr φ ψ))))
⊢ (ConcreteCategory.hom fBC).range = ⊤
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
N₃ : Type u_7
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₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[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₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : N₁
H : G (π₁ x) = 0
y : M₂
hy : i₂ y = g₁ x
⊢ i₃ (f₂ y) = 0

Tactic:
rw [← i₃.comp_apply, ← h₂,
      g₂.comp_apply, hy, hg.apply_apply_eq_zero]

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

Goal state before:
pp: R : CommRingCat
A B : Under R
f g : A ⟶ B
⊢ ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ f = ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ g

Tactic:
ext (a : AlgHom.equalizer (toAlgHom f) (toAlgHom g))

Goal state after:
R : CommRingCat
A B : Under R
f g : A ⟶ B
a : ↥((toAlgHom f).equalizer (toAlgHom g))
⊢ (ConcreteCategory.hom (Under.Hom.right (((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ f))) a =
    (ConcreteCategory.hom (Under.Hom.right (((toAlgHom f).equalizer (toAlgHom g)).val.toUnder ≫ g))) a
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c₁ c₂ : BinaryFan (Over.mk f) (Over.mk g)
a : c₁ ⟶ c₂
⊢ ∀ (j : WalkingCospan),
    Over.Hom.left a.hom ≫ (PullbackCone.mk (Over.Hom.left c₂.fst) (Over.Hom.left c₂.snd) ⋯).π.app j =
      (PullbackCone.mk (Over.Hom.left c₁.fst) (Over.Hom.left c₁.snd) ⋯).π.app j

Tactic:
by rintro (_ | _ | _) <;> simp [← Over.comp_left_assoc, ← Over.comp_left]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ m = Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯

Tactic:
by
    ext1
    refine PushoutCocone.IsColimit.hom_ext hc ?_ ?_
    · simpa using! congr(($e₁).right)
    · simpa using! congr(($e₂).right)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over B
s : Cone F
m : s.pt ⟶ { pt := mk (𝟙 B), π := { app := fun p ↦ p.as.elim, naturality := ⋯ } }.pt
x✝ :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ { pt := mk (𝟙 B), π := { app := fun p ↦ p.as.elim, naturality := ⋯ } }.π.app j = s.π.app j
⊢ m = homMk s.pt.hom ⋯

Tactic:
by ext; simpa using m.w

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

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

Tactic:
by
  cases ‹ExpChar A p› with
  | zero => have := f.charZero; exact .zero
  | prime hp => have := f.charP H p; exact .prime hp

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

Goal state before:
pp: 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✝¹ : P.IsMultiplicative
inst✝ : Q.RespectsIso
X : T
f : optParam (X ⟶ X) (𝟙 X)
hf : autoParam (f = 𝟙 X) mapId._auto_1
⊢ P f

Tactic:
subst hf; exact P.id_mem X

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

Goal state before:
pp: α : Type u
s : Stream' α
⊢ zip appendStream' s.inits s.tails = const s

Tactic:
by
  ext
  simp

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

Goal state before:
pp: case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈ take n s

Tactic:
rw [← hl, take, head_eq_some h_get]

Goal state after:
case zero
α : Type u
x : α
s : Seq α
n : ℕ
h_mn : 0 < n
h_get : s.get? 0 = some x
l : ℕ
hl : l + 1 = n
⊢ x ∈
    match (cons x s.tail).destruct with
    | none => []
    | some (x, r) => x :: take l r
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
n : ℕ
⊢ (s.toList h)[n]? = s.get? n

Tactic:
by
  ext k
  simp only [toList, getElem?_take, Nat.lt_find_iff, length,
    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt]
  intro h m hmn
  let ⟨a, ha⟩ := ge_stable s hmn h
  simp [ha]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n : ℕ
⊢ g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
by
  rcases em <| TerminatedAt g n with terminatedAt_n | not_terminatedAt_n
  · rw [dens_stable_of_terminated n.le_succ terminatedAt_n,
      nums_stable_of_terminated n.le_succ terminatedAt_n, Finset.prod_range_succ,
      partNum_none_iff_s_none.mpr terminatedAt_n]
    grind
  · exact determinant_aux <| Or.inr <| not_terminatedAt_n

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
inst✝ : IsStrictOrderedRing K
a : ℤ
⊢ ∀ (n : ℕ), (of ↑a).s.get? n = none

Tactic:
by
    intro n
    induction n with
    | zero => rw [of_s_head_aux, stream_succ_of_int, Option.bind]
    | succ n ih => exact (of (a : K)).s.prop ih

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:

Tactic:
n ≤ fib n := IH
      _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: m n k : ℕ
⊢ (fib m).gcd (fib (n + k * m + m)) = (fib m).gcd (fib (n + k * m))

Tactic:
gcd_fib_add_self _ _

Goal state after:
m n k : ℕ
⊢ (fib m).gcd (fib (n + k * m)) = (fib m).gcd (fib (n + k * m))
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: case succ.succ.none
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ ∃ conts, (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
use pred_conts

Goal state after:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
g : GenContFract K := ⋯
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast pred_conts
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
this : g.convs (n + 1) = g'.convs' n
⊢ g.convs (n + 1) = g.convs' (n + 1)

Tactic:
rwa [succ_nth_conv'_eq_squashGCF_nth_conv']

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.b = φ P.a * -(x + y + z)

Tactic:
injection eq_sum_three_roots ha h3

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.c = φ P.a * (x * y + x * z + y * z)

Tactic:
injection eq_sum_three_roots ha h3

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.d = φ P.a * -(x * y * z)

Tactic:
injection eq_sum_three_roots ha h3

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Prod

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
hM : Module.Finite R M
hN : Module.Finite R N
⊢ (⊤.prod ⊤).FG

Tactic:
exact hM.1.prod hN.1

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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
⊢ den ≤ den'

Tactic:
simp only [den, den']; gcongr

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
⊢ M • N ∈ I.matrix.carrier

Tactic:
intro i j

Goal state after:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ (M • N) i j ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := ⋯
⊢ N * M * single p q x + N - 1 ∈ matrix n I

Tactic:
intro i j

Goal state after:
case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
x : R
xIJ : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
p q : n
M : Matrix n n R
z : R
zMx : z * M q p * x + z - 1 ∈ I
N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else M i p * x * z)
i j : n
⊢ (N * M * single p q x + N - 1) i j ∈ ↑I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
a✝ : i ∈ Finset.univ
⊢ ∀ c ∈ Finset.univ, single i c (M i c) ∈ (matrix n I).jacobson

Tactic:
intro j _

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
i : n
a✝¹ : i ∈ Finset.univ
j : n
a✝ : j ∈ Finset.univ
⊢ single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ (llcomp R M N M).compr₂ (trace R M) = (llcomp R N M N).flip.compr₂ (trace R N)

Tactic:
apply
    (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
        (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ ((llcomp R M N M).compr₂ (trace R M)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N) =
    ((llcomp R N M N).flip.compr₂ (trace R N)).compl₁₂ (dualTensorHom R N M) (dualTensorHom R M N)
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
by
  have : x - y ≠ 0 := by simp_all [sub_eq_iff_eq_add]
  rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel_right₀ _ this]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
⊢ g₂ ?m.183 = 1

Tactic:
by
    rwa [show g₂ (i₂ x) = i₃ (f₂ x) by simpa using DFunLike.congr_fun hc₂ x]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
⊢ Nonempty (CommRing α)

Tactic:
obtain ⟨e⟩ := Fintype.truncEquivFin α
    exact ⟨open scoped Fin.CommRing in e.commRing⟩

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R ≃+* S
h : IsIntegrallyClosed R
⊢ IsIntegrallyClosed S

Tactic:
let _ : Algebra S R := f.symm.toRingHom.toAlgebra

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R ≃+* S
h : IsIntegrallyClosed R
x✝ : Algebra S R := f.symm.toRingHom.toAlgebra
⊢ IsIntegrallyClosed S
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
by
  refine ⟨fun ⟨x, hx⟩ ↦ ?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩
  by_cases ha : a = 0
  · simpa [ha, hn] using hx
  let K := FractionRing R
  replace ha : algebraMap R K a ≠ 0 := fun h ↦
    ha <| (injective_iff_map_eq_zero _).1 (IsFractionRing.injective R K) _ h
  let y := (algebraMap R K b) / (algebraMap R K a)
  have hy : IsIntegral R y := by
    refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩
    simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]
    replace hx := congr_arg (algebraMap R K) hx
    rw [map_pow] at hx
    simp [hx, ha]
  obtain ⟨k, hk⟩ := algebraMap_eq_of_integral hy
  refine ⟨k, IsFractionRing.injective R K ?_⟩
  rw [map_mul, hk, mul_div_cancel₀ _ ha]

Goal state after: