awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
⊢ (↑(basicOpen s) : Set (PrimeSpectrum S)) = comap f ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum R))
have rw : (↑(basicOpen ((f : (a : R) → S) r) : TopologicalSpace.Opens (PrimeSpectrum S)) : Set (PrimeSpectrum S)) =
  comap f ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: rw [← basicOpen_pow _ n hn, ← hr]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
⊢ IsOpen (comap f '' (fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S))) s)
have this : comap f '' (↑(basicOpen s) : Set (PrimeSpectrum S)) = (↑(basicOpen r) : Set (PrimeSpectrum R))
Tactic: have : (comap f) '' (basicOpen s) = basicOpen r :=
    (Set.eq_preimage_iff_image_eq hbij).mp <| by rw [← basicOpen_pow _ n hn, ← hr]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ LE.le (α := Ideal R) (RingHom.ker (F := R →+* R ⊗[k] K) (algebraMap R (R ⊗[k] K))) (nilradical R)
have h : Eq (α := Ideal R) (RingHom.ker (F := R →+* R ⊗[k] K) (algebraMap R (R ⊗[k] K))) ⊥
Tactic: convert! bot_le
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ := ringExpChar k
h : Eq (α := Ideal R) (RingHom.ker (F := R →+* R ⊗[k] K) (algebraMap R (R ⊗[k] K))) ⊥
⊢ LE.le (α := Ideal R) (RingHom.ker (F := R →+* R ⊗[k] K) (algebraMap R (R ⊗[k] K))) (nilradical R)
have convert_3 : OrderBot (Ideal R)
Tactic: convert! bot_le
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
⊢ Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)
have h : ∀ (x : S),
  Eq (α := L ⊗[R] S)
    ((AlgHom.comp (B := K ⊗[R] S)
            (AlgHom.restrictScalars R
              (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S))
            Algebra.TensorProduct.includeRight :
          (a : S) → L ⊗[R] S)
        x :
      L ⊗[R] S)
    ((AlgHom.comp (B := K ⊗[R] S)
            (AlgHom.restrictScalars R
              (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp
                    (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
                (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))))
            Algebra.TensorProduct.includeRight :
          (a : S) → L ⊗[R] S)
        x :
      L ⊗[R] S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (hypothesis)
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
⊢ IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)))
have heq : Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
  (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
  (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
      (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
    K ⊗[R] S →ₐ[K] L ⊗[R] S)
Tactic: have heq : Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) =
      (e.symm.toAlgHom.comp e2.symm.toAlgHom).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) ((K ⊗[R] S) ⊗[K] L)) := by
    ext; simp [e, e2]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)
⊢ IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap (AlgHom.toRingHom (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)))
have rw : IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
  (comap
    (AlgHom.toRingHom
      (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)))))
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
Goal:
K : Type u_2
R : Type u_3
S : Type u_4
inst : Field K
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R K
inst_4 : Algebra R S
L : Type u_5
inst_5 : Field L
inst_6 : Algebra R L
inst_7 : Algebra K L
inst_8 : IsScalarTower R K L
inst_9 : IsPurelyInseparable K L
e : L ⊗[R] S ≃ₐ[K] L ⊗[K] (K ⊗[R] S) := AlgEquiv.symm (Algebra.TensorProduct.cancelBaseChange R K K L S)
e2 : L ⊗[K] (K ⊗[R] S) ≃ₐ[K] K ⊗[R] S ⊗[K] L := Algebra.TensorProduct.comm K L (K ⊗[R] S)
heq :
  Eq (α := K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (Algebra.TensorProduct.map (Algebra.ofId K L) (AlgHom.id R S) : K ⊗[R] S →ₐ[K] L ⊗[R] S)
    (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
        (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)) :
      K ⊗[R] S →ₐ[K] L ⊗[R] S)
⊢ IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
    (comap
      (AlgHom.toRingHom
        (((↑e.symm : L ⊗[K] (K ⊗[R] S) →ₐ[K] L ⊗[R] S).comp (↑e2.symm : K ⊗[R] S ⊗[K] L →ₐ[K] L ⊗[K] (K ⊗[R] S))).comp
          (IsScalarTower.toAlgHom K (K ⊗[R] S) (K ⊗[R] S ⊗[K] L)))))
have simp : IsHomeomorph (X := PrimeSpectrum (L ⊗[R] S)) (Y := PrimeSpectrum (K ⊗[R] S))
  (comap
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : L ⊗[K] (K ⊗[R] S) →+* L ⊗[R] S)
        (↑e2.symm : K ⊗[R] S ⊗[K] L →+* L ⊗[K] (K ⊗[R] S)))
      (algebraMap (K ⊗[R] S) (K ⊗[R] S ⊗[K] L))))
