mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 3)
⊢ (ofJ0 R).IsElliptic

Tactic:
isElliptic_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 3)
⊢ IsUnit (ofJ0 R).Δ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ (ofJ1728 R).IsElliptic

Tactic:
isElliptic_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j : R
inst✝ : W.IsElliptic
hu : Fact (IsUnit 2)
⊢ IsUnit (ofJ1728 R).Δ
Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ (ofJNe0Or1728 j).IsElliptic

Tactic:
isElliptic_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
j✝ : R
inst✝ : W.IsElliptic
j : R
h1 : Fact (IsUnit j)
h2 : Fact (IsUnit (j - 1728))
⊢ IsUnit (ofJNe0Or1728 j).Δ
Module: Mathlib.AlgebraicGeometry.Sites.Pretopology

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.IsMultiplicative
X : Scheme
S : Sieve X
⊢ S ∈ (grothendieckTopology P) X ↔ ∃ 𝒰, Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Tactic:
simp_rw [grothendieckTopology, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition]
  refine ⟨fun ⟨R, hR, hle⟩ ↦ ?_, fun ⟨𝒰, hle⟩ ↦ ⟨.ofArrows 𝒰.X 𝒰.f, 𝒰.mem_pretopology, hle⟩⟩
  rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
  obtain ⟨(𝒰 : Scheme.Cover _ _), rfl⟩ := hR
  use 𝒰.ulift, le_trans (fun Y g ⟨i⟩ ↦ .mk _) hle

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
    0
⊢ (u • P) y ^ 2 * (u • P) z + W'.a₁ * (u • P) x * (u • P) y * (u • P) z + W'.a₃ * (u • P) y * (u • P) z ^ 2 -
          ((u • P) x ^ 3 + W'.a₂ * (u • P) x ^ 2 * (u • P) z + W'.a₄ * (u • P) x * (u • P) z ^ 2 +
            W'.a₆ * (u • P) z ^ 3) +
        u ^ 3 * 0 -
      (0 +
        u ^ 3 *
          (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3))) =
    0

Tactic:
simp only [smul_fin3_ext]

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu : IsUnit u✝
u : R
P : Fin 3 → R
hP :
  P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
    0
⊢ (u * P y) ^ 2 * (u * P z) + W'.a₁ * (u * P x) * (u * P y) * (u * P z) + W'.a₃ * (u * P y) * (u * P z) ^ 2 -
          ((u * P x) ^ 3 + W'.a₂ * (u * P x) ^ 2 * (u * P z) + W'.a₄ * (u * P x) * (u * P z) ^ 2 +
            W'.a₆ * (u * P z) ^ 3) +
        u ^ 3 * 0 -
      (0 +
        u ^ 3 *
          (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u • P) y * (u • P) z - (3 * (u • P) x ^ 2 + 2 * W'.a₂ * (u • P) x * (u • P) z + W'.a₄ * (u • P) z ^ 2) = 0 ∧
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * (u • P) z ^ 2 = 0 ∧
      (u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * (u • P) x ^ 2 + 2 * W'.a₄ * (u • P) x * (u • P) z + 3 * W'.a₆ * (u • P) z ^ 2) =
        0

Tactic:
simp only [smul_fin3_ext]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P✝ : Fin 3 → R
u✝ : R
hu✝ : IsUnit u✝
u : R
hu : IsUnit u
P : Fin 3 → R
hP✝ : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2) = 0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2 = 0 ∧
      P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) - (3 * (u * P x) ^ 2 + 2 * W'.a₂ * (u * P x) * (u * P z) + W'.a₄ * (u * P z) ^ 2) = 0 ∧
    2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * (u * P z) ^ 2 = 0 ∧
      (u * P y) ^ 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * (u * P x) ^ 2 + 2 * W'.a₄ * (u * P x) * (u * P z) + 3 * W'.a₆ * (u * P z) ^ 2) =
        0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : W.Point
⊢ (-P).toAffineLift = -P.toAffineLift

Tactic:
rcases P with @⟨⟨_⟩, hP⟩
  exact toAffine_neg hP

Goal state after:
Module: Mathlib.AlgebraicGeometry.GluingOneHypercover

Goal state before:
pp: D : GlueData
i₁ i₂ : D.J
W : Scheme
p₁ : W ⟶ D.U i₁
p₂ : W ⟶ D.U i₂
fac : p₁ ≫ D.ι i₁ = p₂ ≫ D.ι i₂
T : Scheme
g : T ⟶ W
x✝ : ⊤.arrows g
⊢ (g ≫ p₁) ≫ D.ι i₁ = (g ≫ p₂) ≫ D.ι i₂

Tactic:
simpa using g ≫= fac

Goal state after:
Module: Mathlib.RingTheory.RingHom.Unramified

