internlm/Lean-Github huggingface dataset:
Theorem: φ_surjective
Proof state before:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ (φ R S M N) 0 = 0
Tactic:
simp only [map_zero]
Proof state after:
no goals
Theorem: φ_surjective
Proof state before:
case tmul
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ ∃ a, (φ R S M N) a = m ⊗ₜ[S] n
Tactic:
use m ⊗ₜ n
Proof state after:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (φ R S M N) (m ⊗ₜ[R] n) = m ⊗ₜ[S] n
Theorem: φ_surjective
Proof state before:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (φ R S M N) (m ⊗ₜ[R] n) = m ⊗ₜ[S] n
Tactic:
simp only [φ_apply]
Proof state after:
no goals
Theorem: φ_surjective
Proof state before:
case add
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
x y : M ⊗[S] N
hx : ∃ a, (φ R S M N) a = x
hy : ∃ a, (φ R S M N) a = y
⊢ ∃ a, (φ R S M N) a = x + y
Tactic:
obtain ⟨a, rfl⟩ := hx
Proof state after:
case add.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
y : M ⊗[S] N
hy : ∃ a, (φ R S M N) a = y
a : M ⊗[R] N
⊢ ∃ a_1, (φ R S M N) a_1 = (φ R S M N) a + y
Theorem: φ_surjective
Proof state before:
case add.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
y : M ⊗[S] N
hy : ∃ a, (φ R S M N) a = y
a : M ⊗[R] N
⊢ ∃ a_1, (φ R S M N) a_1 = (φ R S M N) a + y
Tactic:
obtain ⟨b, rfl⟩ := hy
Proof state after:
case add.intro.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
a b : M ⊗[R] N
⊢ ∃ a_1, (φ R S M N) a_1 = (φ R S M N) a + (φ R S M N) b
Theorem: φ_surjective
Proof state before:
case add.intro.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
a b : M ⊗[R] N
⊢ ∃ a_1, (φ R S M N) a_1 = (φ R S M N) a + (φ R S M N) b
Tactic:
exact ⟨a + b, map_add _ _ _⟩
Proof state after:
no goals
Theorem: ψ_apply
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (ψ R S M N) (m ⊗ₜ[S] n) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
simp only [ψ, ψLeft, ψRight, AlgHom.toRingHom_eq_coe, productMap_apply_tmul, AlgHom.coe_mk,
  RingHom.coe_coe, AlgHom.coe_comp, AlgHom.coe_restrictScalars', Ideal.Quotient.mkₐ_eq_mk,
  Function.comp_apply, includeLeft_apply, includeRight_apply]
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1) * (Ideal.Quotient.mk (kerφ R S M N)) (1 ⊗ₜ[R] n) =
    (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Theorem: ψ_apply
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1) * (Ideal.Quotient.mk (kerφ R S M N)) (1 ⊗ₜ[R] n) =
    (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
rw [← RingHom.map_mul]
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Theorem: ψ_apply
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
m : M
n : N
⊢ (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
simp only [tmul_mul_tmul, _root_.mul_one, _root_.one_mul]
Proof state after:
no goals
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ RingHom.ker (φ R S M N).toRingHom = kerφ R S M N
Tactic:
suffices h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom by
  rw [RingHom.ker_eq_ideal_iff]
  use h
  apply Function.HasLeftInverse.injective
  use ψ R S M N
  intro z
  obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective z
  simp only [AlgHom.toRingHom_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom]
  induction y using TensorProduct.induction_on with
  | zero => simp only [RingHom.map_zero, AlgHom.map_zero]
  | tmul m n => simp only [ψ_apply, φ_apply]
  | add x y hx hy =>
    simp only [RingHom.map_add, AlgHom.map_add, ← Ideal.Quotient.mkₐ_eq_mk, hx, hy]
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
Tactic:
simp only [kerφ]
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ Ideal.span ((fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤) ≤ RingHom.ker (φ R S M N).toRingHom
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ Ideal.span ((fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤) ≤ RingHom.ker (φ R S M N).toRingHom
Tactic:
rw [Ideal.span_le]
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤ ⊆ ↑(RingHom.ker (φ R S M N).toRingHom)
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
⊢ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤ ⊆ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
intro z hz
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
z : M ⊗[R] N
hz : z ∈ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
z : M ⊗[R] N
hz : z ∈ (fun r => (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1)) '' ⊤
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
simp only [Set.top_eq_univ, Set.image_univ, Set.mem_range] at hz
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
z : M ⊗[R] N
hz : ∃ y, (y • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (y • 1) = z
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
z : M ⊗[R] N
hz : ∃ y, (y • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (y • 1) = z
⊢ z ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
obtain ⟨r, rfl⟩ := hz
Proof state after:
case intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
r : S
⊢ (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1) ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Theorem: kerφ_eq
Proof state before:
case intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
r : S
⊢ (r • 1) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (r • 1) ∈ ↑(RingHom.ker (φ R S M N).toRingHom)
Tactic:
simp only [SetLike.mem_coe, RingHom.sub_mem_ker_iff,AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
  φ_apply, TensorProduct.tmul_smul]
Proof state after:
case intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
r : S
⊢ (r • 1) ⊗ₜ[S] 1 = r • 1 ⊗ₜ[S] 1
Theorem: kerφ_eq
Proof state before:
case intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
r : S
⊢ (r • 1) ⊗ₜ[S] 1 = r • 1 ⊗ₜ[S] 1
Tactic:
rfl
Proof state after:
no goals
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ RingHom.ker (φ R S M N).toRingHom = kerφ R S M N
Tactic:
rw [RingHom.ker_eq_ideal_iff]
Proof state after:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ ∃ (h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom),
    Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Theorem: kerφ_eq
Proof state before:
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ ∃ (h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom),
    Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
use h
Proof state after:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Theorem: kerφ_eq
Proof state before:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.Injective ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
apply Function.HasLeftInverse.injective
Proof state after:
case h.a
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.HasLeftInverse ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Theorem: kerφ_eq
Proof state before:
case h.a
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.HasLeftInverse ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
use ψ R S M N
Proof state after:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.LeftInverse ⇑(ψ R S M N) ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Theorem: kerφ_eq
Proof state before:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ Function.LeftInverse ⇑(ψ R S M N) ⇑(Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h)
Tactic:
intro z
Proof state after:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
z : M ⊗[R] N ⧸ kerφ R S M N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) z) = z
Theorem: kerφ_eq
Proof state before:
case h
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
z : M ⊗[R] N ⧸ kerφ R S M N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) z) = z
Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective z
Proof state after:
case h.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) ((Ideal.Quotient.mk (kerφ R S M N)) y)) =
    (Ideal.Quotient.mk (kerφ R S M N)) y
