harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_subset_Ici_iff [DenselyOrdered α] : Ioi b ⊆ Ici a ↔ a ≤ b

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False

Tactic:
exact lt_irrefl _ (ca.trans_le (h bc))

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False

Tactic:
obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
c : α
bc : b < c
ca : c < a
⊢ False

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioi b ⊆ Ici a ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, fun h => Ioi_subset_Ici h⟩

Result:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b

Tactic:
by_contra ba

Result:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_ne_gt {a b : Nat} : compare a b ≠ .gt ↔ a ≤ b

Proof state:
a b : Nat
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b

Tactic:
rw [compare_def_le]

Result:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt) ≠ Ordering.gt ↔ a ≤ b

Proof state:
case isTrue
a b : Nat
h✝ : a ≤ b
⊢ (if b ≤ a then Ordering.eq else Ordering.lt) ≠ Ordering.gt ↔ a ≤ b

Tactic:
split

Result:
case isTrue.isTrue
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

case isTrue.isFalse
a b : Nat
h✝¹ : a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b

Proof state:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt) ≠ Ordering.gt ↔ a ≤ b

Tactic:
(repeat' split) <;> simp [*]

Result:
no goals

Proof state:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt) ≠ Ordering.gt ↔ a ≤ b

Tactic:
repeat' split

Result:
case isTrue.isTrue
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

case isTrue.isFalse
a b : Nat
h✝¹ : a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b

case isFalse
a b : Nat
h✝ : ¬a ≤ b
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonneg_iff_pos_imp_nonneg : 0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) :=
  smul_nonneg_iff.trans <| by
    simp_rw [← not_le, ← or_iff_not_imp_left]; have := le_total a 0; have := le_total b 0; tauto

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
have := le_total a 0

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
this : a ≤ 0 ∨ 0 ≤ a
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Tactic:
simp_rw [← not_le, ← or_iff_not_imp_left]

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
this✝ : a ≤ 0 ∨ 0 ≤ a
this : b ≤ 0 ∨ 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
this : a ≤ 0 ∨ 0 ≤ a
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)

Tactic:
have := le_total b 0

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
this✝ : a ≤ 0 ∨ 0 ≤ a
this : b ≤ 0 ∨ 0 ≤ b
⊢ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 ↔ (a ≤ 0 ∨ 0 ≤ b) ∧ (b ≤ 0 ∨ 0 ≤ a)
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@[simp]
lemma toTwoSided_asIdeal (I : TwoSidedIdeal R) (h) : (TwoSidedIdeal.asIdeal I).toTwoSided h = I :=
  by ext; simp

Proof state:
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
h : ∀ {x y : R}, x ∈ TwoSidedIdeal.asIdeal I → x * y ∈ TwoSidedIdeal.asIdeal I
⊢ (TwoSidedIdeal.asIdeal I).toTwoSided h = I

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
h : ∀ {x y : R}, x ∈ TwoSidedIdeal.asIdeal I → x * y ∈ TwoSidedIdeal.asIdeal I
x✝ : R
⊢ x✝ ∈ (TwoSidedIdeal.asIdeal I).toTwoSided h ↔ x✝ ∈ I

Proof state:
case h
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
h : ∀ {x y : R}, x ∈ TwoSidedIdeal.asIdeal I → x * y ∈ TwoSidedIdeal.asIdeal I
x✝ : R
⊢ x✝ ∈ (TwoSidedIdeal.asIdeal I).toTwoSided h ↔ x✝ ∈ I

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem sInf_toSetoid (S : Set (RingCon R)) : (sInf S).toSetoid = sInf ((·.toSetoid) '' S) :=
  Setoid.ext fun x y =>
    ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x => x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x => x.toSetoid) c = r
⊢ r x y

Tactic:
rw [← hr]

Result:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x => x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x => x.toSetoid) c = r
⊢ ((fun x => x.toSetoid) c) x y

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x => x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x => x.toSetoid) c = r
⊢ ((fun x => x.toSetoid) c) x y

Tactic:
exact h c hS

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem replicate_subset {n : Nat} {a : α} {l : List α} : replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l