Tactic: simp only [AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom,
    AlgEquiv.toAlgHom_toRingHom, IsScalarTower.coe_toAlgHom, comap_comp]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
b : Basis ι R M
a : A
m : M
⊢ (basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a ⊗ₜ[R] m) =
    HSMul.hSMul (β := ι →₀ A) a (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) ⋯ ((b.repr : (a : M) → ι →₀ R) m))
have h : ∀ (a_1 : ι),
  Eq.{u_2 + 1} (α := A) ((((basisAux A b : (a : A ⊗[R] M) → ι →₀ A) (a ⊗ₜ[R] m) : ι →₀ A) : (a : ι) → A) a_1 : A)
    ((HSMul.hSMul (β := ι →₀ A) a
            (Finsupp.mapRange (⇑(algebraMap R A) : (a : R) → A) sorry ((b.repr : (a : M) → ι →₀ R) m)) :
          (a : ι) → A)
        a_1 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
⊢ Eq (α := A ⊗[R] N →ₗ[A] A ⊗[R] M) (baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij))
    ((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij)
have apply : ∀ (i : ι'),
  Eq (α := A ⊗[R] M)
    ((baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij) : (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) i) :
      A ⊗[R] M)
    ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
            A ⊗[R] N →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) i) :
      A ⊗[R] M)
Tactic: apply (basis A b').ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
| ((baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij) : (a : A ⊗[R] N) → A ⊗[R] M)
      ((basis A b' : (a : ι') → A ⊗[R] N) k) :
    A ⊗[R] M)
have simp : (1 ⊗ₜ[R] (((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij : N →ₗ[R] M) : (a : N) → M) ((b' : (a : ι') → N) k : N) :
  A ⊗[R] M)
Tactic: simp only [basis_apply, baseChange_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ Eq (α := A ⊗[R] M)
    ((baseChange A ((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij) : (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)
    ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
            A ⊗[R] N →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)
have conv_lhs : Eq (α := A ⊗[R] M)
  (1 ⊗ₜ[R] (((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij : N →ₗ[R] M) : (a : N) → M) ((b' : (a : ι') → N) k : N) :
    A ⊗[R] M)
  ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij : A ⊗[R] N →ₗ[A] A ⊗[R] M) :
        (a : A ⊗[R] N) → A ⊗[R] M)
      ((basis A b' : (a : ι') → A ⊗[R] N) k) :
    A ⊗[R] M)
Tactic: conv_lhs => simp only [basis_apply, baseChange_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ Eq (α := A ⊗[R] M)
    (1 ⊗ₜ[R] (((b'.linearMap b : (a : ι × ι') → N →ₗ[R] M) ij : N →ₗ[R] M) : (a : N) → M) ((b' : (a : ι') → N) k : N) :
      A ⊗[R] M)
    ((((Basis.linearMap (basis A b') (basis A b) : (a : ι × ι') → A ⊗[R] N →ₗ[A] A ⊗[R] M) ij :
            A ⊗[R] N →ₗ[A] A ⊗[R] M) :
          (a : A ⊗[R] N) → A ⊗[R] M)
        ((basis A b' : (a : ι') → A ⊗[R] N) k) :
      A ⊗[R] M)
