-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem injective : Function.Injective (eval C)

Proof state:
case inr.inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha hb : Products.isGood C a
h : Products.eval C a = Products.eval C a
⊢ ⟨a, ha⟩ = ⟨a, hb⟩

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ Function.Injective (eval C)

Tactic:
intro ⟨a, ha⟩ ⟨b, hb⟩ h

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : eval C ⟨a, ha⟩ = eval C ⟨b, hb⟩
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Proof state:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Tactic:
exact Submodule.subset_span ⟨a, h', rfl⟩

Result:
no goals

Proof state:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Tactic:
rw [← h]

Result:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Proof state:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Tactic:
exact Submodule.subset_span ⟨b, ⟨h',rfl⟩⟩

Result:
no goals

Proof state:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
exfalso

Result:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ False

Proof state:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Tactic:
rw [h]

Result:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Proof state:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ False

Tactic:
apply ha

Result:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Proof state:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
exfalso

Result:
case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ False

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
rcases lt_trichotomy a b with (h'|rfl|h')

Result:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

case inr.inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha hb : Products.isGood C a
h : Products.eval C a = Products.eval C a
⊢ ⟨a, ha⟩ = ⟨a, hb⟩

case inr.inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : b < a
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Proof state:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ False

Tactic:
apply hb

Result:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
h' : a < b
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : eval C ⟨a, ha⟩ = eval C ⟨b, hb⟩
⊢ ⟨a, ha⟩ = ⟨b, hb⟩

Tactic:
dsimp [eval] at h

Result:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
⊢ ⟨a, ha⟩ = ⟨b, hb⟩