Theorem: φ_surjective (DividedPowers/DPAlgebra/RobyLemma9.lean)

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
⊢ Function.Surjective ⇑(φ R S M N)
Tactic:
intro z
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 ⊗[S] N
⊢ ∃ a, (φ R S M N) a = z

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 ⊗[S] N
⊢ ∃ a, (φ R S M N) a = z
Tactic:
induction z using TensorProduct.induction_on with
| zero => use 0; simp only [map_zero]
| tmul m n => use m ⊗ₜ n; simp only [φ_apply]
| add x y hx hy =>
    obtain ⟨a, rfl⟩ := hx
    obtain ⟨b, rfl⟩ := hy
    exact ⟨a + b, map_add _ _ _⟩
State after:
no goals

State before:
case 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
⊢ ∃ a, (φ R S M N) a = 0
Tactic:
use 0
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
⊢ (φ R S M N) 0 = 0

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]
State after:
no goals

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
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

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]
State after:
no goals

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
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

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
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

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 _ _ _⟩
State after:
no goals