Goal state before:
pp: ⊢ PropertyIsLocal fun {R S} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
constructor
  · exact isStableUnderBaseChange.localizationPreserves.away
  · exact ofLocalizationSpanTarget
  · exact ofLocalizationSpanTarget.ofLocalizationSpan
      (stableUnderComposition.stableUnderCompositionWithLocalizationAway
          holdsForLocalizationAway).1
  · exact (stableUnderComposition.stableUnderCompositionWithLocalizationAway
        holdsForLocalizationAway).2

Goal state after:
Module: Mathlib.RingTheory.Smooth.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
A : I → Type u_3
inst✝³ : CommRing R
inst✝² : (i : I) → CommRing (A i)
inst✝¹ : (i : I) → Algebra R (A i)
inst✝ : Finite I
val✝ : Fintype I
H : ∀ (i : I), FormallySmooth R (A i)
B : Type (max u_1 u_2 u_3)
x✝¹ : CommRing B
x✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
g : ((i : I) → A i) →ₐ[R] B ⧸ J
hJ' : ∀ x ∈ RingHom.ker (Ideal.Quotient.mk J), IsNilpotent x
e : I → B
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), (Ideal.Quotient.mk J) (e i) = g (Pi.single i 1)
iso : B ≃ₐ[R] (i : I) → B ⧸ Ideal.span {1 - e i} :=
  let __spread.0 := AlgHom.pi fun i ↦ Ideal.Quotient.mkₐ R (Ideal.span {1 - e i});
  let __spread.1 := Equiv.ofBijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
J' : (i : I) → Ideal (B ⧸ Ideal.span {1 - e i}) := fun i ↦ Ideal.map (Ideal.Quotient.mk (Ideal.span {1 - e i})) J
ι : (i : I) → B ⧸ J →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  fun i ↦ Ideal.quotientMapₐ (J' i) (IsScalarTower.toAlgHom R B (B ⧸ Ideal.span {1 - e i})) ⋯
hι : ∀ (i : I) (x : B ⧸ J), (ι i) x = 0 → (Ideal.Quotient.mk J) (e i) * x = 0
i : I
g' : A i →ₐ[R] (B ⧸ Ideal.span {1 - e i}) ⧸ J' i :=
  AlgHom.ofLinearMap (((ι i).comp g).toLinearMap ∘ₗ LinearMap.single R A i) ⋯ ⋯
⊢ J' i ^ 2 = ⊥

Tactic:
rw [← Ideal.map_pow, hJ, Ideal.map_bot]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
this : f₁' = f₂'
c : B
hc : f₁ (Pi.single x (1 * g x)) - f₂ (Pi.single x (1 * g x)) = 0
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))

Tactic:
one_mul,

Goal state after:
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := Pi.single x 1
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := Ideal.span {1 - f₁ e}
f₁' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₁).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
f₂' : f x →ₐ[R] B ⧸ J' :=
  AlgHom.ofLinearMap (((Ideal.Quotient.mkₐ R J').comp f₂).toLinearMap ∘ₗ LinearMap.single R f x) ⋯ ⋯
this : f₁' = f₂'
c : B
hc : f₁ (Pi.single x (g x)) - f₂ (Pi.single x (g x)) = 0
⊢ f₁ (Pi.single x (g x)) = f₂ (Pi.single x (g x))
Module: Mathlib.RingTheory.Unramified.Pi

Goal state before:
pp: case intro.mpr.hI
R : Type u_1
I : Type u_2
inst✝⁵ : Finite I
f : I → Type u_3
inst✝⁴ : CommRing R
inst✝³ : (i : I) → CommRing (f i)
inst✝² : (i : I) → Algebra R (f i)
val✝ : Fintype I
H✝ : ∀ (i : I), FormallyUnramified R (f i)
B : Type (max u_2 u_3)
inst✝¹ : CommRing B
inst✝ : Algebra R B
J : Ideal B
hJ : J ^ 2 = ⊥
f₁ f₂ : ((i : I) → f i) →ₐ[R] B
e✝ : (Ideal.Quotient.mkₐ R J).comp f₁ = (Ideal.Quotient.mkₐ R J).comp f₂
g : (i : I) → f i
x : I
hf : ∀ (x : (i : I) → f i), f₁ x - f₂ x ∈ J
e : (i : I) → f i := ⋯
he : IsIdempotentElem e
h₁ : f₁ e * (1 - f₂ e) = 0
h₂ : f₂ e * (1 - f₁ e) = 0
H : f₁ e = f₂ e
J' : Ideal B := ⋯
f₁' : f x →ₐ[R] B ⧸ J' := ⋯
f₂' : f x →ₐ[R] B ⧸ J' := ⋯
⊢ Ideal.map (algebraMap B (B ⧸ J')) J ^ 2 = ⊥

Tactic:
rw [← Ideal.map_pow, hJ, Ideal.map_bot]

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

Goal state before:
pp: case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * s✝ • n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝) +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
mul_comm,

Goal state after:
case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝ * (algebraMap A B) z) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝) +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (n✝ * (algebraMap A B) z) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝) +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)

Tactic:
mul_comm,

