harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/InformationTheory/Hamming.lean
theorem swap_hammingDist : swap (@hammingDist _ β _ _) = hammingDist

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ swap hammingDist = hammingDist

Tactic:
funext x y

Result:
case h.h
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y

Proof state:
case h.h
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ swap hammingDist x y = hammingDist x y

Tactic:
exact hammingDist_comm _ _

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem map_div_rev : f (x / y) = f (y / x)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : Group α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) = f (y / x)

Tactic:
rw [← inv_div, map_inv_eq_map]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_pred_singleton {a : ℕ} (h : 0 < a) : Ico (a - 1) a = {a - 1}

Proof state:
a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}

Tactic:
rw [← Icc_pred_right _ h, Icc_self]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem eq_loopyOn_iff : M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅

Proof state:
α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
I : Set α
hIE : I ⊆ M.E
⊢ I = ∅ → M.Indep I

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
h : ∀ X ⊆ M.E, M.Indep X → X = ∅
hIE : ∅ ⊆ M.E
⊢ M.Indep ∅

Proof state:
α : Type u_1
M : Matroid α
E : Set α
⊢ M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅

Tactic:
simp only [ext_iff_indep, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]

Result:
α : Type u_1
M : Matroid α
E : Set α
⊢ M.E = E → ((∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)

Proof state:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅

Tactic:
refine ⟨fun h I hI ↦ (h hI).1, fun h I hIE ↦ ⟨h I hIE, by rintro rfl; simp⟩⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
E : Set α
⊢ M.E = E → ((∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅)

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
⊢ (∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)) ↔ ∀ X ⊆ M.E, M.Indep X → X = ∅
-- Mathlib/Data/Nat/Init.lean
lemma mul_add_mod' (a b c : ℕ) : (a * b + c) % b = c % b

Proof state:
a b c : ℕ
⊢ (a * b + c) % b = c % b

Tactic:
rw [Nat.mul_comm, Nat.mul_add_mod]

Result:
no goals
-- Mathlib/Data/Fintype/Defs.lean
theorem eq_univ_iff_forall : s = univ ↔ ∀ x, x ∈ s

Proof state:
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s = univ ↔ ∀ (x : α), x ∈ s

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
lemma add_norm_nonneg (f : α →ᵇ ℝ) :
    0 ≤ f + const _ ‖f‖

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (fun f => f.toFun) 0 x ≤ (fun f => f.toFun) (f + const α ‖f‖) x

Tactic:
simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_zero, Pi.zero_apply, coe_add,
  const_apply, Pi.add_apply]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ 0 ≤ f x + ‖f‖

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ 0 ≤ f x + ‖f‖

Tactic:
linarith [(abs_le.mp (norm_coe_le_norm f x)).1]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ 0 ≤ f + const α ‖f‖

Tactic:
intro x

Result:
α : Type u_2
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (fun f => f.toFun) 0 x ≤ (fun f => f.toFun) (f + const α ‖f‖) x
-- Mathlib/LinearAlgebra/Pi.lean
theorem iSup_range_single [Finite ι] : ⨆ i, range (single R φ i) = ⊤

Proof state:
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ ⨆ i, range (single R φ i) = ⊤

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ⨆ i, range (single R φ i) = ⊤

Proof state:
case intro.convert_2
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Set.univ ⊆ ↑Finset.univ ∪ ∅

Tactic:
rw [Finset.coe_univ, Set.union_empty]

Result:
no goals

Proof state:
case intro
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ⨆ i, range (single R φ i) = ⊤

Tactic:
convert top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_single R φ _)

Result:
case h.e'_2.h.e'_4.h
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x✝ : ι
⊢ range (single R φ x✝) = ⨆ (_ : x✝ ∈ ?intro.convert_1), range (single R φ x✝)

case intro.convert_1
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Finset ι

case intro.convert_2
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Set.univ ⊆ ↑?intro.convert_1 ∪ ∅

Proof state:
case h.e'_2.h.e'_4.h
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
⊢ range (single R φ i) = ⨆ (_ : i ∈ ?intro.convert_1), range (single R φ i)