Theorem: kerφ_eq
Proof state before:
case h.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((Ideal.Quotient.lift (kerφ R S M N) (φ R S M N).toRingHom h) ((Ideal.Quotient.mk (kerφ R S M N)) y)) =
    (Ideal.Quotient.mk (kerφ R S M N)) y
Tactic:
simp only [AlgHom.toRingHom_eq_coe, Ideal.Quotient.lift_mk, AlgHom.coe_toRingHom]
Proof state after:
case h.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((φ R S M N) y) = (Ideal.Quotient.mk (kerφ R S M N)) y
Theorem: kerφ_eq
Proof state before:
case h.intro
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
y : M ⊗[R] N
⊢ (ψ R S M N) ((φ R S M N) y) = (Ideal.Quotient.mk (kerφ R S M N)) y
Tactic:
induction y using TensorProduct.induction_on with
| zero => simp only [RingHom.map_zero, AlgHom.map_zero]
| tmul m n => simp only [ψ_apply, φ_apply]
| add x y hx hy =>
  simp only [RingHom.map_add, AlgHom.map_add, ← Ideal.Quotient.mkₐ_eq_mk, hx, hy]
Proof state after:
no goals
Theorem: kerφ_eq
Proof state before:
case h.intro.zero
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
⊢ (ψ R S M N) ((φ R S M N) 0) = (Ideal.Quotient.mk (kerφ R S M N)) 0
Tactic:
simp only [RingHom.map_zero, AlgHom.map_zero]
Proof state after:
no goals
Theorem: kerφ_eq
Proof state before:
case h.intro.tmul
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
m : M
n : N
⊢ (ψ R S M N) ((φ R S M N) (m ⊗ₜ[R] n)) = (Ideal.Quotient.mk (kerφ R S M N)) (m ⊗ₜ[R] n)
Tactic:
simp only [ψ_apply, φ_apply]
Proof state after:
no goals
Theorem: kerφ_eq
Proof state before:
case h.intro.add
R : Type u_3
inst✝¹⁰ : CommRing R
S : Type u_4
inst✝⁹ : CommRing S
M : Type u_1
inst✝⁸ : CommRing M
inst✝⁷ : Algebra R M
inst✝⁶ : Algebra S M
N : Type u_2
inst✝⁵ : CommRing N
inst✝⁴ : Algebra R N
inst✝³ : Algebra S N
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R S M
inst✝ : IsScalarTower R S N
h : kerφ R S M N ≤ RingHom.ker (φ R S M N).toRingHom
x y : M ⊗[R] N
hx : (ψ R S M N) ((φ R S M N) x) = (Ideal.Quotient.mk (kerφ R S M N)) x
hy : (ψ R S M N) ((φ R S M N) y) = (Ideal.Quotient.mk (kerφ R S M N)) y
⊢ (ψ R S M N) ((φ R S M N) (x + y)) = (Ideal.Quotient.mk (kerφ R S M N)) (x + y)
Tactic:
simp only [RingHom.map_add, AlgHom.map_add, ← Ideal.Quotient.mkₐ_eq_mk, hx, hy]
Proof state after:
no goals
Theorem: MvPolynomial.degree_eq_weightedDegree
Proof state before:
σ : Type u_1
τ : Type ?u.203
R : Type ?u.206
inst✝ : CommSemiring R
S : Type ?u.212
d : σ →₀ ℕ
⊢ degree d = ∑ i ∈ d.support, d i
Tactic:
simp [degree, weightedDegree, Finsupp.total, Finsupp.sum]
Proof state after:
no goals
Theorem: MvPolynomial.totalDegree_eq_weightedTotalDegree
Proof state before:
σ : Type u_2
τ : Type ?u.7209
R : Type u_1
inst✝ : CommSemiring R
S : Type ?u.7218
φ : MvPolynomial σ R
⊢ φ.totalDegree = weightedTotalDegree 1 φ
Tactic:
simp only [totalDegree, weightedTotalDegree, weightedDegree, LinearMap.toAddMonoidHom_coe,
  Finsupp.total, Pi.one_apply, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
  id_eq, Algebra.id.smul_eq_mul, mul_one]
Proof state after:
no goals