mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), toLinearMap✝¹ (a * b) = a • toLinearMap✝¹ b + b • toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), toLinearMap✝¹ (a * b) = a • toLinearMap✝¹ b + b • toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), toLinearMap✝¹ (a * b) = a • toLinearMap✝¹ b + b • toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝

Tactic:
;

Goal state after:
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring A
inst✝⁶ : CommSemiring B
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), toLinearMap✝¹ (a * b) = a • toLinearMap✝¹ b + b • toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), toLinearMap✝ (a * b) = a • toLinearMap✝ b + b • toLinearMap✝ a
h :
  (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D ↦ D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
Module: Mathlib.Tactic.Peel

Goal state before:
pp: α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x✝ : α
⊢ p x✝ ↔ q x✝

Tactic:
;

Goal state after:
α : Type u_1
p q : α → Prop
f : Filter α
hq : ∀ (x : α), p x ↔ q x
x✝ : α
⊢ p x✝ ↔ q x✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Set.range (comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}

Tactic:
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range (comap (algebraMap R S)) → x ∈ {p | Disjoint ↑M ↑p.asIdeal}

case refine_2
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ x ∈ Set.range (comap (algebraMap R S))
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D₁ D₂ : Derivation R A M
a✝ : A
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(D₁ + D₂);
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝ =
    ((let __LinearMap := ↑R f ∘ₗ ↑D₁;
        { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) +
        let __LinearMap := ↑R f ∘ₗ ↑D₂;
        { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D₁ D₂ : Derivation R A M
a✝ : A
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(D₁ + D₂);
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝ =
    ((let __LinearMap := ↑R f ∘ₗ ↑D₁;
        { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) +
        let __LinearMap := ↑R f ∘ₗ ↑D₂;
        { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a✝ : A
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(r • D);
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝ =
    ((RingHom.id A) r •
        let __LinearMap := ↑R f ∘ₗ ↑D;
        { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a✝ : A
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(r • D);
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝ =
    ((RingHom.id A) r •
        let __LinearMap := ↑R f ∘ₗ ↑D;
        { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ })
      a✝
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a✝ : A
⊢ f (r • D a✝) = r • f (D a✝)

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a✝ : A
⊢ f (r • D a✝) = r • f (D a✝)
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
f₁ f₂ : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ((f₁ + f₂).compDer x✝) a✝ = ((f₁.compDer + f₂.compDer) x✝) a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
f₁ f₂ : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ((f₁ + f₂).compDer x✝) a✝ = ((f₁.compDer + f₂.compDer) x✝) a✝
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ((r • D).compDer x✝) a✝ = (((RingHom.id A) r • D.compDer) x✝) a✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ((r • D).compDer x✝) a✝ = (((RingHom.id A) r • D.compDer) x✝) a✝
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal ↔ x✝ ∈ (comap (RingHom.fst R S) x).asIdeal

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum R
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inl x)).asIdeal ↔ x✝ ∈ (comap (RingHom.fst R S) x).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal ↔ x✝ ∈ (comap (RingHom.snd R S) x).asIdeal

Tactic:
;

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : PrimeSpectrum S
x✝ : R × S
⊢ x✝ ∈ ((primeSpectrumProd R S).symm (Sum.inr x)).asIdeal ↔ x✝ ∈ (comap (RingHom.snd R S) x).asIdeal
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
a : A
⊢ ((↑e.symm).compDer ((↑e).compDer.toFun D)) a = D a

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
a : A
⊢ ((↑e.symm).compDer ((↑e).compDer.toFun D)) a = D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : PrimeSpectrum R
⊢ comap (RingHom.fst R S) I ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))

Tactic:
;

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : PrimeSpectrum R
⊢ comap (RingHom.fst R S) I ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A N
a : A
⊢ ((↑e).compDer.toFun ((↑e.symm).compDer D)) a = D a

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A N
a : A
⊢ ((↑e).compDer.toFun ((↑e.symm).compDer D)) a = D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : PrimeSpectrum S
⊢ comap (RingHom.snd R S) I ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))

Tactic:
;

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
I : PrimeSpectrum S
⊢ comap (RingHom.snd R S) I ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h.h
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
n✝ : ℕ
p✝ : 0 < n✝
this : ∀ (g : G), g ^ n✝ = 1
⊢ g ^ n✝ = 1

Tactic:
;

Goal state after:
case h.h
G : Type u
inst✝ : Monoid G
h : ExponentExists G
g : G
n✝ : ℕ
p✝ : 0 < n✝
this : ∀ (g : G), g ^ n✝ = 1
⊢ g ^ n✝ = 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
x✝ : (i : ι) → R i
⊢ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal ↔ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal

Tactic:
;

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
q : PrimeSpectrum (R i)
hp : comap (Pi.evalRingHom R i) q ∈ ↑(basicOpen (Pi.single i f))
x✝ : (i : ι) → R i
⊢ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal ↔ x✝ ∈ (comap (Pi.evalRingHom R i) q).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (↑a) (Localization.Away ↑a)

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
a : ↑(Set.range f)
⊢ IsLocalization.Away (↑a) (Localization.Away ↑a)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case negSucc
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x ↦ g ^ x) (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ (g ^ k.succ)⁻¹ ∈ H

Tactic:
;

Goal state after:
case negSucc
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx : ∃ x ∈ H, x ≠ 1
x : α
hx₁ : x ∈ H
hx₂ : x ≠ 1
k : ℕ
hk✝ : (fun x ↦ g ^ x) (Int.negSucc k) = x
hk : g ^ Int.negSucc k = x
⊢ (g ^ k.succ)⁻¹ ∈ H
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

pp: case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

pp: case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x

Tactic:
;

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) *
      orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) =
    (orderOf x).lcm (orderOf y)

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
⊢ x ∈ H

Tactic:
;

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
⊢ x ∈ H
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)

pp: case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf y ≠ 0

pp: case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y

pp: case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

pp: case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x

Tactic:
;

Goal state after:
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) =
    (orderOf x).lcm (orderOf y)

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf y ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y

case hx
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ orderOf x ≠ 0

case hn
G : Type u
inst✝ : Monoid G
x y : G
h : Commute x y
hx : orderOf x ≠ 0
hy : orderOf y ≠ 0
⊢ (orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x