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

Goal state before:
pp: case property.refine_3.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 x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op)

Tactic:
F.1.map_comp,

Goal state after:
case property.refine_3.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 x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map (eqToHom ⋯).op ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r s : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a b : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    (Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a +
          Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            c +
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩
    obtain ⟨s, α, β, h₁, h₂, h₃, h₄⟩ := crown₄
      (rightToMax U₁ V ≫ leftToMax (max U₁ V) (max U₂ V)) (rightToMax (max U₁ U₂) V)
      (rightToMax U₂ V ≫ rightToMax (max U₁ V) (max U₂ V)) (rightToMax (max U₁ U₂) V)
      (leftToMax U₁ V ≫ leftToMax (max U₁ V) (max U₂ V))
      (leftToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V)
      (leftToMax U₂ V ≫ rightToMax (max U₁ V) (max U₂ V))
      (rightToMax U₁ U₂ ≫ leftToMax (max U₁ U₂) V)
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ β α ?_
    dsimp
    simp only [add_smul, map_add, ← ConcreteCategory.comp_apply, ← Functor.map_comp, *]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι✝ : Type u_2
inst✝⁵ : Finite ι✝
ι : Type u_2
inst✝⁴ : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (A i)] [inst_1 : (i : ι) → Module R (A i)]
    [inst_2 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst✝³ : (i : Option ι) → AddCommMonoid (A i)
inst✝² : (i : Option ι) → Module R (A i)
inst✝¹ : (i : Option ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option ι), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option ι) → A i)

Tactic:
let e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι

Goal state after:
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι✝ : Type u_2
inst✝⁵ : Finite ι✝
ι : Type u_2
inst✝⁴ : Fintype ι
hind :
  ∀ {A : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (A i)] [inst_1 : (i : ι) → Module R (A i)]
    [inst_2 : (i : ι) → TopologicalSpace (A i)] [∀ (i : ι), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : ι) → A i)
A : Option ι → Type u_3
inst✝³ : (i : Option ι) → AddCommMonoid (A i)
inst✝² : (i : Option ι) → Module R (A i)
inst✝¹ : (i : Option ι) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option ι), IsModuleTopology R (A i)
e : Option ι ≃ ι ⊕ Unit := Equiv.optionEquivSumPUnit ι
⊢ IsModuleTopology R ((i : Option ι) → A i)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mp
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* 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₂
f : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

Tactic:
rintro ⟨f, rfl⟩
    exact ⟨f.continuous, f, rfl⟩

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

Goal state before:
pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
⊢ f = g

Tactic:
let f' : S →ₐ[R] T := ⟨f.hom, RingHom.congr_fun (congrArg Hom.hom e)⟩

Goal state after:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
T : CommRingCat
f g : of S ⟶ T
e : ofHom (algebraMap R S) ≫ f = ofHom (algebraMap R S) ≫ g
this : Algebra R ↑T := (Hom.hom (ofHom (algebraMap R S) ≫ g)).toAlgebra
f' : S →ₐ[R] ↑T := { toRingHom := Hom.hom f, commutes' := ⋯ }
⊢ f = g
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by
  algebraize [f.hom]
  have : Algebra.IsEpi R S := CommRingCat.epi_iff_epi.mp <| inferInstanceAs (Epi f)
  rwa [Algebra.isEpi_iff_surjective_algebraMap_of_finite] at this

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] (AlgHom.id R S) s = 1 ⊗ₜ[R] s

Tactic:
AlgHom.id_apply

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] s = 1 ⊗ₜ[R] s
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
⊢ IsEffective R S

Tactic:
intro s
  refine ⟨?_, TensorProduct.includeLeftSubRight_zero_of_mem_range⟩
  intro hs
  use g s
  apply (TensorProduct.lid R S).symm.injective
  rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ } ≫
      (ofCone c).π.app i =
    s.π.app i

Tactic:
ext x; exact congr($(hc.fac ((forget₂ _ _).mapCone s) i).hom x)

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 := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = (F.map φ ≫ F.map β) ≫ (h.isoMap α ⋯).inv

Tactic:
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 := IsFiltered.max i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv
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₀)
⊢ h.cocone ≅ c

