mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case h.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
c : ↥I.primeCompl
g : N →ₗ[R] M
⊢ ↑R
        (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
              (LocalizedModule I.primeCompl N))
            ((LocalizedModule.map I.primeCompl) f))
          ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N =
    ↑R ((LocalizedModule.map I.primeCompl) (((llcomp R N M N) f) g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N

Tactic:
ext

Goal state after:
case h.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
c : ↥I.primeCompl
g : N →ₗ[R] M
x✝ : N
⊢ (↑R
          (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
                (LocalizedModule I.primeCompl N))
              ((LocalizedModule.map I.primeCompl) f))
            ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
        LocalizedModule.mkLinearMap I.primeCompl N)
      x✝ =
    (↑R ((LocalizedModule.map I.primeCompl) (((llcomp R N M N) f) g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N) x✝
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mpr.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
g : N →ₗ[R] M
s : ↥I.primeCompl
⊢ ↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N =
    ↑R
        (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
              (LocalizedModule I.primeCompl N))
            ((LocalizedModule.map I.primeCompl) f))
          ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
      LocalizedModule.mkLinearMap I.primeCompl N

Tactic:
ext

Goal state after:
case mpr.h
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f)).range
g : N →ₗ[R] M
s : ↥I.primeCompl
x✝ : N
⊢ (↑R ((LocalizedModule.map I.primeCompl) (f ∘ₗ g)) ∘ₗ LocalizedModule.mkLinearMap I.primeCompl N) x✝ =
    (↑R
          (((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
                (LocalizedModule I.primeCompl N))
              ((LocalizedModule.map I.primeCompl) f))
            ((LocalizedModule.map I.primeCompl) g)) ∘ₗ
        LocalizedModule.mkLinearMap I.primeCompl N)
      x✝
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R

case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ (fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {0} = U

Tactic:
ext

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ (fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {0} ↔ x✝ ∈ U
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ = U

Tactic:
ext

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ ↔ x✝ ∈ U
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ⇑(ofIsClopen hU) ⁻¹' {0} = U

Tactic:
ext

Goal state after:
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {0} ↔ x✝ ∈ U
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ⇑(ofIsClopen hU) ⁻¹' {1} = Uᶜ

Tactic:
ext

Goal state after:
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ⇑(ofIsClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ (fun x a ↦ (f a) x) ⁻¹' {g} = ⋂ a, ⇑(f a) ⁻¹' {g a}

Tactic:
ext

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
x✝ : X
⊢ x✝ ∈ (fun x a ↦ (f a) x) ⁻¹' {g} ↔ x✝ ∈ ⋂ a, ⇑(f a) ⁻¹' {g a}
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
⊢ comap f = fun g ↦ const X (g y)

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (comap f x✝¹) x✝ = (const X (x✝¹ y)) x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝ : LocallyConstant X Y
⊢ map (⇑e.symm) (map (⇑e) x✝) = x✝

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ (map (⇑e.symm) (map (⇑e) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝ : LocallyConstant X Z
⊢ map (⇑e) (map (⇑e.symm) x✝) = x✝

Tactic:
ext

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝¹ : LocallyConstant X Z
x✝ : X
⊢ (map (⇑e) (map (⇑e.symm) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x✝ : ⨁ (i : ι), N i
⊢ (directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ ⋯.equiv) (1 ⊗ₜ[R] x✝) = (lmap ε) x✝

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x✝ : ⨁ (i : ι), N i
i✝ : ι
⊢ ((directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ ⋯.equiv) (1 ⊗ₜ[R] x✝)) i✝ = ((lmap ε) x✝) i✝
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ (LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x) =
    (finsuppLEquivDirectSum S M' ι) (Finsupp.mapRange ⇑ε ⋯ x)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module S M'
inst✝ : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
i✝ : ι
⊢ ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ ⋯.equiv) (1 ⊗ₜ[R] x)) i✝ =
    ((finsuppLEquivDirectSum S M' ι) (Finsupp.mapRange ⇑ε ⋯ x)) i✝
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case e_f
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
⊢ algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl)) =
    (↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv).comp ↑includeRight

Tactic:
ext

Goal state after:
case e_f
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x✝ : Localization p.primeCompl
⊢ (algebraMap (Localization p.primeCompl) (Localization (algebraMapSubmonoid S p.primeCompl))) x✝ =
    ((↑(Localization.tensorLeftAlgEquiv p.primeCompl S).toRingEquiv).comp ↑includeRight) x✝
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (preimageEquivFiber R S p) q₁ ≤ (preimageEquivFiber R S p) q₂ ↔ q₁ ≤ q₂

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ (preimageEquivFiber R S p) q₁ ≤ (preimageEquivFiber R S p) q₂ → q₁ ≤ q₂

case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
⊢ q₁ ≤ q₂ → (preimageEquivFiber R S p) q₁ ≤ (preimageEquivFiber R S p) q₂
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G

Tactic:
let hG' : CommGroup G := { hG with mul_comm := h }
  cases hG
  infer_instance

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
⊢ ↑(leftCancelEquiv Q e) ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f) = f ∘ₗ ↑(leftCancelEquiv P e)

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((AlgebraTensorModule.curry
          ((AlgebraTensorModule.curry (↑(leftCancelEquiv Q e) ∘ₗ LinearMap.lTensor M (LinearMap.lTensor N f))) x✝²))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry ((AlgebraTensorModule.curry (f ∘ₗ ↑(leftCancelEquiv P e))) x✝²)) x✝¹) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
⊢ ↑(rightCancelEquiv Q e) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M f) = f ∘ₗ ↑(rightCancelEquiv P e)

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
f : P →ₗ[R] Q
x✝² : P
x✝¹ : M
x✝ : N
⊢ (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry (↑(rightCancelEquiv Q e) ∘ₗ LinearMap.rTensor N (LinearMap.rTensor M f))))
          x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (f ∘ₗ ↑(rightCancelEquiv P e)))) x✝²) x✝¹) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
