mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ rank ↥(closure s) ≤ Nat.card ↑s

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
G : Type u_1
inst✝¹ : Group G
s : Set G
inst✝ : Finite ↑s
this : Fintype ↑s
⊢ rank ↥(closure s) ≤ Fintype.card ↑s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤

Tactic:
eq_top_iff

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → ⊤ ≤ U
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
⊢ 0 < #{a | orderOf a = Nat.card α}

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
⊢ 0 < #{a | orderOf a = Fintype.card α}
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : x ∈ LocallyFiniteOrder.finsetIoc a b
hxmin : ∀ ⦃y : α⦄, (fun x ↦ x ∈ LocallyFiniteOrder.finsetIoc a b) y → y ≤ x → x ≤ y
⊢ ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : a < x ∧ x ≤ b
hxmin : ∀ ⦃y : α⦄, a < y ∧ y ≤ b → y ≤ x → x ≤ y
⊢ ∃ x, a ⋖ x ∧ x ≤ b
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d

Tactic:
have h : (powMonoidHom d : G →* G).ker.index ≠ 0 := Subgroup.index_ne_zero_of_finite

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
h : (powMonoidHom d).ker.index ≠ 0
⊢ Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g'

Tactic:
nth_rw 2 [← zpow_one g']

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g' ^ 1
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p G
hP : ↑P ≤ N
⊢ normalizer ↑P ⊔ N = ⊤

Tactic:
rw [← normalizer_sup_eq_top (P.subtype hP), P.coe_subtype, subgroupOf_map_subtype,
    inf_of_le_left hP, P.coe_coe]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, ∑ i ∈ {a}, ↑(μ i) = 1) ↔ (↑{a}).Pairwise fun i j ↦ I i ⊔ I j = ⊤

pp: case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    s.Nonempty →
      ((∃ μ, ∑ i ∈ s, ↑(μ i) = 1) ↔ (↑s).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a s h, ↑(μ i) = 1) ↔ (↑(Finset.cons a s h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)

Tactic:
· simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true]
    refine fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩
    · simp [h]
    · simp only [dif_pos, Submodule.coe_mk]

Goal state after:
case refine_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s),
    s.Nonempty →
      ((∃ μ, ∑ i ∈ s, ↑(μ i) = 1) ↔ (↑s).Pairwise fun i j ↦ I i ⊔ I j = ⊤) →
        ((∃ μ, ∑ i ∈ Finset.cons a s h, ↑(μ i) = 1) ↔ (↑(Finset.cons a s h)).Pairwise fun i j ↦ I i ⊔ I j = ⊤)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case inr
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
⊢ ⨆ i ∈ S, torsionBySet R M ↑(p i) = torsionBySet R M ↑(⨅ i ∈ S, p i)

Tactic:
apply le_antisymm

Goal state after:
case inr.a
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
⊢ ⨆ i ∈ S, torsionBySet R M ↑(p i) ≤ torsionBySet R M ↑(⨅ i ∈ S, p i)

case a
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
⊢ torsionBySet R M ↑(⨅ i ∈ S, p i) ≤ ⨆ i ∈ S, torsionBySet R M ↑(p i)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : ↥((mapSubmodule R M a) ⟨p, hp⟩)
⊢ (of R M a).symm ↑x ∈ p

Tactic:
obtain ⟨x, hx⟩ := x

Goal state after:
R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : Submodule R M
hp : p ∈ ((Algebra.lsmul R R M) a).invtSubmodule
x : AEval R M a
hx : x ∈ (mapSubmodule R M a) ⟨p, hp⟩
⊢ (of R M a).symm ↑⟨x, hx⟩ ∈ p
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) = reesAlgebra I

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) ≤ reesAlgebra I

case a
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ reesAlgebra I ≤ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ P = map N.mkQ (I • N')

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ P ≤ map N.mkQ (I • N')

case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
⊢ map N.mkQ (I • N') ≤ map N.mkQ P
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N = N'

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N ≤ N'

case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N = map (I • N).mkQ N'
⊢ N' ≤ N
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i)) = F.submodule.toAddSubmonoid

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i)) ≤ F.submodule.toAddSubmonoid

case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ F.submodule.toAddSubmonoid ≤ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ ⋃ i, single R i '' ↑(F.N i) ⊆ ↑F.submodule.toAddSubmonoid

