R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x : M
hx : x ∈ ⨆ (i : ι), p i
⊢ ∃ x_1, C x x_1
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x : M
hx : x ∈ ⨆ (i : ι), p i
⊢ C x hx
refine' Exists.elim _ fun (hx : x ∈ ⨆ i, p i) (hc : C x hx) => hc
case refine'_1
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝¹ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x✝ : M
hx✝ : x✝ ∈ ⨆ (i : ι), p i
i : ι
x : M
hx : x ∈ p i
⊢ (fun x => ∃ hx, C x hx) x

case refine'_2
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x : M
hx : x ∈ ⨆ (i : ι), p i
⊢ (fun x => ∃ hx, C x hx) 0

case refine'_3
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝¹ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), p i
x y : M
⊢ (fun x => ∃ hx, C x hx) x → (fun x => ∃ hx, C x hx) y → (fun x => ∃ hx, C x hx) (x + y)
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x : M
hx : x ∈ ⨆ (i : ι), p i
⊢ ∃ x_1, C x x_1
refine' iSup_induction p (C := fun x : M ↦ ∃ (hx : x ∈ ⨆ i, p i), C x hx) hx
  (fun i x hx => _) _ fun x y => _
no goals
case refine'_1
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝¹ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x✝ : M
hx✝ : x✝ ∈ ⨆ (i : ι), p i
i : ι
x : M
hx : x ∈ p i
⊢ (fun x => ∃ hx, C x hx) x
exact ⟨_, hp _ _ hx⟩
no goals
case refine'_2
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x : M
hx : x ∈ ⨆ (i : ι), p i
⊢ (fun x => ∃ hx, C x hx) 0
exact ⟨_, h0⟩
case refine'_3.intro.intro
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝¹ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), p i
x y : M
w✝¹ : x ∈ ⨆ (i : ι), p i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), p i
Cy : C y w✝
⊢ ∃ hx, C (x + y) hx
case refine'_3
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝¹ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), p i
x y : M
⊢ (fun x => ∃ hx, C x hx) x → (fun x => ∃ hx, C x hx) y → (fun x => ∃ hx, C x hx) (x + y)
rintro ⟨_, Cx⟩ ⟨_, Cy⟩
no goals
case refine'_3.intro.intro
R : Type u_2
R₂ : Type ?u.218812
K : Type ?u.218815
M : Type u_3
M₂ : Type ?u.218821
V : Type ?u.218824
S : Type ?u.218827
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x✝¹ : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
ι : Sort u_1
p : ι → Submodule R M
C : (x : M) → (x ∈ ⨆ (i : ι), p i) → Prop
hp : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x (_ : x ∈ ⨆ (i : ι), p i)
h0 : C 0 (_ : 0 ∈ ⨆ (i : ι), p i)
hadd :
  ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i),
    C x hx → C y hy → C (x + y) (_ : x + y ∈ ⨆ (i : ι), p i)
x✝ : M
hx : x✝ ∈ ⨆ (i : ι), p i
x y : M
w✝¹ : x ∈ ⨆ (i : ι), p i
Cx : C x w✝¹
w✝ : y ∈ ⨆ (i : ι), p i
Cy : C y w✝
⊢ ∃ hx, C (x + y) hx
refine' ⟨_, hadd _ _ _ _ Cx Cy⟩