mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
⊢ IsLocalHom f ↔ PrimeSpectrum.comap f (closedPoint S) = closedPoint R

Tactic:
have := (local_hom_TFAE f).out 0 4
  rw [this, PrimeSpectrum.ext_iff]
  rfl

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : b ≤ iSup s
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1

Tactic:
replace hb : (b : α) ≤ iSup ((↑) ∘ s) := le_trans hb <| (coe_iSup s) ▸ le_refl _

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : ↑b ≤ iSup (Subtype.val ∘ s)
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
⊢ H ≤ Subgroup.map (normalizer ↑H).subtype (comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))

Tactic:
by
    intro y hy
    simp only [Subgroup.coe_subtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]
    refine ⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩
    dsimp only
    rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]
    simpa using! hy

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
key : p ∣ Nat.card ↥⊥
⊢ p ∣ 1

Tactic:
card_bot

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Nat.card G
h : ↑P = ⊥
key : p ∣ 1
⊢ p ∣ 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : ↑(ϕ • P) = Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P

Tactic:
Subsingleton.elim (ϕ • P) P,

Goal state after:
G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
h : ↑P = Subgroup.map ((MulDistribMulAction.toMonoidEnd (G ≃* G) G) ϕ) ↑P
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : Fin (s.length + 1)
hx : s.toFun i ≠ last s
hi : ↑i < (s.length - 1).succ
⊢ s.toFun i ∈ eraseLast s

Tactic:
exact ⟨⟨↑i, hi⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso
    ((snoc s₁ x₁ hsat₁).toFun
        (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).castSucc,
      (snoc s₁ x₁ hsat₁).toFun (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)).succ)
    ((snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).castSucc,
      (snoc s₂ x₂ hsat₂).toFun
        (e (Fin.last (s₁.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length))).succ)

Tactic:
change Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc,
        (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
      ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).castSucc,
        (snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).succ)

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc, (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
    ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).castSucc, (snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).succ)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S✝ : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S✝
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
S : Submodule R M
⊢ ∃ a, S = R ∙ a

Tactic:
by
    obtain rfl | rfl := eq_bot_or_eq_top S
    · exact ⟨0, Submodule.span_zero.symm⟩
    have := IsSimpleModule.nontrivial R M
    have ⟨m, hm⟩ := exists_ne (0 : M)
    exact ⟨m, (span_singleton_eq_top R hm).symm⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
g : PolynomialModule R M
n : ℕ
⊢ ((monomial i) r • g).coeff n = if i ≤ n then r • g.coeff (n - i) else 0

Tactic:
induction g using PolynomialModule.induction_linear with

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
⊢ a * ↑(μ i) ∈ p j

Tactic:
have := coe_mem (μ i)

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
p : ι → Ideal R
S : Finset ι
hp : (↑S).Pairwise fun i j ↦ p i ⊔ p j = ⊤
h : S.Nonempty
x : M
hx : ∀ (a : ↑↑(⨅ i ∈ S, p i)), ↑a • x = 0
μ : (i : ι) → ↥(⨅ j ∈ S, ⨅ (_ : j ≠ i), p j)
hμ : ∑ i ∈ S, ↑(μ i) = 1
i : ι
a : R
ha : a ∈ ↑(p i)
j : ι
hj : j ∈ S
ij : ¬j = i
this : ↑(μ i) ∈ ⨅ j ∈ S, ⨅ (_ : j ≠ i), p j
⊢ a * ↑(μ i) ∈ p j
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x✝ y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
x : PolynomialModule R R
⊢ (coeffAddEquiv.trans (AddMonoidAlgebra.coeffAddEquiv.symm.trans (toFinsuppIso R).symm.toAddEquiv)).toFun (r • x) =
    (RingHom.id R[X]) r •
      (coeffAddEquiv.trans (AddMonoidAlgebra.coeffAddEquiv.symm.trans (toFinsuppIso R).symm.toAddEquiv)).toFun x