Tactic:
induction n with
| zero => simp
| succ n ih => simp +contextual [replicate_succ, ih, cons_subset]

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
l : List α
n : Nat
ih : replicate n a ⊆ l ↔ n = 0 ∨ a ∈ l
⊢ replicate (n + 1) a ⊆ l ↔ n + 1 = 0 ∨ a ∈ l

Tactic:
simp +contextual [replicate_succ, ih, cons_subset]

Result:
no goals

Proof state:
case zero
α : Type u_1
a : α
l : List α
⊢ replicate 0 a ⊆ l ↔ 0 = 0 ∨ a ∈ l

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_le_left {a b : Ordinal} (h : a ≤ b) (c : Ordinal) : a / c ≤ b / c

Proof state:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c

Tactic:
rw [le_div hc]

Result:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b

Proof state:
case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b

Tactic:
exact (mul_div_le a c).trans h

Result:
no goals

Proof state:
case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0

Tactic:
rw [div_zero, div_zero]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
⊢ a / c ≤ b / c

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0

case inr
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c
-- Mathlib/Algebra/RingQuot.lean
theorem lift_unique (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y)
    (g : RingQuot r →+* T) (h : g.comp (mkRingHom r) = f) : g = lift ⟨f, w⟩

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
g : RingQuot r →+* T
h : g.comp (mkRingHom r) = f
⊢ g = lift ⟨f, w⟩

Tactic:
ext

Result:
case w.a
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
g : RingQuot r →+* T
h : g.comp (mkRingHom r) = f
x✝ : R
⊢ (g.comp (mkRingHom r)) x✝ = ((lift ⟨f, w⟩).comp (mkRingHom r)) x✝

Proof state:
case w.a
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → f x = f y
g : RingQuot r →+* T
h : g.comp (mkRingHom r) = f
x✝ : R
⊢ (g.comp (mkRingHom r)) x✝ = ((lift ⟨f, w⟩).comp (mkRingHom r)) x✝

Tactic:
simp [h]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem IsPreprimitive.of_subsingleton [SMul G X] [Nonempty G] [Subsingleton X] :
    IsPreprimitive G X where
  exists_smul_eq (x y)

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y

Tactic:
rw [eq_iff_true_of_subsingleton]

Result:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True

Proof state:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ ∃ g, g • x = y

Tactic:
use Classical.arbitrary G

Result:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ Classical.arbitrary G • x = y

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
x y : X
⊢ True

Tactic:
trivial

Result:
no goals

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
B✝ : Set X
B : IsBlock G B✝
⊢ B✝.Subsingleton

Tactic:
exact Set.subsingleton_of_subsingleton

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
B✝ : Set X
B : IsBlock G B✝
⊢ IsTrivialBlock B✝

Tactic:
left

Result:
case h
G : Type u_1
X : Type u_2
inst✝² : SMul G X
inst✝¹ : Nonempty G
inst✝ : Subsingleton X
B✝ : Set X
B : IsBlock G B✝
⊢ B✝.Subsingleton
-- Mathlib/Data/PFun.lean
theorem fix_stop {f : α →. β ⊕ α} {b : β} {a : α} (hb : Sum.inl b ∈ f a) : b ∈ f.fix a

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'

Tactic:
exact Or.inl hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ b ∈ f.fix a

Tactic:
rw [PFun.mem_fix_iff]

Result:
α : Type u_1
β : Type u_2
f : α →. β ⊕ α
b : β
a : α
hb : Sum.inl b ∈ f a
⊢ Sum.inl b ∈ f a ∨ ∃ a', Sum.inr a' ∈ f a ∧ b ∈ f.fix a'
-- Mathlib/Data/Set/Insert.lean
theorem subset_pair_iff_eq {x y : α} : s ⊆ {x, y} ↔ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Proof state:
α : Type u
s : Set α
x y : α
h : x ∈ s → {y} = s \ {x} → s = {x, y}
⊢ (s = ∅ ∨ s = {y}) ∨ x ∈ s ∧ ((s = ∅ ∨ s = {x}) ∨ s \ {x} = {y}) → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u
s : Set α
x y : α
⊢ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y} → s ⊆ {x, y}

Tactic:
rintro (rfl | rfl | rfl | rfl) <;> simp [pair_subset_iff]

Result:
no goals

Proof state:
α : Type u
s : Set α
x y : α
h₁ : x ∈ s
h₂ : {y} = s \ {x}
⊢ s = {x, y}

