-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.span_iff_products [WellFoundedLT I] :
    ⊤ ≤ Submodule.span ℤ (Set.range (eval C)) ↔
      ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

Proof state:
case intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
suffices L l by assumption

Result:
case intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
⊢ L l

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
⊢ L l

Tactic:
suffices Products.eval C '' {m | m < l} ⊆ span ℤ (Set.range (GoodProducts.eval C)) by
  rw [← span_le] at this
  exact this hl

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
⊢ Products.eval C '' {m | m < l} ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))

Proof state:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ L l

Tactic:
apply subset_span

Result:
case pos.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ Products.eval C l ∈ Set.range (eval C)

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
⊢ Products.eval C '' {m | m < l} ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
rintro a ⟨m, hm, rfl⟩

Result:
case neg.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
m : Products I
hm : m ∈ {m | m < l}
⊢ Products.eval C m ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
⊢ Submodule.span ℤ (Set.range (Products.eval C)) ≤ Submodule.span ℤ (Set.range (eval C))

Tactic:
rw [span_le]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
⊢ Set.range (Products.eval C) ⊆ ↑(Submodule.span ℤ (Set.range (eval C)))

Proof state:
case intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
let L : Products I → Prop := fun m ↦ m.eval C ∈ span ℤ (Set.range (GoodProducts.eval C))

Result:
case intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : ¬Products.isGood C l
⊢ L l

Tactic:
simp only [Products.isGood, not_not] at hl

Result:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
⊢ L l

Proof state:
case neg.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
m : Products I
hm : m ∈ {m | m < l}
⊢ Products.eval C m ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
exact h m hm

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})
this : Submodule.span ℤ (Products.eval C '' {m | m < l}) ≤ Submodule.span ℤ (Set.range (eval C))
⊢ L l

Tactic:
exact this hl

Result:
no goals

Proof state:
case intro.ind
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
⊢ ∀ (x : Products I), (∀ y < x, L y) → L x

Tactic:
intro l h

Result:
case intro.ind
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
⊢ L l

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l : Products I
L : Products I → Prop := fun m => Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
this : L l
⊢ Products.eval C l ∈ ↑(Submodule.span ℤ (Set.range (eval C)))

Tactic:
assumption

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

Tactic:
refine ⟨fun h ↦ le_trans h (span_mono (fun a ⟨b, hb⟩ ↦ ⟨b.val, hb⟩)), fun h ↦ le_trans h ?_⟩

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
⊢ Submodule.span ℤ (Set.range (Products.eval C)) ≤ Submodule.span ℤ (Set.range (eval C))