Tactic:
by
    dsimp
    induction x using induction_linear with
    | zero => simp
    | add _ _ hp hq => simp_all [smul_add, mul_add]
    | single n a =>
    ext i
    simp only [coeffAddEquiv_apply, AddMonoidAlgebra.coeffAddEquiv_symm_apply,
      toFinsuppIso_symm_apply, coeff_ofFinsupp, smul_single_apply, smul_eq_mul, coeff_single,
      AddMonoidAlgebra.ofCoeff_single, ofFinsupp_single]
    split_ifs with hn
    · rw [show i = (i - n) + n by lia, Polynomial.coeff_mul_monomial]
      simp
    · rw [Polynomial.coeff_mul, Finset.sum_eq_zero]
      simp [Polynomial.coeff_monomial]
      lia

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
heq : ⨆ i ∈ ⊤, torsionBySet R M ↑(map i) = torsionBySet R M ↑(⨅ i ∈ ⊤, map i)
⊢ torsionBySet R M ↑P ⊔ torsionBySet R M ↑Q = torsionBySet R M ↑(P ⊓ Q)

pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
⊢ (↑⊤).Pairwise fun i j ↦ map i ⊔ map j = ⊤

Tactic:
· have : ⨆ i, ⨆ (_ : i = 0 ∨ i = 1), torsionBySet R M ↑(map i) =
        torsionBySet R M ↑(map 0) ⊔ torsionBySet R M ↑(map 1) := iSup_pair
    simpa [Finset.top_eq_univ, Fin.univ_succ, Fin.isValue, coe_iInf, this] using heq

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : Ideal R
hc : P ⊔ Q = ⊤
map : Fin 2 → Ideal R :=
  fun x ↦
    match x with
    | 0 => P
    | 1 => Q
⊢ (↑⊤).Pairwise fun i j ↦ map i ⊔ map j = ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
algebraize [f.hom, f'.hom, g.hom, g'.hom, f'.hom.comp g.hom]

Goal state after:
A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
algInst✝⁴ : Algebra ↑A ↑B := (Hom.hom f).toAlgebra
algInst✝³ : Algebra ↑A' ↑B' := (Hom.hom f').toAlgebra
algInst✝² : Algebra ↑A ↑A' := (Hom.hom g).toAlgebra
algInst✝¹ : Algebra ↑B ↑B' := (Hom.hom g').toAlgebra
algInst✝ : Algebra ↑A ↑B' := ((Hom.hom f').comp (Hom.hom g)).toAlgebra
scalarTowerInst✝ : IsScalarTower ↑A ↑A' ↑B' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap ↑A ↑B'))
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ I * I

Tactic:
exact Ideal.mul_mem_mul hx hy

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u
inst✝⁴ : CommRing R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ RingHom.ker f.kerSquareLift.toRingHom ≤ (RingHom.ker f.toRingHom).cotangentIdeal

Tactic:
intro x hx; obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x; exact ⟨x, hx, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ x ∈ ⨅ i, I ^ i • ⊤ → ∃ r, ↑r • x = x

Tactic:
obtain ⟨r, hr₁, hr₂⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
        obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
        have := hk k (le_refl _)
        rw [hN, hN] at this
        exact le_of_eq this.symm)
    intro H
    exact ⟨⟨r, hr₁⟩, hr₂ _ H⟩

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f : X ⟶ Y
inst✝ : IsIso f
i : β
⊢ IsIso (f i)

Tactic:
change IsIso ((eval i).map f)
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Tactic:
have := congr_app (associativity F m₁ m₂ m₃) X
  dsimp at this
  simpa using this

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
⊢ ∀ (X : Discrete A),
    (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj X)).hom =
      MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj X) ≫
        (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as X.as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor X).hom

