Theorem: DirectSum.lmap'_surjective (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ Surjective ⇑(lmap' f)
Tactic:
intro c
State after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
c : ⨁ (i : ι), γ i
⊢ ∃ a, (lmap' f) a = c

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
c : ⨁ (i : ι), γ i
⊢ ∃ a, (lmap' f) a = c
Tactic:
induction' c using DirectSum.induction_on with i xi x y hx hy
State after:
case H_zero
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ ∃ a, (lmap' f) a = 0

case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y

State before:
case H_zero
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ ∃ a, (lmap' f) a = 0

case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
. exact ⟨0, map_zero _⟩
State after:
case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y

State before:
case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi

case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
. use of _ i (h i xi).choose
  rw [← lof_eq_of R, lmap'_lof, lof_eq_of, (h i xi).choose_spec]
State after:
case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y

State before:
case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
. obtain ⟨a, ha, rfl⟩ := hx
  obtain ⟨b, hb, rfl⟩ := hy
  exact ⟨a + b, map_add _ _ _⟩
State after:
no goals

State before:
case H_zero
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
⊢ ∃ a, (lmap' f) a = 0
Tactic:
exact ⟨0, map_zero _⟩
State after:
no goals

State before:
case H_basic
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ ∃ a, (lmap' f) a = (of (fun i => γ i) i) xi
Tactic:
use of _ i (h i xi).choose
State after:
case h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ (lmap' f) ((of (fun i => β i) i) ⋯.choose) = (of (fun i => γ i) i) xi

State before:
case h
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
i : ι
xi : γ i
⊢ (lmap' f) ((of (fun i => β i) i) ⋯.choose) = (of (fun i => γ i) i) xi
Tactic:
rw [← lof_eq_of R, lmap'_lof, lof_eq_of, (h i xi).choose_spec]
State after:
no goals

State before:
case H_plus
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
x y : ⨁ (i : ι), γ i
hx : ∃ a, (lmap' f) a = x
hy : ∃ a, (lmap' f) a = y
⊢ ∃ a, (lmap' f) a = x + y
Tactic:
obtain ⟨a, ha, rfl⟩ := hx
State after:
case H_plus.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
y : ⨁ (i : ι), γ i
hy : ∃ a, (lmap' f) a = y
a : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + y

State before:
case H_plus.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
y : ⨁ (i : ι), γ i
hy : ∃ a, (lmap' f) a = y
a : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + y
Tactic:
obtain ⟨b, hb, rfl⟩ := hy
State after:
case H_plus.intro.refl.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
a b : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + (lmap' f) b

State before:
case H_plus.intro.refl.intro.refl
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → AddCommMonoid (γ i)
inst✝ : (i : ι) → Module R (γ i)
f : (i : ι) → β i →ₗ[R] γ i
h : ∀ (i : ι), Surjective ⇑(f i)
a b : ⨁ (i : ι), β i
⊢ ∃ a_1, (lmap' f) a_1 = (lmap' f) a + (lmap' f) b
Tactic:
exact ⟨a + b, map_add _ _ _⟩
State after:
no goals