awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
hNO : N ≤ O
rw : Submodule.map ϕ (Submodule.comap O.subtype N) = (ϕ ∘ₗ Submodule.inclusion hNO).range
rw₁ : Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.inclusion hNO).range
⊢ ϕ.submoduleImage N = (ϕ ∘ₗ Submodule.inclusion hNO).range
have rw₂ : Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.comap O.subtype N)
Tactic: rw [submoduleImage, range_comp, Submodule.range_inclusion]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
have rw : Eq (α := Submodule R₂ ↥f.range) (range f.rangeRestrict) ⊤
Tactic: rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
rw : Eq (α := Submodule R₂ ↥f.range) (range f.rangeRestrict) ⊤
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)
have rw₁ : Eq.{u_6 + 1} (α := Submodule R₂ ↥f.range) ⊤ ⊤
Tactic: rw [← range_eq_top, range_rangeRestrict]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
⊢ (f.restrict h).range = comap q.subtype (map f p)
have rw : map (f.restrict h) ⊤ = comap q.subtype (map f p)
Tactic: rw [← Submodule.map_top, map_restrict, Submodule.map_top, p.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
rw : map (f.restrict h) ⊤ = comap q.subtype (map f p)
⊢ (f.restrict h).range = comap q.subtype (map f p)
have rw₁ : comap q.subtype (map f (map p.subtype ⊤)) = comap q.subtype (map f p)
Tactic: rw [← Submodule.map_top, map_restrict, Submodule.map_top, p.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
rw : map (f.restrict h) ⊤ = comap q.subtype (map f p)
rw₁ : comap q.subtype (map f (map p.subtype ⊤)) = comap q.subtype (map f p)
⊢ (f.restrict h).range = comap q.subtype (map f p)
have rw₂ : comap q.subtype (map f p.subtype.range) = comap q.subtype (map f p)
Tactic: rw [← Submodule.map_top, map_restrict, Submodule.map_top, p.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
rw : map (f.restrict h) ⊤ = comap q.subtype (map f p)
rw₁ : comap q.subtype (map f (map p.subtype ⊤)) = comap q.subtype (map f p)
rw₂ : comap q.subtype (map f p.subtype.range) = comap q.subtype (map f p)
⊢ (f.restrict h).range = comap q.subtype (map f p)
have rw₃ : comap q.subtype (map f p) = comap q.subtype (map f p)
Tactic: rw [← Submodule.map_top, map_restrict, Submodule.map_top, p.range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.RestrictScalars (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s : Set (Submodule R M)
⊢ Eq (α := Submodule S M) (restrictScalars S (sInf s)) (sInf (restrictScalars S '' s))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule S M) (restrictScalars S (sInf s)) x ↔
    Membership.mem (γ := Submodule S M) (sInf (restrictScalars S '' s)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.RestrictScalars (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
ι : Sort u_4
s : ι → Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S (iInf s)) (⨅ (i : ι), restrictScalars S (s i))
have h : ∀ (x : M),
  Membership.mem (γ := Submodule S M) (restrictScalars S (iInf s)) x ↔
    Membership.mem (γ := Submodule S M) (⨅ (i : ι), restrictScalars S (s i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.RestrictScalars (goal)
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S (s ⊓ t)) (restrictScalars S s ⊓ restrictScalars S t)
have h : ∀ (x : M),
  Membership.mem (γ := Submodule S M) (restrictScalars S (s ⊓ t)) x ↔
    Membership.mem (γ := Submodule S M) (restrictScalars S s ⊓ restrictScalars S t) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), SSubset.{u_3} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
h₂ : (↑(insert j s).card : ℕ∞) < ENat.card K
⊢ SSubset.{u_3} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
have insert : ∀ (hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ),
  Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
Tactic: simp only [ssubset_univ_iff] at hj' ⊢
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : (↑(insert j s).card : ℕ∞) < ENat.card K
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
have insert : ∀ (hj : j ∉ ∅) (h₂ : (↑(Finset.card (α := ι) (insert j ∅)) : ℕ∞) < ENat.card K)
  (hj' :
    ∀ (h₂ : (↑(Finset.card.{u_1} (α := ι) ∅) : ℕ∞) < ENat.card K),
      Ne.{u_3 + 1} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)) univ),
  Ne.{u_3 + 1} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) (insert j ∅) i), (↑(p i) : Set M)) univ
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s, hj, h₂, hj'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : (↑(Insert.insert j s).card : ℕ∞) < ENat.card K
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
insert :
  ∀ (hj : j ∉ ∅) (h₂ : (↑(Finset.card (α := ι) (Insert.insert j ∅)) : ℕ∞) < ENat.card K)
    (hj' :
      ∀ (h₂ : (↑(Finset.card.{u_1} (α := ι) ∅) : ℕ∞) < ENat.card K),
        Ne.{u_3 + 1} (α := Set M) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), (↑(p i) : Set M)) univ),
    Ne.{u_3 + 1} (α := Set M)
      (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) (Insert.insert j ∅) i), (↑(p i) : Set M)) univ
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ
have insert₁ : ∀ (hs : s.Nonempty), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ Insert.insert j s, (↑(p i) : Set M)) univ
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
h₂ : (↑(insert j s).card : ℕ∞) < ENat.card K
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
hs : s.Nonempty
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
have h₃ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
Tactic: replace h₂ : s.card + 1 < ENat.card K := by simpa [Finset.card_insert_of_notMem hj] using h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hj' : ∀ (h₂ : (↑s.card : ℕ∞) < ENat.card K), Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
have hj'₁ : Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
Tactic: specialize hj' (lt_trans ENat.natCast_lt_succ h₂)
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
⊢ Ne.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
have insert : ∀ (hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ),
  Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