Tactic:
by
        rintro ⟨n⟩
        ext X
        simp [h.zero_add_inv_app, ← Functor.map_comp]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.restrictScalars S (ideal R S) ≤
    Submodule.restrictScalars S (Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Tactic:
← KaehlerDifferential.submodule_span_range_eq_ideal,

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S (Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ φ.f 1 ≫ ((single₀ V).obj X).d 1 0 = 0

Tactic:
HomologicalComplex.single_obj_d,

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ φ.f 1 ≫ 0 = 0
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
φ : (single₀ V).obj X ⟶ C
⊢ ((single₀ V).obj X).d 0 1 ≫ φ.f 1 = 0

Tactic:
HomologicalComplex.single_obj_d,

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : CochainComplex V ℕ
X : V
φ : (single₀ V).obj X ⟶ C
⊢ 0 ≫ φ.f 1 = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).inv.app X) ≫ (shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X =
    (shiftFunctorAdd C a₂ a₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).inv.app X

Tactic:
by
  simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
⊢ j + 0 = 0 + j

Tactic:
zero_add,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
⊢ j + 0 = j
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ j + 0 = 0 + j

Tactic:
zero_add,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
i j : A
h : i + j = 0
X : C
⊢ j + 0 = j
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ ({ f := fun i ↦ (f i).hom, comm' := hf } ≫ { f := fun i ↦ (f i).inv, comm' := ⋯ }).f i = (𝟙 C₁).f i

Tactic:
exact (f i).hom_inv_id

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + (m' + (m + n)) = 0

Tactic:
← add_assoc m',

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + (m' + m + n) = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + (0 + n) = 0

Tactic:
zero_add,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + n = 0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Function.Surjective ⇑(D R S).tensorProductTo

Tactic:
by
  intro x; obtain ⟨x, rfl⟩ := (KaehlerDifferential.ideal R S).toCotangent_surjective x
  exact ⟨x, KaehlerDifferential.D_tensorProductTo x⟩

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X) =
    (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
        (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)

Tactic:
← cancel_mono ((shiftFunctorComm C m₁ m₃).inv.app (X⟦m₂⟧)),

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ ((shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫ (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X)) ≫
      (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X) =
    ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
        (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
          (shiftFunctorComm C m₁ m₃).hom.app ((shiftFunctor C m₂).obj X)) ≫
      (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (↑(quotKerTotalEquiv R S).symm).compDer (D R S) = derivationQuotKerTotal R S

Tactic:
convert! (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential_comp

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
| (mapBaseChange R A B) (x ⊗ₜ[A] y)

Tactic:
← mul_one x,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
| (mapBaseChange R A B) ((x * 1) ⊗ₜ[A] y)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_2.e'_12
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ mapRange.linearMap (Algebra.linearMap B B) ∘ₗ lmapDomain B B ⇑(algebraMap B B) = LinearMap.id

Tactic:
· ext; simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

Tactic:
constructor
  · intro h X Y f hf
    exact h _ (W.le_isoClosure _ hf)
  · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    simp only [Arrow.iso_w' e, F.map_comp]
    have := h _ hf'
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
⊢ ofHom 0 = 0

Tactic:
simp only [ofHom, HomologicalComplex.zero_f_apply, ofHoms_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ (e ≫ g).f i = (((dNext i) fun i j ↦ h.hom i j ≫ g.f j) + (prevD i) fun i j ↦ h.hom i j ≫ g.f j) + (f ≫ g).f i

Tactic:
rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp,
    comp_f, Preadditive.add_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i) ≫ D.d i j = 0 + C.d i j ≫ hom j i ≫ D.d i j

Tactic:
zero_add,

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
hij : c.Rel i j
eq1 : (prevD i) hom ≫ D.d i j = 0
eq2 : C.d i j ≫ (dNext j) hom = 0
⊢ (C.d i j ≫ hom j i) ≫ D.d i j = C.d i j ≫ hom j i ≫ D.d i j
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j

Tactic:
zero_add,

Goal state after:
case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j