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

Goal state before:
pp: case h
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'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e.toHomeomorph.symm) (TopologicalSpace.induced (⇑e) τ) = τ

Tactic:
induced_compose

Goal state after:
case h
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'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced (⇑e) τ ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A} ∧
    TopologicalSpace.induced (⇑e ∘ ⇑e.toHomeomorph.symm) τ = τ
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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
⊢ (ConcreteCategory.hom (cM.ι.app i)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app i)) r • (ConcreteCategory.hom (cM.ι.app i)) m

Tactic:
let := filteredColimitsModule R M H

Goal state after:
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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
⊢ (ConcreteCategory.hom (cM.ι.app i)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app i)) r • (ConcreteCategory.hom (cM.ι.app i)) m
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S

Tactic:
simp_rw [Algebra.isEpi_iff_forall_one_tmul_eq, eq_comm]

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : M ≃L[R] M
this : (↑((ContinuousLinearEquiv.unitsEquiv R M).symm e))⁻¹ʳ = (↑e).inverse
⊢ (↑e)⁻¹ʳ = (↑e).inverse

Tactic:
by
    convert! this

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

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
⊢ ((if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
      if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0).Nodup

Tactic:
by
        split_ifs with h₁ h₂
        · simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
          let f : ((left a : WalkingMulticospan J) ⟶ right b) → Prop
            | .fst a => True
            | .snd a => False
          apply ne_of_apply_ne f
          conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]
          conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]
          simp
        all_goals simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat).obj X).str ≤
    TopologicalSpace.induced (fun x ↦ Finsupp.single x 1)
      (TopologicalSpace.induced ((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun
        ((𝟭 (TopModuleCat R)).obj X).topologicalSpace)

Tactic:
induced_compose

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ ((forget₂ (TopModuleCat R) TopCat).obj X).str ≤
    TopologicalSpace.induced
      (((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun ∘ fun x ↦
        Finsupp.single x 1)
      ((𝟭 (TopModuleCat R)).obj X).topologicalSpace
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
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q
  let f (S : Σ R : Subtype Q', FGAlgCatSkeleton R) : CommRingCat := .of S.2.eval.obj
  refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
  obtain ⟨R, hR, φ, hφ⟩ := hPQ S hS
  wlog hR' : Q' R generalizing R
  · obtain ⟨R', hR', ⟨e⟩⟩ := hQQ' _ hR
    exact this R' (hQ'Q _ hR') (e.inv ≫ φ)
      (hφ.comp e.symm.commRingCatIsoToRingEquiv.finite.finiteType) hR'
  obtain ⟨T, e, he⟩ := hφ.exists_smallRepr
  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_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₃
⊢ 0 x = 0

Tactic:
zero_apply

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₃
⊢ 0 = 0
Module: Mathlib.Algebra.Module.SnakeLemma

Goal state before:
pp: case mpr
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_8
K₃ : Type u_9
C₁ : Type u_10
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
⊢ x ∈ Set.range ⇑F → (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0

Tactic:
rintro ⟨y, rfl⟩
    exact (δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ (ι₂ y) congr($hF y)
      _ (by rw [map_zero, hι₂.apply_apply_eq_zero])).trans π₁.map_zero

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

Goal state before:
pp: case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
f₂ : (F ⋙ coyoneda.obj (Opposite.op S)).obj j
e :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) f₂
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) f₂

Tactic:
obtain ⟨k, hik, hjk, e⟩ := RingHom.EssFiniteType.exists_comp_map_eq_of_isColimit
      R (F ⋙ Under.forget R) { app i := (F.obj i).hom } S.hom ((Under.forget R).mapCocone c)
      (PreservesColimit.preserves hc).some
      (RingHom.FiniteType.of_finitePresentation hS).essFiniteType
      f₁.right (Under.w f₁) f₂.right (Under.w f₂) congr($(e).right)

Goal state after:
case refine_2
J : Type uJ
inst✝² : Category.{vJ, uJ} J
inst✝¹ : IsFiltered J
R : CommRingCat
S : Under R
hS : (Hom.hom S.hom).FinitePresentation
F : J ⥤ Under R
inst✝ : PreservesColimit (F ⋙ Under.forget R) (forget CommRingCat)
c : Cocone F
hc : IsColimit c
i j : J
f₁ : (F ⋙ coyoneda.obj (Opposite.op S)).obj i
f₂ : (F ⋙ coyoneda.obj (Opposite.op S)).obj j
e✝ :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app i)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op S)).mapCocone c).ι.app j)) f₂
k : J
hik : i ⟶ k
hjk : j ⟶ k
e : Under.Hom.right f₁ ≫ (F ⋙ Under.forget R).map hik = Under.Hom.right f₂ ≫ (F ⋙ Under.forget R).map hjk
⊢ ∃ k f g,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op S)).map g)) f₂
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X B : C
inst✝ : HasFiniteWidePushouts C
⊢ HasFiniteColimits (Under B)