x✝ : P →ₗ[R] Q
⊢ (rightCancelEquiv Q e).congrRight ((LinearMap.rTensorHom N) ((LinearMap.rTensorHom M) x✝)) =
    (LinearEquiv.congrLeft Q R (rightCancelEquiv P e)).symm x✝

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
e : M ⊗[R] N ≃ₗ[R] R
x✝³ : P →ₗ[R] Q
x✝² : P
x✝¹ : M
x✝ : N
⊢ (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              ((rightCancelEquiv Q e).congrRight ((LinearMap.rTensorHom N) ((LinearMap.rTensorHom M) x✝³)))))
          x✝²)
        x✝¹)
      x✝ =
    (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry ((LinearEquiv.congrLeft Q R (rightCancelEquiv P e)).symm x✝³)))
          x✝²)
        x✝¹)
      x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ ↑(LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight).symm ∘ₗ curry ↑e =
    rTensorHom N ∘ₗ ↑(ringLmapEquivSelf R R M).symm

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry
          ((↑(LinearEquiv.congrLeft (M ⊗[R] N) R (TensorProduct.lid R N) ≪≫ₗ e.congrRight).symm ∘ₗ curry ↑e) x✝¹))
        1)
      x✝ =
    ((AlgebraTensorModule.curry ((rTensorHom N ∘ₗ ↑(ringLmapEquivSelf R R M).symm) x✝¹)) 1) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
⊢ contractLeft R N ∘ₗ ↑(LinearEquiv.rTensor N (linearEquivDual e)) = ↑e

Tactic:
ext

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ⊗[R] N ≃ₗ[R] R
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (contractLeft R N ∘ₗ ↑(LinearEquiv.rTensor N (linearEquivDual e)))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ↑e) x✝¹) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Module.Finite R M ∧ Projective R M

Tactic:
let N := Dual R M

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
N : Type (max v u) := Dual R M
⊢ Module.Finite R M ∧ Projective R M
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ (∀ (x : K), (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x)).Splits) ∧
    normalClosure F K ↥(normalClosure F K L) = ⊤

Tactic:
constructor

Goal state after:
case left
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ ∀ (x : K), (Polynomial.map (algebraMap F ↥(normalClosure F K L)) (minpoly F x)).Splits

case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
⊢ normalClosure F K ↥(normalClosure F K L) = ⊤
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ ⇑(toModuleEnd R M) =
    ⇑(lid R M).conj ∘
      ⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) ∘
        ⇑(RingEquiv.moduleEndSelf R) ∘ ⇑MulOpposite.opEquiv

Tactic:
ext

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
x✝¹ : R
x✝ : M
⊢ ((toModuleEnd R M) x✝¹) x✝ =
    ((⇑(lid R M).conj ∘
          ⇑(rTensorEquiv R R (TensorProduct.comm R M (Dual R M) ≪≫ₗ linearEquiv R M)) ∘
            ⇑(RingEquiv.moduleEndSelf R) ∘ ⇑MulOpposite.opEquiv)
        x✝¹)
      x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
A : Type u_5
B : Type u_6
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
⊢ (mapAlgebra A B).comp (mapAlgebra R A) = mapAlgebra R B

Tactic:
ext

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
A : Type u_5
B : Type u_6
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
x✝ : Pic R
⊢ ((mapAlgebra A B).comp (mapAlgebra R A)) x✝ = (mapAlgebra R B) x✝
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ mapAlgebra R R = MonoidHom.id (Pic R)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : Pic R
⊢ (mapAlgebra R R) x✝ = (MonoidHom.id (Pic R)) x✝
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
⊢ aeval (⇑f ∘ x) = f.comp (aeval x)

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_3
A : Type u_5
A' : Type u_6
x : ι → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (⇑f ∘ x)
i✝ : ι
⊢ (aeval (⇑f ∘ x)) (X i✝) = (f.comp (aeval x)) (X i✝)
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M := ⋯
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M := ⋯
P : Ideal R
x✝ : P.IsMaximal
⊢ (IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(TensorProduct.comm R M M) ∘ₗ ff P =
    ↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) ∘ₗ ff P

Tactic:
ext

Goal state after:
case refine_1
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝² : P.IsMaximal
x✝¹ x✝ : M
⊢ ((AlgebraTensorModule.curry ((IsLocalizedModule.map P.primeCompl (ff P) (ff P)) ↑(TensorProduct.comm R M M) ∘ₗ ff P))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (↑(TensorProduct.comm R (LocalizedModule P.primeCompl M) (LocalizedModule P.primeCompl M)) ∘ₗ ff P))
        x✝¹)
      x✝