Tactic:
refine Cocone.ext (asIso (c.ι.app i₀)) (fun j ↦ ?_)
    let i := IsFiltered.max i₀ j
    let α : i₀ ⟶ i := IsFiltered.leftToMax _ _
    let β : j ⟶ i := IsFiltered.rightToMax _ _
    dsimp
    rw [← c.w α, ← c.w β, h.coconeιApp_eq 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
A : C
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} ((const C).obj A)

Tactic:
have : Fact Cardinal.aleph0.IsRegular := Cardinal.fact_isRegular_aleph0
  exact ⟨Cardinal.aleph0, inferInstance, inferInstance⟩

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

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ IsCardinalFiltered J₂ κ

Tactic:
rw [isCardinalFiltered_iff]

Goal state after:
J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ (∀ ⦃ι : Type w⦄ (j : ι → J₂), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
    ∀ ⦃ι : Type w⦄ ⦃j k : J₂⦄ (f : ι → (j ⟶ k)), HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), f i ≫ a = b
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝⁵ : HasPullbacks A
inst✝⁴ : HasPullbacks T
inst✝³ : PreservesLimitsOfShape WalkingCospan L
X : T
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.HasOfPostcompProperty P
Y : CostructuredArrow L X
pres : LimitPresentation WalkingCospan Y
hpres : ∀ (j : WalkingCospan), MorphismProperty.costructuredArrowObj L P (pres.diag.obj j)
h :
  IsPullback (L.map (pres.π.app WalkingCospan.left).left) (L.map (pres.π.app WalkingCospan.right).left)
    (L.map (pres.diag.map WalkingCospan.Hom.inl).left) (L.map (pres.diag.map WalkingCospan.Hom.inr).left)
⊢ P (L.map (pres.diag.map WalkingCospan.Hom.inr).left ≫ (pres.diag.obj WalkingCospan.one).hom)

Tactic:
by simpa using hpres .right

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

Goal state before:
pp: T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ HasPullbacks (P.CostructuredArrow ⊤ L X)

Tactic:
apply +allowSynthFailures hasLimitsOfShape_of_closedUnderLimitsOfShape

Goal state after:
case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ HasLimitsOfShape WalkingCospan (Comma L (Functor.fromPUnit X))

case inst
T : Type u_1
inst✝⁷ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁶ : Category.{v_2, u_2} A
L : A ⥤ T
X : T
inst✝⁵ : P.IsStableUnderComposition
inst✝⁴ : P.IsStableUnderBaseChange
inst✝³ : P.HasOfPostcompProperty P
inst✝² : HasPullbacks A
inst✝¹ : HasPullbacks T
inst✝ : PreservesLimitsOfShape WalkingCospan L
⊢ (commaObj L (Functor.fromPUnit X) P).IsClosedUnderLimitsOfShape WalkingCospan
Module: Mathlib.CategoryTheory.Limits.MorphismProperty