Tactic:
by
  rw [← hasFiniteLimits_opposite_iff]
  exact hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : p • r = 0
⊢ False

Tactic:
nsmul_eq_mul

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fintype R
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : p ∣ Fintype.card R
h₀ : ¬p ∣ ringChar R
r : R
hr : addOrderOf r = p
hr₁ : ↑p * r = 0
⊢ False
Module: Mathlib.Algebra.Category.Ring.Under.Property

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQp : HasFiniteProducts fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).IsStableUnderCobaseChange
R S : CommRingCat
f : R ⟶ S
this✝ :
  CreatesFiniteProducts (MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ R)
n : ℕ
K : Discrete (Fin n) ⥤ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q).Under ⊤ R
this :
  PreservesLimit K
    (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ f ⋙
      MorphismProperty.Under.forget (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ S)
⊢ PreservesLimit K (MorphismProperty.Under.pushout (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊤ f)

Tactic:
exact preservesLimit_of_reflects_of_preserves _ (MorphismProperty.Under.forget _ ⊤ S)

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

Goal state before:
pp: R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
⊢ IsIso ((Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)).lift (Fork.ofι h' w')) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))

Tactic:
have heq : (Under.equalizerForkIsLimit _ _).lift (Fork.ofι h' w') =
      (AlgHom.tensorEqualizer S S (toAlgHom f) (toAlgHom g)).toUnder ≫
        Under.homMk (CommRingCat.ofHom (.id _)) := by
    refine Fork.IsLimit.hom_ext (Under.equalizerForkIsLimit _ _) ?_
    rw [Fork.IsLimit.lift_ι]
    ext : 2
    dsimp
    ext x <;> rfl

Goal state after:
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f g : A ⟶ B
c : Fork f g := Under.equalizerFork f g
hc : IsLimit c := Under.equalizerForkIsLimit f g
ι : R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g)) ⟶ A := ((toAlgHom f).equalizer (toAlgHom g)).val.toUnder
h' : (R.tensorProd S).obj (R.mkUnder ↥((toAlgHom f).equalizer (toAlgHom g))) ⟶ (R.tensorProd S).obj A :=
  (R.tensorProd S).map ι
w' : h' ≫ (R.tensorProd S).map f = h' ≫ (R.tensorProd S).map g
e : IsLimit ((R.tensorProd S).mapCone c) ≃ IsLimit (Fork.ofι h' w') := isLimitMapConeForkEquiv (R.tensorProd S) ⋯
heq :
  (Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)).lift (Fork.ofι h' w') =
    (AlgHom.tensorEqualizer (↑S) (↑S) (toAlgHom f) (toAlgHom g)).toUnder ≫
      CategoryTheory.Under.homMk
        (ofHom
          (RingHom.id
            ↥((Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom f)).equalizer
                (Algebra.TensorProduct.map (AlgHom.id ↑S ↑S) (toAlgHom g)))))
        ⋯
⊢ IsIso ((Under.equalizerForkIsLimit ((R.tensorProd S).map f) ((R.tensorProd S).map g)).lift (Fork.ofι h' w')) ↔
    Function.Bijective ⇑(AlgHom.tensorEqualizer (↑R) (↑S) (toAlgHom f) (toAlgHom g))