have simp_rw : Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] if ij.2 = k then (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
  (if ij.2 = k then 1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
Tactic: simp_rw [Basis.linearMap_apply_apply, basis_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] if ij.2 = k then (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
    (if ij.2 = k then 1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
have isTrue : ij.2 = k → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M)
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
ι' : Type u_3
N : Type u_4
inst_4 : Fintype ι'
inst_5 : DecidableEq ι'
inst_6 : AddCommMonoid N
inst_7 : Module R N
A : Type u_5
inst_8 : CommSemiring A
inst_9 : Algebra R A
b : Basis ι R M
b' : Basis ι' R N
ij : ι × ι'
k : ι'
isTrue :
  ij.2 = k → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M) (1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 : A ⊗[R] M)
⊢ Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] if ij.2 = k then (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
    (if ij.2 = k then 1 ⊗ₜ[R] (b : (a : ι) → M) ij.1 else 0 : A ⊗[R] M)
have isFalse : ¬ij.2 = k → Eq (α := A ⊗[R] M) (1 ⊗ₜ[R] 0) 0
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Free (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst : Fintype ι
inst_1 : Finite ι₂
inst_2 : DecidableEq ι
inst_3 : CommSemiring R
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : AddCommMonoid M₁
inst_7 : Module R M₁
inst_8 : AddCommMonoid M₂
inst_9 : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
⊢ Eq (α := Matrix ι₂ ι A)
    ((toMatrix (basis A b₁) (basis A b₂) : (a : A ⊗[R] M₁ →ₗ[A] A ⊗[R] M₂) → Matrix ι₂ ι A) (baseChange A f) :
      Matrix ι₂ ι A)
    (Matrix.map.{u_1, u_6, u_5, u_4} (α := R) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι R) f)
        (⇑(algebraMap R A) : (a : R) → A) :
      Matrix ι₂ ι A)
have a : ∀ (i : ι₂) (j : ι),
  Eq.{u_6 + 1} (α := A)
    ((toMatrix (basis A b₁) (basis A b₂) : (a : A ⊗[R] M₁ →ₗ[A] A ⊗[R] M₂) → Matrix ι₂ ι A) (baseChange A f) i j : A)
    (Matrix.map.{u_1, u_6, u_5, u_4} (α := R) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι R) f)
        (⇑(algebraMap R A) : (a : R) → A) i j :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
⊢ (↑(f.lift h) : OneHom B Γ).toFun 0 = 0
have h₁ : Eq.{u_3 + 1} (α := B) (0 : B) ((f : (a : A) → B) 0 : B)
Tactic: convert! f.lift_eq (P := Γ) _ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
h₁ : Eq.{u_3 + 1} (α := B) (0 : B) ((f : (a : A) → B) 0 : B)
⊢ (↑(f.lift h) : OneHom B Γ).toFun 0 = 0
have h₂ : Eq.{u_2 + 1} (α := Γ) (0 : Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) 0 : Γ)
Tactic: convert! f.lift_eq (P := Γ) _ 0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
x y : B
⊢ ∃ (a : A) (b : A) (s : ↥S), f.mk' a s = x ∧ f.mk' b s = y
have obtain : ∀ (a : A) (s : ↥S), ∃ (a_1 : A) (b : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b s_1 = y
Tactic: obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
y : B
a : A
s : ↥S
⊢ ∃ (a_1 : A) (b : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b s_1 = y
have obtain : ∀ (b : A) (t : ↥S), ∃ (a_1 : A) (b_1 : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b_1 s_1 = f.mk' b t
Tactic: obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ ∃ (a_1 : A) (b_1 : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b_1 s_1 = f.mk' b t
have h₁ : f.mk' (a * (↑t : A)) (s * t) = f.mk' a s ∧ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
Tactic: use a * t, b * s, s * t
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ f.mk' (a * (↑t : A)) (s * t) = f.mk' a s ∧ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
have h₁ : f.mk' (a * (↑t : A)) (s * t) = f.mk' a s
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a : A
s : ↥S
b : A
t : ↥S
h₁ : f.mk' (a * (↑t : A)) (s * t) = f.mk' a s
⊢ f.mk' (a * (↑t : A)) (s * t) = f.mk' a s ∧ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
have h₂ : f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ f.mk' (a * (↑t : A)) (s * t) = f.mk' a s
have h₁ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) ((↑s : A) * (a * (↑t : A))) : B)
  ((f : (a : A) → B) ((↑s : A) * (↑t : A) * a) : B)
Tactic: rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a : A
s : ↥S
b : A
t : ↥S
⊢ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
have h₁ : Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) ((↑t : A) * (b * (↑s : A))) : B)
  ((f : (a : A) → B) ((↑s : A) * (↑t : A) * b) : B)
Tactic: rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
x y : B
⊢ (↑(f.lift h) : OneHom B Γ).toFun (x + y) ≤
    max ((↑(f.lift h) : OneHom B Γ).toFun x) ((↑(f.lift h) : OneHom B Γ).toFun y)
have obtain : ∀ (a b : A) (s : ↥S),
  (↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s + f.mk' b s) ≤
    max ((↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s)) ((↑(f.lift h) : OneHom B Γ).toFun (f.mk' b s))
Tactic: obtain ⟨a, b, s, rfl, rfl⟩ : ∃ (a b : A) (s : S), f.mk' a s = x ∧ f.mk' b s = y := by
        obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
        obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
        use a * t, b * s, s * t
        constructor <;>
          · rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
            ring_nf
Cleared hypotheses: x, y