Tactic: contrapose hj'
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ insert j s, (↑(p i) : Set M)) univ
⊢ Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
have hj'₁ : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
Tactic: replace hj' : (p j : Set M) ∪ (⋃ i ∈ s, p i) = univ := by
      simpa only [Finset.mem_insert, iUnion_iUnion_eq_or_left] using hj'
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
this : (↑(p j) : Set M) ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
⊢ Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
have rwa : ∀ (hj' : Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ)
  (this : (↑(p j) : Set M) ⊆ ⋃ i ∈ s, (↑(p i) : Set M)), Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
Tactic: rwa [union_eq_right.mpr this] at hj'
Cleared hypotheses: hj', this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
⊢ Eq.{u_3 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) univ
have insert : (↑(p j) : Set M) ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
Tactic: suffices (p j : Set M) ⊆ ⋃ i ∈ s, p i by rwa [union_eq_right.mpr this] at hj'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
⊢ x ∈ (↑(p j) : Set M) → Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have insert : ∀ (hx : x ∈ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
Tactic: (hx : x ∈ p j)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have insert : ∀ (hx : 0 ∈ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) 0
Tactic: rcases eq_or_ne x 0 with rfl | hx₀
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
insert : ∀ (hx : 0 ∈ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) 0
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have insert₁ : ∀ (hx₀ : x ≠ 0), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
Tactic: rcases eq_or_ne x 0 with rfl | hx₀
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
⊢ ∃ (y : M), y ∉ p j
have h₃ : p j ≠ ⊤
Tactic: specialize h₁ j
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
h₁ : p j ≠ ⊤
⊢ ∃ (y : M), y ∉ p j
have contrapose! : ∀ (h₁ : ∀ (y : M), y ∈ p j), p j = ⊤
Tactic: contrapose! h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
h₁ : ∀ (y : M), y ∈ p j
⊢ p j = ⊤
have h : ∀ (x : M), x ∈ p j ↔ Membership.mem (γ := Submodule K M) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have insert : ∀ (y : M) (hy : y ∉ p j), Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
Tactic: obtain ⟨y, hy⟩ : ∃ y, y ∉ p j := by specialize h₁ j; contrapose! h₁; ext; simp [h₁]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have hy₀ : y ≠ 0
Tactic: have hy₀ : y ≠ 0 := by aesop
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
⊢ sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
have suffices : Disjoint sxy (↑(p j) : Set M)
Tactic: suffices Disjoint sxy (p j) from this.subset_right_of_subset_union <| hj' ▸ sxy.subset_univ
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
⊢ Disjoint sxy (↑(p j) : Set M)
have rw : sxy ∩ (↑(p j) : Set M) ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
t : K
ht₀ : t ≠ 0
ht : x + t • y ∈ p j
⊢ Membership.mem (γ := Set M) ∅ (x + t • y)
have ht₁ : y ∈ p j
Tactic: rw [(p j).add_mem_iff_right hx, (p j).smul_mem_iff ht₀] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
⊢ Membership.mem (γ := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) x
have hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
Tactic: have hsxy : sxy ⊆ ⋃ i ∈ s, p i := by
      suffices Disjoint sxy (p j) from this.subset_right_of_subset_union <| hj' ▸ sxy.subset_univ
      rw [Set.disjoint_iff]
      rintro - ⟨⟨t, ht₀, rfl⟩, ht : x + t • y ∈ p j⟩
      rw [(p j).add_mem_iff_right hx, (p j).smul_mem_iff ht₀] at ht
      contradiction
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
this : ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
⊢ ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k
have obtain : ∀ (k : ι) (hk : k ∈ s) (t₁ t₂ : K) (htne : x + t₁ • y ≠ x + t₂ • y) (ht₁ : x + t₁ • y ∈ p k) (ht₂ : x + t₂ • y ∈ p k),
  ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k
Tactic: obtain ⟨k, hk, -, ⟨t₁, -, rfl⟩, -, ⟨t₂, -, rfl⟩, htne, ht₁, ht₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
⊢ ∃ k ∈ s, ∃ (t₁ : K) (t₂ : K), t₁ ≠ t₂ ∧ x + t₁ • y ∈ p k ∧ x + t₂ • y ∈ p k
have suffices : ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
Tactic: suffices ∃ᵉ (k ∈ s) (z₁ ∈ sxy) (z₂ ∈ sxy), z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k by
        obtain ⟨k, hk, -, ⟨t₁, -, rfl⟩, -, ⟨t₂, -, rfl⟩, htne, ht₁, ht₂⟩ := this
        exact ⟨k, hk, t₁, t₂, by aesop, ht₁, ht₂⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Union (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
p : ι → Submodule K M
h₁ : ∀ (i : ι), p i ≠ ⊤
j : ι
s : Finset ι
hj : j ∉ s
hs : s.Nonempty
h₂ : HAdd.hAdd (α := ℕ∞) (↑s.card : ℕ∞) 1 < ENat.card K
hj' : (↑(p j) : Set M) ∪ ⋃ i ∈ s, (↑(p i) : Set M) = univ
x : M
hx : x ∈ p j
hx₀ : x ≠ 0
y : M
hy : y ∉ p j
hy₀ : y ≠ 0
sxy : Set M := {x_1 : M | ∃ (t : K) (_ : t ≠ 0), x + t • y = x_1}
hsxy : sxy ⊆ ⋃ i ∈ s, (↑(p i) : Set M)
⊢ ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
have choose : ∀ (f : (z : (↑sxy : Type u_3)) → ι)
  (hf : ∀ (z : (↑sxy : Type u_3)), Membership.mem (γ := Set M) (⋃ (_ : f z ∈ s), (↑(p (f z)) : Set M)) (↑z : M)),
  ∃ k ∈ s, ∃ z₁ ∈ sxy, ∃ z₂ ∈ sxy, z₁ ≠ z₂ ∧ z₁ ∈ p k ∧ z₂ ∈ p k
Tactic: choose f hf using fun z : sxy ↦ mem_iUnion.mp (hsxy z.property)