Module: Mathlib.Algebra.CharP.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
z : ℤ
hp : Nat.Prime p
⊢ IsUnit ↑z ↔ ¬↑p ∣ z

Tactic:
by
  obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
  · simp [CharP.isUnit_natCast_iff hp, Int.ofNat_dvd]
  · simp [CharP.isUnit_natCast_iff hp, Int.dvd_neg, Int.ofNat_dvd]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
a : ℤ
⊢ a ∈ RingHom.ker (algebraMap ℤ R) ↔ a ∈ Ideal.span {↑p}

Tactic:
simp [CharP.intCast_eq_zero_iff R p, Ideal.mem_span_singleton]

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

Goal state before:
pp: 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

Tactic:
rcases o with - | b <;> intro h

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

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

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

Tactic:
simp [*, take_succ]

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

Goal state before:
pp: case succ
α : Type u
n✝ : ℕ
a✝ : ∀ (s : Stream' α), (take n✝ s).length = n✝
s : Stream' α
⊢ (take (n✝ + 1) s).length = n✝ + 1

Tactic:
simp [*, take_succ]

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

Goal state before:
pp: α : Type u
s : Stream' α
m n : ℕ
⊢ List.take (m + 1) (take (n + 1) s) = take (min (n + 1) (m + 1)) s

Tactic:
by rw [take_succ, List.take_succ_cons, Nat.succ_min_succ, take_succ, take_take]

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
h : LiftRel R ca cb
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
let ⟨b', mb', ab⟩ := h.left ma
      rwa [mem_unique mb mb']

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

Goal state before:
pp: case pure
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α
b : β
⊢ LiftRelAux R C (Sum.inl a) (pure b).destruct ↔ ∃ b_1, b_1 ∈ pure b ∧ R a b_1

Tactic:
| pure b =>

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

Goal state before:
pp: case refine_2.pure
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
b : β
Hc : C ca'.think (pure b)
h : LiftRelAux R C ca'.think.destruct (pure b).destruct
⊢ LiftRel R ca' (pure b)

Tactic:
| pure b =>

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
hp : p ≠ 0
⊢ (p * if H : p = 0 then 0 else Classical.choose ⋯) = 1

Tactic:
dif_neg hp,

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
hp : p ≠ 0
⊢ p * Classical.choose ⋯ = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
x : R
hx : ∀ (x_1 : I), 1 - e x_1 ∣ x
this : ∀ (s : Finset I), (∏ i ∈ s, (1 - e i)) * x = x
⊢ x = 0

Tactic:
by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k = ⊥

Tactic:
← le_bot_iff,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : k ≤ m
hk : (f.genEigenspace μ) m = ⊥
⊢ (f.genEigenspace μ) k ≤ ⊥
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ (trace R M) (↑f * g * ↑f⁻¹) = (trace R M) g

Tactic:
rw [trace_mul_comm]
  simp

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x = 0

Tactic:
rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x ∈ (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) k
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case intro.inr
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i ≠ j
⊢ (Matrix.single j i 1).trace = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)

Tactic:
Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm

Goal state after:
case intro.inr
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
i j : ι
hij : i ≠ j
⊢ 0 = (contractLeft R M) (b.coord i ⊗ₜ[R] b j)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R M) (↑(LinearEquiv.refl R M) ∘ₗ f) = (trace R M) f

Tactic:
LinearEquiv.refl_toLinearMap,

Goal state after:
case pos
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R M) (id ∘ₗ f) = (trace R M) f
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case neg
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ 0 = 0 f

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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ ¬∃ s, Nonempty (Basis (↥s) R N)

Tactic:
zero_apply

Goal state after:
case neg
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ 0 = 0

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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ s, Nonempty (Basis (↥s) R M)
⊢ ¬∃ s, Nonempty (Basis (↥s) R N)
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
mul_comm : ∀ (a b : R), a * b = b * a
one_mul : ∀ (a : R), 1 * a = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
a : R
⊢ a * 1 = a

Tactic:
by
    rw [mul_comm, one_mul]

Goal state after: