harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem sup_le (f g f' : α →ₘ[μ] β) (hf : f ≤ f') (hg : g ≤ f') : f ⊔ g ≤ f'

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᶠ[ae μ] ↑f'
hg : ↑g ≤ᶠ[ae μ] ↑f'
⊢ ↑(f ⊔ g) ≤ᶠ[ae μ] ↑f'

Tactic:
filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᶠ[ae μ] ↑f'
hg : ↑g ≤ᶠ[ae μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᶠ[ae μ] ↑f'
hg : ↑g ≤ᶠ[ae μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝

Tactic:
rw [ha_sup]

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᶠ[ae μ] ↑f'
hg : ↑g ≤ᶠ[ae μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ⊔ ↑g a✝ ≤ ↑f' a✝

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : f ≤ f'
hg : g ≤ f'
⊢ f ⊔ g ≤ f'

Tactic:
rw [← coeFn_le] at hf hg ⊢

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᶠ[ae μ] ↑f'
hg : ↑g ≤ᶠ[ae μ] ↑f'
⊢ ↑(f ⊔ g) ≤ᶠ[ae μ] ↑f'

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᶠ[ae μ] ↑f'
hg : ↑g ≤ᶠ[ae μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ⊔ ↑g a✝ ≤ ↑f' a✝

Tactic:
exact sup_le haf hag

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_concat (s n : Nat) : range' s (n + 1) step = range' s n step ++ #[s + step * n]

Proof state:
step s n : Nat
⊢ range' s (n + 1) step = range' s n step ++ #[s + step * n]

Tactic:
exact (range'_append s n 1 step).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_mul_le (a : Int) {b : Int} (H : b ≠ 0) : a / b * b ≤ a :=
  Int.le_of_sub_nonneg <| by rw [Int.mul_comm, ← emod_def]; apply emod_nonneg _ H

Proof state:
a b : Int
H : b ≠ 0
⊢ 0 ≤ a - a / b * b

Tactic:
rw [Int.mul_comm, ← emod_def]

Result:
a b : Int
H : b ≠ 0
⊢ 0 ≤ a % b

Proof state:
a b : Int
H : b ≠ 0
⊢ 0 ≤ a % b

Tactic:
apply emod_nonneg _ H

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_not_dvd (I : Ideal R) (hI : I ≠ 0) :
    ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
        ∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
      v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I

Tactic:
intro h_contr

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ hf.toFinset.erase v, i.maxPowDividing I
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
have h_ne_zero : v.maxPowDividing I ≠ 0 := pow_ne_zero _ v.ne_bot

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : (mulSupport fun v => v.maxPowDividing I).Finite
h_ne_zero : v.maxPowDividing I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem exists_ne_zero_mem_ringOfIntegers_of_norm_le {B : ℝ}
    (h : (minkowskiBound K ↑1) ≤ volume (convexBodySum K B)) :
    ∃ a : 𝓞 K, a ≠ 0 ∧ |Algebra.norm ℚ (a : K)| ≤ (B / finrank ℚ K) ^ finrank ℚ K

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd : ↑|(Algebra.norm ℚ) w✝| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_bd : ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Proof state:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_bd : ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_of_norm_le K ↑1 h

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd : ↑|(Algebra.norm ℚ) w✝| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
/-- If `S` is a closed subalgebra of a Banach algebra `A`, then for any `x : S`, the boundary of
the spectrum of `x` relative to `S` is a subset of the boundary of the spectrum of `↑x : A`
relative to `A`. -/
lemma Subalgebra.frontier_subset_frontier :
    frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 (x : A))

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ frontier (σ 𝕜 ↑x)

Tactic:
rw [frontier_eq_closure_inter_closure (s := σ 𝕜 (x : A)),
  (spectrum.isClosed (x : A)).closure_eq]

Result:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 ↑x ∩ closure (σ 𝕜 ↑x)ᶜ

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ closure (σ 𝕜 ↑x)ᶜ

Tactic:
rw [frontier_eq_closure_inter_closure]

Result:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ closure (σ 𝕜 x) ∩ closure (σ 𝕜 x)ᶜ ⊆ closure (σ 𝕜 ↑x)ᶜ

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ closure (σ 𝕜 x) ∩ closure (σ 𝕜 x)ᶜ ⊆ closure (σ 𝕜 ↑x)ᶜ

Tactic:
exact inter_subset_right |>.trans <|
  closure_mono <| compl_subset_compl.mpr <| spectrum.subset_subalgebra x

Result:
no goals

Proof state:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ σ 𝕜 ↑x ∩ closure (σ 𝕜 ↑x)ᶜ

Tactic:
apply subset_inter (frontier_spectrum S x)

Result:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst✝⁵ : NormedRing A
inst✝⁴ : CompleteSpace A
inst✝³ : SetLike SA A
inst✝² : SubringClass SA A
inst✝¹ : NormedField 𝕜
inst✝ : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed ↑S
x : ↥S
⊢ frontier (σ 𝕜 x) ⊆ closure (σ 𝕜 ↑x)ᶜ
-- Mathlib/Data/Finset/Insert.lean
@[norm_cast]
lemma singleton_subset_coe : {a} ⊆ (s : Set α) ↔ {a} ⊆ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ {a} ⊆ ↑s ↔ {a} ⊆ s

Tactic:
rw [← coe_subset, coe_singleton]

Result:
no goals
-- Mathlib/Algebra/Ring/Invertible.lean
theorem Ring.inverse_sub_inverse [Ring α] {a b : α} (h : IsUnit a ↔ IsUnit b) :
    Ring.inverse a - Ring.inverse b = Ring.inverse a * (b - a) * Ring.inverse b

Proof state:
case neg
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
simp [inverse_non_unit, ha, hb]

Result:
no goals

Proof state:
case pos.intro
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
obtain ⟨ib⟩ := hb.nonempty_invertible

Result:
case pos.intro.intro
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Proof state:
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
by_cases ha : IsUnit a

Result:
case pos
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

case neg
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Proof state:
case neg
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
have hb := h.not.mp ha

Result:
case neg
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Proof state:
case pos.intro.intro
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
simp_rw [inverse_invertible, invOf_sub_invOf]

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
have hb := h.mp ha

Result:
case pos
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Proof state:
case pos
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b

Tactic:
obtain ⟨ia⟩ := ha.nonempty_invertible

Result:
case pos.intro
α : Type u
inst✝ : Ring α
a b : α
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
⊢ inverse a - inverse b = inverse a * (b - a) * inverse b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.unsat_of_lift_unsat (cnf : CNF Nat) :
    (CNF.lift cnf).Unsat → cnf.Unsat

Proof state:
cnf : CNF Nat
h2 : (lift cnf).Unsat
a b : Fin cnf.numLiterals
ha : CNF.Mem a cnf.relabelFin
hb : CNF.Mem b cnf.relabelFin
n_eq✝ : ↑a = ↑b
⊢ a = b

Tactic:
cases a

Result:
case mk
cnf : CNF Nat
h2 : (lift cnf).Unsat
b : Fin cnf.numLiterals
hb : CNF.Mem b cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
ha : CNF.Mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝, isLt✝⟩ = ↑b
⊢ ⟨val✝, isLt✝⟩ = b

Proof state:
case mk.mk
cnf : CNF Nat
h2 : (lift cnf).Unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : CNF.Mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : CNF.Mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩

Tactic:
simp_all

Result:
no goals

Proof state:
cnf : CNF Nat
h2 : (lift cnf).Unsat
⊢ ∀ {v1 v2 : Fin cnf.numLiterals},
    CNF.Mem v1 cnf.relabelFin → CNF.Mem v2 cnf.relabelFin → ⟨↑v1 + 1, ⋯⟩ = ⟨↑v2 + 1, ⋯⟩ → v1 = v2

Tactic:
intro a b ha hb hab

Result:
cnf : CNF Nat
h2 : (lift cnf).Unsat
a b : Fin cnf.numLiterals
ha : CNF.Mem a cnf.relabelFin
hb : CNF.Mem b cnf.relabelFin
hab : ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩
⊢ a = b

Proof state:
cnf : CNF Nat
⊢ (lift cnf).Unsat → cnf.Unsat

Tactic:
intro h2

Result:
cnf : CNF Nat
h2 : (lift cnf).Unsat
⊢ cnf.Unsat

Proof state:
cnf : CNF Nat
h2 : (lift cnf).Unsat
⊢ cnf.Unsat

Tactic:
have h3 :=
  CNF.unsat_relabel_iff
    (by
      intro a b ha hb hab
      injections hab
      cases a; cases b; simp_all)
    |>.mp h2

Result:
cnf : CNF Nat
h2 : (lift cnf).Unsat
h3 : cnf.relabelFin.Unsat
⊢ cnf.Unsat

Proof state:
cnf : CNF Nat
h2 : (lift cnf).Unsat
a b : Fin cnf.numLiterals
ha : CNF.Mem a cnf.relabelFin
hb : CNF.Mem b cnf.relabelFin
hab : ⟨↑a + 1, ⋯⟩ = ⟨↑b + 1, ⋯⟩
⊢ a = b

Tactic:
injections hab

Result:
cnf : CNF Nat
h2 : (lift cnf).Unsat
a b : Fin cnf.numLiterals
ha : CNF.Mem a cnf.relabelFin
hb : CNF.Mem b cnf.relabelFin
n_eq✝ : ↑a = ↑b
⊢ a = b

Proof state:
cnf : CNF Nat
h2 : (lift cnf).Unsat
h3 : cnf.relabelFin.Unsat
⊢ cnf.Unsat

Tactic:
exact CNF.unsat_relabelFin.mp h3

Result:
no goals

Proof state:
case mk
cnf : CNF Nat
h2 : (lift cnf).Unsat
b : Fin cnf.numLiterals
hb : CNF.Mem b cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
ha : CNF.Mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝, isLt✝⟩ = ↑b
⊢ ⟨val✝, isLt✝⟩ = b

Tactic:
cases b

Result:
case mk.mk
cnf : CNF Nat
h2 : (lift cnf).Unsat
val✝¹ : Nat
isLt✝¹ : val✝¹ < cnf.numLiterals
ha : CNF.Mem ⟨val✝¹, isLt✝¹⟩ cnf.relabelFin
val✝ : Nat
isLt✝ : val✝ < cnf.numLiterals
hb : CNF.Mem ⟨val✝, isLt✝⟩ cnf.relabelFin
n_eq✝ : ↑⟨val✝¹, isLt✝¹⟩ = ↑⟨val✝, isLt✝⟩
⊢ ⟨val✝¹, isLt✝¹⟩ = ⟨val✝, isLt✝⟩
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_monomial_eq (s : σ →₀ ℕ) (a : R) (ha : a ≠ 0) :
    degrees (monomial s a) = toMultiset s

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ ((monomial s) a).degrees = toMultiset s

Tactic:
classical
  exact (supDegree_single s a).trans (if_neg ha)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ ((monomial s) a).degrees = toMultiset s

Tactic:
exact (supDegree_single s a).trans (if_neg ha)

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
lemma isSplitMono_toSimplexCategory_map_of_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y}
    (hm : P_δ m) : IsSplitMono <| toSimplexCategory.map m

Proof state:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono (toSimplexCategory.map m)

Tactic:
constructor

Result:
case exists_splitMono
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ Nonempty (SplitMono (toSimplexCategory.map m))

Proof state:
case exists_splitMono.val.sm
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono m

Tactic:
exact isSplitMono_P_δ hm |>.exists_splitMono.some

Result:
no goals

Proof state:
case exists_splitMono.val
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono (toSimplexCategory.map m)

Tactic:
apply SplitMono.map

Result:
case exists_splitMono.val.sm
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono m

Proof state:
case exists_splitMono
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ Nonempty (SplitMono (toSimplexCategory.map m))

Tactic:
constructor

Result:
case exists_splitMono.val
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ SplitMono (toSimplexCategory.map m)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
lemma isClosedEmbedding_nonUnitalStarAlgHom {a : A} {φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A}
    (hφ : IsClosedEmbedding φ) {f : C(S, R)} (h : QuasispectrumRestricts a f)
    (halg : IsUniformEmbedding (algebraMap R S)) :
    IsClosedEmbedding (h.nonUnitalStarAlgHom φ)

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Field S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalRing S
inst✝¹² : ContinuousStar S
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module S A
inst✝⁸ : IsScalarTower S A A
inst✝⁷ : SMulCommClass S A A
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : CompleteSpace R
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
hφ : IsClosedEmbedding ⇑φ
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
halg : IsUniformEmbedding ⇑(algebraMap R S)
this : h.homeomorph.symm 0 = 0
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)

Tactic:
refine hφ.comp <| IsUniformEmbedding.isClosedEmbedding <| .comp
  (ContinuousMapZero.isUniformEmbedding_comp _ halg)
  (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Field S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalRing S
inst✝¹² : ContinuousStar S
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module S A
inst✝⁸ : IsScalarTower S A A
inst✝⁷ : SMulCommClass S A A
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : CompleteSpace R
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
hφ : IsClosedEmbedding ⇑φ
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
halg : IsUniformEmbedding ⇑(algebraMap R S)
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)

Tactic:
have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)

Result:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝²¹ : Semifield R
inst✝²⁰ : StarRing R
inst✝¹⁹ : MetricSpace R
inst✝¹⁸ : IsTopologicalSemiring R
inst✝¹⁷ : ContinuousStar R
inst✝¹⁶ : Field S
inst✝¹⁵ : StarRing S
inst✝¹⁴ : MetricSpace S
inst✝¹³ : IsTopologicalRing S
inst✝¹² : ContinuousStar S
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module S A
inst✝⁸ : IsScalarTower S A A
inst✝⁷ : SMulCommClass S A A
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R S A
inst✝³ : StarModule R S
inst✝² : ContinuousSMul R S
inst✝¹ : TopologicalSpace A
inst✝ : CompleteSpace R
a : A
φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A
hφ : IsClosedEmbedding ⇑φ
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
halg : IsUniformEmbedding ⇑(algebraMap R S)
this : h.homeomorph.symm 0 = 0
⊢ IsClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem contractNth_apply_of_ne (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (hjk : (j : ℕ) ≠ k) : contractNth j op g k = g (j.succAbove k)

Proof state:
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rcases lt_trichotomy (k : ℕ) j with (h | h | h)

Result:
case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

case inr.inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k = ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Proof state:
case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]

Result:
case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j

Proof state:
case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc

Tactic:
exact Fin.le_iff_val_le_val.2 (le_of_lt h)

Result:
no goals

Proof state:
case inr.inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k = ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
exact False.elim (hjk h.symm)

Result:
no goals

Proof state:
case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j

Tactic:
rwa [Fin.lt_iff_val_lt_val]

Result:
no goals

Proof state:
case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]

Result:
case inr.inr.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j ≤ k.castSucc