Tactic:
simp [h₁, h₂]

Result:
no goals

Proof state:
α : Type u
s : Set α
x y : α
⊢ s ⊆ {x, y} → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
rw [subset_insert_iff, subset_singleton_iff_eq, subset_singleton_iff_eq,
  ← subset_empty_iff (s := s \ {x}), diff_subset_iff, union_empty, subset_singleton_iff_eq]

Result:
α : Type u
s : Set α
x y : α
⊢ (s = ∅ ∨ s = {y}) ∨ x ∈ s ∧ ((s = ∅ ∨ s = {x}) ∨ s \ {x} = {y}) → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Proof state:
α : Type u
s : Set α
x y : α
⊢ s ⊆ {x, y} ↔ s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
refine ⟨?_, by rintro (rfl | rfl | rfl | rfl) <;> simp [pair_subset_iff]⟩

Result:
α : Type u
s : Set α
x y : α
⊢ s ⊆ {x, y} → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Proof state:
α : Type u
s : Set α
x y : α
⊢ (s = ∅ ∨ s = {y}) ∨ x ∈ s ∧ ((s = ∅ ∨ s = {x}) ∨ s \ {x} = {y}) → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}

Tactic:
have h : x ∈ s → {y} = s \ {x} → s = {x,y} := fun h₁ h₂ ↦ by simp [h₁, h₂]

Result:
α : Type u
s : Set α
x y : α
h : x ∈ s → {y} = s \ {x} → s = {x, y}
⊢ (s = ∅ ∨ s = {y}) ∨ x ∈ s ∧ ((s = ∅ ∨ s = {x}) ∨ s \ {x} = {y}) → s = ∅ ∨ s = {x} ∨ s = {y} ∨ s = {x, y}
-- Mathlib/LinearAlgebra/Quotient/Defs.lean
theorem mkQ_surjective : Function.Surjective p.mkQ

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, p.mkQ a = Quot.mk (⇑p.quotientRel) x

Tactic:
exact ⟨x, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ Function.Surjective ⇑p.mkQ

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
b✝ : M ⧸ p
x : M
⊢ ∃ a, p.mkQ a = Quot.mk (⇑p.quotientRel) x
-- Mathlib/Topology/ContinuousMap/Units.lean
theorem spectrum_eq_preimage_range (f : C(X, R)) :
    spectrum 𝕜 f = algebraMap _ _ ⁻¹' Set.range f

Proof state:
case h
X : Type u_1
R : Type u_3
𝕜 : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedField 𝕜
inst✝² : NormedDivisionRing R
inst✝¹ : Algebra 𝕜 R
inst✝ : CompleteSpace R
f : C(X, R)
x : 𝕜
⊢ x ∈ spectrum 𝕜 f ↔ x ∈ ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f

Tactic:
simp only [spectrum.mem_iff, isUnit_iff_forall_ne_zero, not_forall, sub_apply,
  algebraMap_apply, mul_one, Classical.not_not, Set.mem_range,
  sub_eq_zero, @eq_comm _ (x • 1 : R) _, Set.mem_preimage, Algebra.algebraMap_eq_smul_one,
  smul_apply, one_apply]

Result:
no goals

Proof state:
X : Type u_1
R : Type u_3
𝕜 : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedField 𝕜
inst✝² : NormedDivisionRing R
inst✝¹ : Algebra 𝕜 R
inst✝ : CompleteSpace R
f : C(X, R)
⊢ spectrum 𝕜 f = ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f

Tactic:
ext x

Result:
case h
X : Type u_1
R : Type u_3
𝕜 : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedField 𝕜
inst✝² : NormedDivisionRing R
inst✝¹ : Algebra 𝕜 R
inst✝ : CompleteSpace R
f : C(X, R)
x : 𝕜
⊢ x ∈ spectrum 𝕜 f ↔ x ∈ ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem restr_trans (s : Set α) : (e.restr s).trans e' = (e.trans e').restr s :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl) <| by
    simp [trans_source, inter_comm, inter_assoc]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
s : Set α
⊢ ((e.restr s).trans e').source = ((e.trans e').restr s).source