Tactic:
Set.iUnion_subset_iff

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑F.submodule.toAddSubmonoid
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ ⋃ i, single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
Set.iUnion_subset_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ (∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ I.Cotangent ≃ₗ[R] ↥I.cotangentIdeal

Tactic:
refine
  { LinearMap.codRestrict (I.cotangentIdeal.restrictScalars R) I.cotangentToQuotientSquare
      fun x => by rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _,
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Function.Injective fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩

case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Function.Surjective fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e : Submodule.Quotient.mk ↑x = Submodule.Quotient.mk ↑y
⊢ ↑x - ↑y ∈ I ^ 2

Tactic:
Submodule.Quotient.eq

Goal state after:
case refine_1
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x y : ↥I
e : ↑x - ↑y ∈ I ^ 2
⊢ ↑x - ↑y ∈ I ^ 2
Module: Mathlib.RingTheory.Ideal.Cotangent

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

Goal state after:
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

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.toRingHom).cotangentIdeal ≤ RingHom.ker f.kerSquareLift.toRingHom
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ ⊤.spanRank = ⊤.spanRank

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ ⊤.spanRank ≤ ⊤.spanRank

case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ ⊤.spanRank ≤ ⊤.spanRank
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X Y : Dᵒᵖ
f : X ⟶ Y
b : ↑(R.obj X)
⊢ (ConcreteCategory.hom (d'.app Y).desc)
      ((ModuleCat.Hom.hom ((relativeDifferentials' φ').map f)) (CommRingCat.KaehlerDifferential.d b)) =
    (ModuleCat.Hom.hom (M'.map f)) (d'.d b)

Tactic:
erw [relativeDifferentials'_map_d φ' f]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X Y : Dᵒᵖ
f : X ⟶ Y
b : ↑(R.obj X)
⊢ (ConcreteCategory.hom (d'.app Y).desc) (CommRingCat.KaehlerDifferential.d ((ConcreteCategory.hom (R.map f)) b)) =
    (ModuleCat.Hom.hom (M'.map f)) (d'.d b)
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
⊢ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.restrictScalars S (ideal R S)

Tactic:
apply le_antisymm

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 R S)

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.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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
⊢ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = ideal R S

Tactic:
apply le_antisymm

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

case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ideal R S ≤ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
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₂ : HomologicalComplex V c
f : C₁.Hom C₂
i : ι
w : c.Rel i (c.next i)
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv

Tactic:
simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

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
i j k : A
h : i + j = k
⊢ j + i = k

Tactic:
by rw [add_comm j i, h]

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
X : C
n : A
⊢ 𝟙 ((shiftFunctor C n).obj X) = (shiftFunctor C n).map (𝟙 X)

Tactic:
rw [Functor.map_id]

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

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) = ideal R S

Tactic:
apply le_antisymm

Goal state after:
case h.a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) ≤ ideal R S

case a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ ideal R S ≤ Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S))
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
⊢ (linearCombination S ⇑(D R S)).ker = kerTotal R S

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤ kerTotal R S

case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ kerTotal R S ≤ (linearCombination S ⇑(D R S)).ker
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ x ≫ K.d i' i ≫ K.d i j = 0

Tactic:
K.d_comp_d,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
⊢ x ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ x ≫ K.d i' i ≫ K.d i j = 0

Tactic:
K.d_comp_d,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
i' : ι
x : A ⟶ K.X i'
hx : k = x ≫ K.d i' i
h : ¬c.Rel i' i
⊢ x ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)

Tactic:
rw [Functor.map_comp, ShortComplex.opcyclesMap_comp]

Goal state after:
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
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A
        (Set.range fun x ↦
          single ((algebraMap A B) x.1) 1 + single ((algebraMap A B) x.2) 1 -
            single ((algebraMap A B) x.1 + (algebraMap A B) x.2) 1) ⊔
      (Submodule.span A
          (Set.range fun x ↦
            single ((algebraMap A B) x.2) ((algebraMap A B) x.1) +
                single ((algebraMap A B) x.1) ((algebraMap A B) x.2) -
              single ((algebraMap A B) x.1 * (algebraMap A B) x.2) 1) ⊔
        (Submodule.span A (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔
          Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1))) =
    Submodule.span A
        (Set.range
          ((fun x ↦ single x.1 1 + single x.2 1 - single (x.1 + x.2) 1) ∘
            Prod.map ⇑(algebraMap A B) ⇑(algebraMap A B))) ⊔
      (Submodule.span A
          (Set.range
            ((fun x ↦ single x.2 x.1 + single x.1 x.2 - single (x.1 * x.2) 1) ∘
              Prod.map ⇑(algebraMap A B) ⇑(algebraMap A B))) ⊔
        Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1))

Tactic:
congr!

Goal state after:
case e'_4.e'_4
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.span A (Set.range fun x ↦ single ((algebraMap A B) ((algebraMap R A) x)) 1) ⊔
      Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1) =
    Submodule.span A (Set.range fun x ↦ single ((algebraMap S B) x) 1)
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
⊢ (mapBaseChange R A B).range = (map R A B B).ker

Tactic:
apply le_antisymm

Goal state after:
case a
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
⊢ (mapBaseChange R A B).range ≤ (map R A B B).ker

case a
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
⊢ (map R A B B).ker ≤ (mapBaseChange R A B).range
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mp
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
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ (kerCotangentToTensor R A B).range → x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker

pp: case mpr
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
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker → x ∈ (kerCotangentToTensor R A B).range

Tactic:
· rintro ⟨x, rfl⟩
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    simp only [kerCotangentToTensor_toCotangent, Submodule.restrictScalars_mem, LinearMap.mem_ker,
      mapBaseChange_tmul, map_D, RingHom.mem_ker.mp x.2, map_zero, smul_zero]

Goal state after:
case mpr
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
h : Function.Surjective ⇑(algebraMap A B)
x : B ⊗[A] Ω[A⁄R]
⊢ x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker → x ∈ (kerCotangentToTensor R A B).range