Tactic:
exact ((@iSup_pos _ _ _ fun _ => range <| single R φ i) <| Finset.mem_univ i).symm

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x✝ : ι
⊢ range (single R φ x✝) = ⨆ (_ : x✝ ∈ ?intro.convert_1), range (single R φ x✝)

Tactic:
rename_i i

Result:
case h.e'_2.h.e'_4.h
R : Type u
ι : Type x
inst✝⁴ : Semiring R
φ : ι → Type i
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
⊢ range (single R φ i) = ⨆ (_ : i ∈ ?intro.convert_1), range (single R φ i)
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_span_le (s : Set M) : Module.rank R (span R s) ≤ #s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (Module.rank R ({ x // x ∈ s } →₀ R)) ≤ lift.{max u v, v} #↑s

Tactic:
rw [rank_finsupp_self]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (lift.{u, v} #{ x // x ∈ s }) ≤ lift.{max u v, v} #↑s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ Module.rank R ↥(span R s) ≤ #↑s

Tactic:
rw [Finsupp.span_eq_range_linearCombination, ← lift_strictMono.le_iff_le]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{?u.168348, v} (Module.rank R ↥(LinearMap.range (Finsupp.linearCombination R Subtype.val))) ≤
    lift.{?u.168348, v} #↑s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{?u.168348, v} (Module.rank R ↥(LinearMap.range (Finsupp.linearCombination R Subtype.val))) ≤
    lift.{?u.168348, v} #↑s

Tactic:
refine (lift_rank_range_le _).trans ?_

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (Module.rank R ({ x // x ∈ s } →₀ R)) ≤ lift.{max u v, v} #↑s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (lift.{u, v} #{ x // x ∈ s }) ≤ lift.{max u v, v} #↑s

Tactic:
simp only [lift_lift, le_refl]

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_empty : sInf ∅ = 0

Proof state:
⊢ 0 ∈ ∅ ∨ ∅ = ∅

Tactic:
right

Result:
case h

⊢ ∅ = ∅

Proof state:
⊢ sInf ∅ = 0

Tactic:
rw [sInf_eq_zero]

Result:
⊢ 0 ∈ ∅ ∨ ∅ = ∅

Proof state:
case h

⊢ ∅ = ∅

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem singleton_add_eq (a : A) (r : R) : {r} + σ a = σ (↑ₐ r + a) :=
  ext fun x => by
    rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r x : R
⊢ x ∈ {r} + σ a ↔ x ∈ σ (↑ₐ r + a)

Tactic:
rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma div_le_iff_le_mul (h : 0 < b) (h' : b ≠ ⊤) : a / b ≤ c ↔ a ≤ b * c

Proof state:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c ↔ a ≤ b * c

Tactic:
nth_rw 1 [← @mul_div_cancel c b (ne_bot_of_gt h) h' (ne_of_gt h)]

Result:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c

Proof state:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b

Tactic:
exact StrictMono.le_iff_le (strictMono_div_right_of_pos h h')

Result:
no goals

Proof state:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ b * (c / b) ↔ a ≤ b * c

Tactic:
rw [mul_div b c b, mul_comm b]

Result:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a / b ≤ c * b / b ↔ a ≤ c * b
-- Mathlib/Topology/Order/Hom/Basic.lean
theorem cancel_left {g : β →Co γ} {f₁ f₂ : α →Co β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : Preorder α
inst✝³ : TopologicalSpace β
inst✝² : Preorder β
inst✝¹ : TopologicalSpace γ
inst✝ : Preorder γ
g : β →Co γ
f₁ f₂ : α →Co β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
@[reassoc]
lemma ProjectiveResolution.iso_hom_naturality {X Y : C} (f : X ⟶ Y)
    (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
    (φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f) :
    (projectiveResolutions C).map f ≫ Q.iso.hom =
      P.iso.hom ≫ (HomotopyCategory.quotient _ _).map φ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (projectiveResolutions C).map f ≫ Q.iso.hom = P.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ

Tactic:
rw [← cancel_epi (P.iso).inv, iso_inv_naturality_assoc f P Q φ comm,
  Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem map₂Right_eq_zipWith (h : length bs ≤ length as) :
    map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs

Proof state:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
this : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b
⊢ map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs

Tactic:
simp only [map₂Right, map₂Left_eq_zipWith, zipWith_flip, *]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
⊢ map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs

Tactic:
have : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b := rfl

Result:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
as : List α
bs : List β
h : bs.length ≤ as.length
this : (fun a b => flip f a (some b)) = flip fun a b => f (some a) b
⊢ map₂Right f as bs = zipWith (fun a b => f (some a) b) as bs
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_prod' (h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) :
    (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (Multiset.map (fun f => f.leadingCoeff) (Multiset.map f s.val)).prod ≠ 0

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using natDegree_multiset_prod' (s.1.map f) (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
    zipWithAll f (mkArray n a) (mkArray n b) = mkArray n (f a b)

Proof state:
α : Type u_1
β : Type u_2
α✝ : Type u_3
f : Option α → Option β → α✝
a : α
b : β
n : Nat
⊢ zipWithAll f (mkArray n a) (mkArray n b) = mkArray n (f (some a) (some b))

Tactic:
simp [← List.toArray_replicate]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
theorem smul_le_self_of_tower {α : Type*} [Semiring α] [Module α R] [Module α M]
    [SMulCommClass α R M] [IsScalarTower α R M] (a : α) (S : Submodule R M) : a • S ≤ S

Proof state:
case intro.intro
R : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
α : Type u_4
inst✝⁴ : Semiring α
inst✝³ : Module α R
inst✝² : Module α M
inst✝¹ : SMulCommClass α R M
inst✝ : IsScalarTower α R M
a : α
S : Submodule R M
x : M
hx : x ∈ ↑S
⊢ (DistribMulAction.toLinearMap R M a) x ∈ S

Tactic:
exact smul_of_tower_mem _ a hx

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
α : Type u_4
inst✝⁴ : Semiring α
inst✝³ : Module α R
inst✝² : Module α M
inst✝¹ : SMulCommClass α R M
inst✝ : IsScalarTower α R M
a : α
S : Submodule R M
⊢ a • S ≤ S

Tactic:
rintro y ⟨x, hx, rfl⟩

Result:
case intro.intro
R : Type u_2
M : Type u_3
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
α : Type u_4
inst✝⁴ : Semiring α
inst✝³ : Module α R
inst✝² : Module α M
inst✝¹ : SMulCommClass α R M
inst✝ : IsScalarTower α R M
a : α
S : Submodule R M
x : M
hx : x ∈ ↑S
⊢ (DistribMulAction.toLinearMap R M a) x ∈ S
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma XClass_ne_zero [Nontrivial R] (x : R) : XClass W x ≠ 0 :=
  AdjoinRoot.mk_ne_zero_of_natDegree_lt W.monic_polynomial (C_ne_zero.mpr <| X_sub_C_ne_zero x) <|
    by rw [natDegree_polynomial, natDegree_C]; norm_num1

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
x : R
⊢ (C (X - C x)).natDegree < W.polynomial.natDegree

Tactic:
rw [natDegree_polynomial, natDegree_C]

Result:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
x : R
⊢ 0 < 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
x : R
⊢ 0 < 2

Tactic:
norm_num1

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma compactSpace {R S A : Type*} [Semifield R] [Field S] [NonUnitalRing A]
    [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A]
    [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] {a : A} (f : C(S, R))
    (h : QuasispectrumRestricts a f) [h_cpct : CompactSpace (σₙ S a)] :
    CompactSpace (σₙ R a)

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝¹⁰ : Semifield R
inst✝⁹ : Field S
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Module R A
inst✝⁵ : Module S A
inst✝⁴ : IsScalarTower S A A
inst✝³ : SMulCommClass S A A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_cpct : IsCompact (σₙ S a)
⊢ IsCompact (σₙ R a)

Tactic:
exact h.image ▸ h_cpct.image (map_continuous f)

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝¹⁰ : Semifield R
inst✝⁹ : Field S
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Module R A
inst✝⁵ : Module S A
inst✝⁴ : IsScalarTower S A A
inst✝³ : SMulCommClass S A A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_cpct : CompactSpace ↑(σₙ S a)
⊢ CompactSpace ↑(σₙ R a)

Tactic:
rw [← isCompact_iff_compactSpace] at h_cpct ⊢

Result:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝¹⁰ : Semifield R
inst✝⁹ : Field S
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Algebra R S
inst✝⁶ : Module R A
inst✝⁵ : Module S A
inst✝⁴ : IsScalarTower S A A
inst✝³ : SMulCommClass S A A
inst✝² : IsScalarTower R S A
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts a ⇑f
h_cpct : IsCompact (σₙ S a)
⊢ IsCompact (σₙ R a)
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma opcyclesIsoSc'_inv_fromOpcycles :
    (K.opcyclesIsoSc' i j k hi hk).inv ≫ K.fromOpcycles j k =
      (K.sc' i j k).fromOpcycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.opcyclesIsoSc' i j k hi hk).inv ≫ K.fromOpcycles j k = (K.sc' i j k).fromOpcycles

Tactic:
simp only [← cancel_epi (K.sc' i j k).pOpcycles,  pOpcycles_opcyclesIsoSc'_inv_assoc,
  p_fromOpcycles, ShortComplex.p_fromOpcycles, shortComplexFunctor'_obj_g]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem _root_.PreValuationRing.iff_dvd_total [Monoid R] :
    PreValuationRing R ↔ IsTotal R (· ∣ ·)

Proof state:
R : Type u_1
inst✝ : Monoid R
⊢ PreValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2

Tactic:
refine ⟨fun H => ⟨fun a b => ?_⟩, fun H => ⟨fun a b => ?_⟩⟩

Result:
case refine_1
R : Type u_1
inst✝ : Monoid R
H : PreValuationRing R
a b : R
⊢ a ∣ b ∨ b ∣ a

case refine_2
R : Type u_1
inst✝ : Monoid R
H : IsTotal R fun x1 x2 => x1 ∣ x2
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a

Proof state:
case refine_1
R : Type u_1
inst✝ : Monoid R
H : PreValuationRing R
a b : R
⊢ a ∣ b ∨ b ∣ a

Tactic:
obtain ⟨c, rfl | rfl⟩ := PreValuationRing.cond a b <;> simp

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Monoid R
H : IsTotal R fun x1 x2 => x1 ∣ x2
a b : R
⊢ ∃ c, a * c = b ∨ b * c = a

Tactic:
obtain ⟨c, rfl⟩ | ⟨c, rfl⟩ := @IsTotal.total _ _ H a b <;> use c <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem and_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∧ b) = a

Proof state:
a b : Prop
h : b = True
⊢ (a ∧ b) = a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem not_isCofinal_iff {s : Set α} : ¬ IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬IsCofinal s ↔ ∃ x, ∀ y ∈ s, y < x

Tactic:
simp [IsCofinal]

Result:
no goals
-- Mathlib/Topology/Germ.lean
lemma eq_of_germ_isConstant_on {s : Set X} (h : ∀ x ∈ s, (f : Germ (𝓝 x) Y).IsConstant)
    (hs : IsPreconnected s) {x' : X} (x_in : x ∈ s) (x'_in : x' ∈ s) : f x = f x'

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
⊢ f x = f x'

Tactic:
let i : s → X := fun x ↦ x

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x => ↑x
⊢ f x = f x'

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x => ↑x
this : PreconnectedSpace ↑s
⊢ (f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩

Tactic:
exact eq_of_germ_isConstant (fun y ↦ Germ.isConstant_comp_subtype (h y y.2)) _ _

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x => ↑x
⊢ (f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩

Tactic:
have : PreconnectedSpace s := Subtype.preconnectedSpace hs

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x => ↑x
this : PreconnectedSpace ↑s
⊢ (f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x => ↑x
⊢ f x = f x'

Tactic:
show (f ∘ i) (⟨x, x_in⟩ : s) = (f ∘ i) (⟨x', x'_in⟩ : s)

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, (↑f).IsConstant
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : ↑s → X := fun x => ↑x
⊢ (f ∘ i) ⟨x, x_in⟩ = (f ∘ i) ⟨x', x'_in⟩