Tactic:
simp [trans_source, inter_comm, inter_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_modify_self (h : m.1.WF) {k : α} {f : β k → β k} {hc : (m.modify k f).contains k} :
    haveI h' : m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : β k → β k
hc : (m.modify k f).contains k = true
⊢ m.contains k = true

Tactic:
rwa [contains_modify _ h] at hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
f : β k → β k
hc : (m.modify k f).contains k = true
⊢ (m.modify k f).get k hc = f (m.get k ⋯)

Tactic:
simp_to_model [modify] using List.getValueCast_modifyKey_self

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean
@[reassoc (attr := simp)]
lemma ι_colimitFiberwiseColimitIso_inv (X : Grothendieck F) :
    colimit.ι G X ≫ (colimitFiberwiseColimitIso G).inv =
    colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫
      colimit.ι (fiberwiseColimit G) X.base

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit (F.map f ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : HasColimit (fiberwiseColimit G)
X : Grothendieck F
⊢ colimit.ι G X ≫ (colimitFiberwiseColimitIso G).inv =
    colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base

Tactic:
rw [Iso.comp_inv_eq]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit (F.map f ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : HasColimit (fiberwiseColimit G)
X : Grothendieck F
⊢ colimit.ι G X =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base) ≫
      (colimitFiberwiseColimitIso G).hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝² : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit (F.map f ⋙ Grothendieck.ι F Y ⋙ G)
inst✝ : HasColimit (fiberwiseColimit G)
X : Grothendieck F
⊢ colimit.ι G X =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base) ≫
      (colimitFiberwiseColimitIso G).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem modByMonic_eq_self_iff [Nontrivial R] (hq : Monic q) : p %ₘ q = p ↔ degree p < degree q :=
  ⟨fun h => h ▸ degree_modByMonic_lt _ hq, fun h => by
    classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]⟩

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          let_fun _wf := ⋯;
          let dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Tactic:
dsimp

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).2
    else p) =
    p

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p %ₘ q = p

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p %ₘ q = p

Tactic:
unfold modByMonic divModByMonicAux

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          let_fun _wf := ⋯;
          let dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).2
    else p) =
    p

Tactic:
rw [dif_pos hq, if_neg (mt And.left this)]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p

Tactic:
classical
have : ¬degree q ≤ degree p := not_le_of_gt h
unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Bounded.weak_left : ∀ {t : Ordnode α} {o₁ o₂}, Bounded t o₁ o₂ → Bounded t ⊥ o₂
  | nil, o₁, o₂, h => by cases o₂ <;> trivial
  | node _ _ _ _, _, _, ⟨ol, Or⟩ => ⟨ol.weak_left, Or⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : nil.Bounded o₁ o₂
⊢ nil.Bounded ⊥ o₂

Tactic:
cases o₂ <;> trivial

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem Acc.list_chain' {l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r a) :
    Acc (List.lex_chains r) l

Proof state:
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: l)), Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
rw [(by rfl : l = l'.1)]

Result:
case mk.cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl' : List.Chain' (flip r) l
l' : List.chains r := ⟨l, hl'⟩
this : Acc (List.lex_chains r) l'
⊢ ∀ (hl : List.Chain' (flip r) (a :: ↑l')), Acc (List.lex_chains r) ⟨a :: ↑l', hl⟩

Proof state:
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.Chain' (flip r) (a :: l)
hl' : List.Chain' (flip r) l
l' : List.chains r := ⟨l, hl'⟩
⊢ Acc (List.lex_chains r) l'

Tactic:
rcases l with - | ⟨b, l⟩

Result:
case nil
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
hl : List.Chain' (flip r) [a]
hl' : List.Chain' (flip r) []
l' : List.chains r := ⟨[], hl'⟩
⊢ Acc (List.lex_chains r) l'

case cons
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.Chain' (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
b : α
l : List α
hl : List.Chain' (flip r) (a :: b :: l)
hl' : List.Chain' (flip r) (b :: l)
l' : List.chains r := ⟨b :: l, hl'⟩
⊢ Acc (List.lex_chains r) l'
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int)

Proof state:
a : Int
⊢ a ∣ ↑a.natAbs

Tactic:
rw [Int.dvd_natAbs]

Result:
a : Int
⊢ a ∣ a

Proof state:
a : Int
⊢ a ∣ a

Tactic:
exact Int.dvd_refl a

Result:
no goals