Goal state after:
case tmul.smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
z : A
s✝ : S
n✝ : B
e :
  (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) n✝ +
      n✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
⊢ s✝ • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z * n✝) =
    (algebraMap A B) z • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) (s✝ • n✝) +
      (s✝ • n✝) • (⋯.lift ((mk R S Ω[A⁄R]) 1 ∘ₗ ↑(D R A))) ((algebraMap A B) z)
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : Algebra S B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : Algebra.IsPushout R S A B
a : A
this : Algebra.IsPushout R A S B
a' : A
s : S
⊢ s • a' • (D S B) ((algebraMap A B) a) = (Algebra.IsPushout.equiv R A S B) (a' ⊗ₜ[R] s) • (D S B) ((algebraMap A B) a)

Tactic:
· simp [Algebra.IsPushout.equiv_tmul, mul_smul, smul_comm]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: case refine_1
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
⊢ ∀ (n : ℕ), ↑(a n) ≡ ↑(a (n + 1)) [SMOD I ^ n • ⊤]

pp: case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
⊢ (map I f) ((mk I M) (AdicCauchySequence.mk I M (fun n ↦ ↑(a n)) ?refine_1)) = (mk I N) b

Tactic:
· refine fun n ↦ SModEq.symm ?_
    simp only [SModEq, mapPreimage, Submodule.Quotient.mk_sub,
      sub_eq_self, Submodule.Quotient.mk_eq_zero, SetLike.coe_mem, a]

Goal state after:
case refine_2
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → ↑(⇑f ⁻¹' {↑b n}) := mapPreimage hf b
⊢ (map I f) ((mk I M) (AdicCauchySequence.mk I M (fun n ↦ ↑(a n)) ⋯)) = (mk I N) b
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f) ∘ₗ eval I M n = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m

Tactic:
← comp_assoc,

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u_4
inst✝³ : AddCommGroup P
inst✝² : Module R P
T : Type u_5
inst✝¹ : AddCommGroup T
inst✝ : Module (AdicCompletion I R) T
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ (transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f)) ∘ₗ eval I M n = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ eval I M m
Module: Mathlib.RingTheory.AdicCompletion.Algebra

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ Submodule.Quotient.mk (↑r m • ↑x m) = ↑r m • Submodule.Quotient.mk (↑x m)

Tactic:
Submodule.Quotient.mk_smul

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ ↑r m • Submodule.Quotient.mk (↑x m) = ↑r m • Submodule.Quotient.mk (↑x m)
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r x : AdicCompletion I R
⊢ ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (r • x)) ∘ₗ of I M =
    (RingHom.id (AdicCompletion I R)) r • ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M

Tactic:
apply LinearMap.ext
        simp [mul_smul]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.AsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
r x : AdicCompletion I R
⊢ ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) (r • x)) ∘ₗ of I M =
    (RingHom.id (AdicCompletion I R)) r • ↑R ((LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M)) x) ∘ₗ of I M

Tactic:
by
        apply LinearMap.ext
        simp [mul_smul]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : PreSubmersivePresentation R S ι σ
inst✝ : Finite σ
⊢ IsUnit P.jacobian ↔ Function.Bijective ⇑P.aevalDifferential

Tactic:
rw [P.jacobian_eq_det_aevalDifferential, ← LinearMap.isUnit_iff_isUnit_det]
  exact Module.End.isUnit_iff P.aevalDifferential

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ Q.jacobian * (algebraMap S T) P.jacobian = P.jacobian • Q.jacobian

Tactic:
mul_comm,

Goal state after:
case intro.intro
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T ι' σ'
P : PreSubmersivePresentation R S ι σ
inst✝¹ : Finite σ
inst✝ : Finite σ'
val✝¹ : Fintype σ'
val✝ : Fintype σ
⊢ (algebraMap S T) P.jacobian * Q.jacobian = P.jacobian • Q.jacobian
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Function.Bijective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
refine ⟨?_, Submodule.projectionOnto_comp_surjective_of_exact hfg _ hmap⟩

Goal state after:
R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
p q : Submodule R M
hpq : IsCompl p q
hker : Disjoint g.ker q
hmap : map g q = ⊤
⊢ Function.Injective ⇑(p.projectionOnto q hpq ∘ₗ f)
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔
      (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1} ⊔
        Ideal.comap ((localizationAway T g).ofComp P).toAlgHom ⊥) =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}

Tactic:
← RingHom.ker_eq_comap_bot,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
f : P.Ring
h : (algebraMap P.Ring S) f = g
this :
  (localizationAway T g).ker =
    Ideal.map ((localizationAway T g).ofComp P).toAlgHom (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1})
⊢ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔
      (Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1} ⊔ RingHom.ker ((localizationAway T g).ofComp P).toAlgHom) =
    RingHom.ker ((localizationAway T g).ofComp P).toAlgHom ⊔ Ideal.span {(rename Sum.inr) f * X (Sum.inl ()) - 1}