Goal state before:
pp: T : Type u_1
inst✝⁵ : Category.{v_1, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{v_2, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ (MorphismProperty.structuredArrowObj L P).colimitsOfShape (Discrete PEmpty.{1}) ≤
    MorphismProperty.structuredArrowObj L P

Tactic:
by
    rintro X p
    let t : IsInitial X := (ObjectProperty.colimitsOfShape_isEmpty_iff _ _ _ |>.mp p).some
    let e : X ≅ StructuredArrow.mk (𝟙 (L.obj Y)) := t.uniqueUpToIso StructuredArrow.mkIdInitial
    simpa [MorphismProperty.structuredArrowObj_iff,
      P.structuredArrow_iso_iff e] using P.id_mem (L.obj Y)

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

Goal state before:
pp: case pos
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
⊢ 0⁻¹ ∈ S

Tactic:
inv_zero

Goal state after:
case pos
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
⊢ 0 ∈ S
Module: Mathlib.Algebra.CharZero.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p = r - ↑k • (p / ↑z)

Tactic:
div_eq_mul_inv,

Goal state after:
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
p r : R
z : ℤ
hz : z ≠ 0
⊢ (∃ k, k • p = z • r) ↔ ∃ k k_1, k_1 • p = r - ↑k • (p * (↑z)⁻¹)
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
a : α
s : Seq α
⊢ Option.map Prod.fst (some (a, s)) = some a

Tactic:
Option.map_some

Goal state after:
α : Type u
a : α
s : Seq α
⊢ some (a, s).fst = some a
Module: Mathlib.Data.Stream.Init

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

Tactic:
apply append_left_injective _ _ (a.drop (m + n)) ((a.drop m).drop n) <;>
    simp [-drop_drop]

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
⊢ ∀ m < n, ¬(↑s).get (m + 1) = none

Tactic:
intro m hmn hs

Goal state after:
case succ
α : Type u
n : ℕ
ih : ∀ {s : Seq α}, (∀ (h : s.Terminates), n ≤ s.length h) → (take n s).length = n
s : Seq α
hle : ∀ (h : s.Terminates), n + 1 ≤ s.length h
a : α
ha : a ∈ s.get? 0
h : s.tail.Terminates
m : ℕ
hmn : m < n
hs : (↑s).get (m + 1) = none
⊢ False
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
c : Computation α
⊢ (empty α <|> c) = c

Tactic:
by
  apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl
  intro s' s h; rw [← h]
  induction s using recOn with rw [think_empty]
  | pure s => simp
  | think s => simp only [BisimO, orElse_think, destruct_think]; rw [← think_empty]

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
n : ℕ
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none

Tactic:
rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
    IntFractPair.get?_seq1_eq_succ_get?_stream]

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

Goal state before:
pp: case e'_3
α : Type u
n : ℕ
x : α
s : Seq α
⊢ s.length' + 1 - (↑n + 1) = s.length' - ↑n

Tactic:
generalize s.length' = m

Goal state after:
case e'_3
α : Type u
n : ℕ
x : α
s : Seq α
m : ℕ∞
⊢ m + 1 - (↑n + 1) = m - ↑n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β → γ
s : Seq α
⊢ zipWith f s nil = nil

Tactic:
by
  ext1
  simp

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

Goal state before:

Tactic:
v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
        _ = ⌊v⌋ := by simp [fract_eq_zero]

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

Goal state before:
pp: n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)

Tactic:
cases n
  · simp
  · rw [two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
    simp only [← add_assoc, add_tsub_cancel_right]
    ring

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.a * φ P.a * (x - y) * (x - z) * (y - z) * (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
mul_ne_zero_iff,

Goal state after:
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.a ≠ 0 ∧ φ P.a ≠ 0) ∧ x - y ≠ 0) ∧ x - z ≠ 0) ∧ y - z ≠ 0) ∧
      (((φ P.a ≠ 0 ∧ φ P.a ≠ 0) ∧ x - y ≠ 0) ∧ x - z ≠ 0) ∧ y - z ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
this : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n
⊢ (1 - (1 - a ^ n) ^ n) * e₂ = 0

Tactic:
rw [this, mul_assoc]

Goal state after:
case inr.refine_2
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
n : ℕ
hn : (a - a ^ 2) ^ n = 0
k : Rᵐᵒᵖ
hk : MulOpposite.unop (1 ^ n - MulOpposite.op (1 - a ^ n) ^ n) = MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ n)) * k)
this : 1 - (1 - a ^ n) ^ n = MulOpposite.unop k * a ^ n
⊢ MulOpposite.unop k * (a ^ n * e₂) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * (e' * (1 - e₂) * e') = (1 - e₂) * e'

Tactic:
mul_sub,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * ((e' * 1 - e' * e₂) * e') = (1 - e₂) * e'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * (1 - e₂) * e' = 0

Tactic:
mul_sub,

Goal state after:
case refine_4
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (e₂ * 1 - e₂ * e₂) * e' = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
⊢ CompleteOrthogonalIdempotents e

Tactic:
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker f h he'' (fun _ ↦ ⟨_, rfl⟩)

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
he : ∀ (i : I), IsIdempotentElem (e i)
he' : ∀ (i : I), IsMulCentral (e i)
he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)
e' : I → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = ⇑f ∘ e
⊢ CompleteOrthogonalIdempotents e
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
⊢ Function.Surjective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
suffices Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j}) by
    intro x
    obtain ⟨x, rfl⟩ := Ideal.quotientInfToPiQuotient_surj this x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by ext i; simp [Ideal.quotientInfToPiQuotient]⟩
  intro i j hij
  rw [Ideal.isCoprime_span_singleton_iff]
  exact ⟨1, e i, by simp [mul_sub, he.ortho hij]⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (a / b)) 1 = (f.genEigenspace (b⁻¹ * a)) 1

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (a * b⁻¹)) 1 = (f.genEigenspace (b⁻¹ * a)) 1