harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ Literal.negate l ↔ p ⊭ l

Proof state:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

Tactic:
intro h pl

Result:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False

Proof state:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p ⊨ l.negate ↔ ¬(p ⊨ l)

Tactic:
simp only [Literal.negate, sat_iff]

Result:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)

Proof state:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd

Tactic:
cases h : p l.fst <;> simp_all

Result:
no goals

Proof state:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬(p ⊨ l)
⊢ p l.fst = !l.snd

Tactic:
rw [sat_iff] at h

Result:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd

Proof state:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd

Tactic:
intro h

Result:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬(p ⊨ l)
⊢ p l.fst = !l.snd

Proof state:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False

Tactic:
rw [sat_iff, h] at pl

Result:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : (!l.snd) = l.snd
⊢ False

Proof state:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)

Tactic:
constructor

Result:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd

Proof state:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : (!l.snd) = l.snd
⊢ False

Tactic:
simp at pl

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem mk_covBy_mk_iff_right : (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂

Tactic:
simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
private lemma noAccidental (hs : IsCornerFree (A : Set (G × G))) :
    NoAccidental (triangleIndices A) where
  eq_or_eq_or_eq a a' b b' c c' ha hb hc

Proof state:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
hs : IsCornerFree ↑A
a a' b b' c c' : G
ha : (a', b) ∈ A ∧ c = a' + b
hb : (a, b') ∈ A ∧ c = a + b'
hc : (a, b) ∈ A ∧ c' = a + b
⊢ a = a' ∨ b = b' ∨ c = c'

Tactic:
exact .inl <| hs ⟨hc.1, hb.1, ha.1, hb.2.symm.trans ha.2⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
hs : IsCornerFree ↑A
a a' b b' c c' : G
ha : (a', b, c) ∈ Corners.triangleIndices A
hb : (a, b', c) ∈ Corners.triangleIndices A
hc : (a, b, c') ∈ Corners.triangleIndices A
⊢ a = a' ∨ b = b' ∨ c = c'

Tactic:
simp only [mk_mem_triangleIndices] at ha hb hc

Result:
G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
hs : IsCornerFree ↑A
a a' b b' c c' : G
ha : (a', b) ∈ A ∧ c = a' + b
hb : (a, b') ∈ A ∧ c = a + b'
hc : (a, b) ∈ A ∧ c' = a + b
⊢ a = a' ∨ b = b' ∨ c = c'
-- Mathlib/Probability/ConditionalProbability.lean
@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[s|s] = 1

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs₀ : μ s ≠ 0
hs : μ s ≠ ⊤
⊢ μ[s | s] = 1

Tactic:
simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem le_size_erase [LawfulBEq α] (a : α) (l : Array α) : l.size - 1 ≤ (l.erase a).size

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ { toList := l }.size - 1 ≤ ({ toList := l }.erase a).size

Tactic:
simpa using List.le_length_erase a l

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ l.size - 1 ≤ (l.erase a).size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ { toList := l }.size - 1 ≤ ({ toList := l }.erase a).size
-- Mathlib/Data/NNReal/Defs.lean
theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n

Proof state:
case a
n : ℤ
⊢ ↑↑n.natAbs = ↑(nnabs ↑n)

Tactic:
rw [NNReal.coe_natCast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]

Result:
no goals

Proof state:
n : ℤ
⊢ ↑n.natAbs = nnabs ↑n

Tactic:
ext

Result:
case a
n : ℤ
⊢ ↑↑n.natAbs = ↑(nnabs ↑n)
-- Mathlib/Order/Interval/Set/Pi.lean
theorem pi_univ_Icc : (pi univ fun i ↦ Icc (x i) (y i)) = Icc x y :=
  ext fun y ↦ by simp [Pi.le_def, forall_and]

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ univ.pi fun i => Icc (x i) (y✝ i)) ↔ y ∈ Icc x y✝

Tactic:
simp [Pi.le_def, forall_and]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem isFractional_of_le {I : Submodule R P} {J : FractionalIdeal S P} (hIJ : I ≤ J) :
    IsFractional S I

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
⊢ IsFractional S I

Tactic:
obtain ⟨a, a_mem, ha⟩ := J.isFractional

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
⊢ IsFractional S I

Proof state:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)

Tactic:
exact ha b (hIJ b_mem)

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
⊢ IsFractional S I

Tactic:
use a, a_mem

Result:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
⊢ ∀ b ∈ I, IsInteger R (a • b)

Proof state:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
⊢ ∀ b ∈ I, IsInteger R (a • b)

Tactic:
intro b b_mem

Result:
case right
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
J : FractionalIdeal S P
hIJ : I ≤ ↑J
a : R
a_mem : a ∈ S
ha : ∀ b ∈ ↑J, IsInteger R (a • b)
b : P
b_mem : b ∈ I
⊢ IsInteger R (a • b)
-- Mathlib/Topology/Category/TopCat/Opens.lean
lemma set_range_inclusion' {X : TopCat} (U : Opens X) :
    Set.range (inclusion' U) = (U : Set X)

Proof state:
case h.mpr
X : TopCat
U : Opens ↑X
x : ↑X
h : x ∈ ↑U
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Tactic:
exact ⟨⟨x, h⟩, rfl⟩

Result:
no goals

Proof state:
case h.mp
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') → x ∈ ↑U

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.mp.intro
X : TopCat
U : Opens ↑X
x : ↑((toTopCat X).obj U)
⊢ (ConcreteCategory.hom U.inclusion') x ∈ ↑U

Proof state:
case h.mp.intro
X : TopCat
U : Opens ↑X
x : ↑((toTopCat X).obj U)
⊢ (ConcreteCategory.hom U.inclusion') x ∈ ↑U

Tactic:
exact x.2

Result:
no goals

Proof state:
case h.mpr
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ ↑U → x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Tactic:
intro h

Result:
case h.mpr
X : TopCat
U : Opens ↑X
x : ↑X
h : x ∈ ↑U
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Proof state:
case h
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') ↔ x ∈ ↑U

Tactic:
constructor

Result:
case h.mp
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') → x ∈ ↑U

case h.mpr
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ ↑U → x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Proof state:
X : TopCat
U : Opens ↑X
⊢ Set.range ⇑(ConcreteCategory.hom U.inclusion') = ↑U

Tactic:
ext x

Result:
case h
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') ↔ x ∈ ↑U
-- Mathlib/Data/Nat/Init.lean
protected lemma div_le_self' (m n : ℕ) : m / n ≤ m

Proof state:
case inl
m : ℕ
⊢ m / 0 ≤ m

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
hn : n > 0
⊢ m = 1 * m

Tactic:
rw [Nat.one_mul]

Result:
no goals

Proof state:
case inr
m n : ℕ
hn : n > 0
⊢ m ≤ n * m

Tactic:
calc
  m = 1 * m := by rw [Nat.one_mul]
  _ ≤ n * m := Nat.mul_le_mul_right _ hn

Result:
no goals

Proof state:
case inr
m n : ℕ
hn : n > 0
⊢ m / n ≤ m

Tactic:
refine Nat.div_le_of_le_mul' ?_

Result:
case inr
m n : ℕ
hn : n > 0
⊢ m ≤ n * m

Proof state:
m n : ℕ
⊢ m / n ≤ m

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Result:
case inl
m : ℕ
⊢ m / 0 ≤ m

case inr
m n : ℕ
hn : n > 0
⊢ m / n ≤ m
-- Mathlib/ModelTheory/Substructures.lean
theorem realize_formula_top {α : Type*} {φ : L.Formula α} {v : α → (⊤ : L.Substructure M)} :
    φ.Realize v ↔ φ.Realize (((↑) : (⊤ : L.Substructure M) → M) ∘ v)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) ↔ φ.Realize (Subtype.val ∘ v)

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)

Tactic:
rw [← StrongHomClass.realize_formula Substructure.topEquiv φ]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u_3
φ : L.Formula α
v : α → ↥⊤
⊢ φ.Realize (⇑topEquiv ∘ v) ↔ φ.Realize (Subtype.val ∘ v)
-- Mathlib/Data/Nat/Init.lean
protected lemma div_le_of_le_mul' (h : m ≤ k * n) : m / k ≤ n

Proof state:
case inl
m n : ℕ
h : m ≤ 0 * n
⊢ m / 0 ≤ n

Tactic:
simp

Result:
no goals

Proof state:
case inr
m n k : ℕ
h : m ≤ k * n
hk : k > 0
⊢ k * (m / k) ≤ k * n

Tactic:
calc
  k * (m / k) ≤ m % k + k * (m / k) := Nat.le_add_left _ _
  _ = m := mod_add_div _ _
  _ ≤ k * n := h

Result:
no goals

Proof state:
m n k : ℕ
h : m ≤ k * n
⊢ m / k ≤ n

Tactic:
obtain rfl | hk := k.eq_zero_or_pos

Result:
case inl
m n : ℕ
h : m ≤ 0 * n
⊢ m / 0 ≤ n

case inr
m n k : ℕ
h : m ≤ k * n
hk : k > 0
⊢ m / k ≤ n

Proof state:
case inr
m n k : ℕ
h : m ≤ k * n
hk : k > 0
⊢ m / k ≤ n

Tactic:
refine Nat.le_of_mul_le_mul_left ?_ hk

Result:
case inr
m n k : ℕ
h : m ≤ k * n
hk : k > 0
⊢ k * (m / k) ≤ k * n
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_comp_le_tsum_of_inj {β : Type*} {f : α → ℝ} (hf : Summable f) (hn : ∀ a, 0 ≤ f a)
    {i : β → α} (hi : Function.Injective i) : tsum (f ∘ i) ≤ tsum f

Proof state:
case intro
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable fun i => ↑(f i)
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)

Tactic:
rw [NNReal.summable_coe] at hf

Result:
case intro
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable f
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)

Proof state:
case intro
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable f
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)

Tactic:
simpa only [Function.comp_def, ← NNReal.coe_tsum] using NNReal.tsum_comp_le_tsum_of_inj hf hi

Result:
no goals

Proof state:
α : Type u_1
β : Type u_4
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ tsum (f ∘ i) ≤ tsum f

Tactic:
lift f to α → ℝ≥0 using hn

Result:
case intro
α : Type u_1
β : Type u_4
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable fun i => ↑(f i)
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
theorem LinearMap.rank_range_add_rank_ker (f : M →ₗ[R] M₁) :
    Module.rank R (LinearMap.range f) + Module.rank R (LinearMap.ker f) = Module.rank R M

Proof state:
R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
⊢ Module.rank R ↥(range f) + Module.rank R ↥(ker f) = Module.rank R M

Tactic:
rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank]

Result:
no goals

Proof state:
R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
⊢ Module.rank R ↥(range f) + Module.rank R ↥(ker f) = Module.rank R M

Tactic:
haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p)

Result:
R : Type u_1
M M₁ : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M₁
this : (p : Submodule R M) → DecidableEq (M ⧸ p)
⊢ Module.rank R ↥(range f) + Module.rank R ↥(ker f) = Module.rank R M
-- Mathlib/Analysis/RCLike/Basic.lean
theorem ratCast_re (q : ℚ) : re (q : K) = q

Proof state:
K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ re ↑q = ↑q

Tactic:
rw [← ofReal_ratCast, ofReal_re]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
lemma powers_le {n : M} {P : Submonoid M} : powers n ≤ P ↔ n ∈ P

Proof state:
M : Type u_1
inst✝ : Monoid M
n : M
P : Submonoid M
⊢ powers n ≤ P ↔ n ∈ P

Tactic:
simp [powers_eq_closure]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem scheme_eq_of_locallyRingedSpace_eq {X Y : Scheme.{u}}
    (H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace) : X = Y

Proof state:
case mk
Y : Scheme
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ } = Y

Tactic:
cases Y

Result:
case mk.mk
toLocallyRingedSpace✝¹ : LocallyRingedSpace
local_affine✝¹ :
  ∀ (x : ↑toLocallyRingedSpace✝¹.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝¹.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ }.toLocallyRingedSpace =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ } =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }

Proof state:
case mk.mk
toLocallyRingedSpace✝¹ : LocallyRingedSpace
local_affine✝¹ :
  ∀ (x : ↑toLocallyRingedSpace✝¹.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝¹.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ }.toLocallyRingedSpace =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝¹, local_affine := local_affine✝¹ } =
    { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }

Tactic:
congr

Result:
no goals

Proof state:
X Y : Scheme
H : X.toLocallyRingedSpace = Y.toLocallyRingedSpace
⊢ X = Y

Tactic:
cases X

Result:
case mk
Y : Scheme
toLocallyRingedSpace✝ : LocallyRingedSpace
local_affine✝ :
  ∀ (x : ↑toLocallyRingedSpace✝.toTopCat),
    ∃ U R, Nonempty (toLocallyRingedSpace✝.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))
H :
  { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ }.toLocallyRingedSpace =
    Y.toLocallyRingedSpace
⊢ { toLocallyRingedSpace := toLocallyRingedSpace✝, local_affine := local_affine✝ } = Y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) : n - m = 0

Proof state:
n m : Nat
h : n ≤ m
k : Nat
hk : n + k = m
⊢ n - m = 0

Tactic:
rw [← hk, Nat.sub_self_add]

Result:
no goals

Proof state:
n m : Nat
h : n ≤ m
⊢ n - m = 0

Tactic:
match le.dest h with
| ⟨k, hk⟩ => rw [← hk, Nat.sub_self_add]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/BigOperators.lean
lemma geo_series [Nontrivial β] (x : β) (hx1 : abv x < 1) :
    IsCauSeq abv fun n ↦ ∑ m ∈ range n, x ^ m

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

Tactic:
intro n _

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ |(1 - abv x ^ n) / (1 - abv x)| ≤ 1 / (1 - abv x)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ (1 - abv x ^ n) / (1 - abv x) ≤ 1 / (1 - abv x)

Tactic:
gcongr

Result:
case refine_1.hab
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ abv x ^ n ≤ 1

Tactic:
exact pow_le_one₀ (by positivity) hx1.le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m => ∑ n ∈ range m, abv (x ^ n)

Tactic:
simp only [abv_pow abv, geom_sum_eq hx1']

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
⊢ IsCauSeq abs fun m => (abv x ^ m - 1) / (abv x - 1)
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
@[simp]
lemma lift_comp_eqToHom_iff {R S S' : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S') :
    p.IsHomLift (f ≫ eqToHom h) φ ↔ p.IsHomLift f φ where
  mp := fun hφ' => by subst h; simpa using hφ'
  mpr := fun _ => inferInstance

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S S' : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
h : S = S'
hφ' : p.IsHomLift (f ≫ eqToHom h) φ
⊢ p.IsHomLift f φ

Tactic:
subst h

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
hφ' : p.IsHomLift (f ≫ eqToHom ⋯) φ
⊢ p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
hφ' : p.IsHomLift (f ≫ eqToHom ⋯) φ
⊢ p.IsHomLift f φ

Tactic:
simpa using hφ'

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem iff_not_exists_isMinBadSeq (rk : α → ℕ) {s : Set α} :
    s.PartiallyWellOrderedOn r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ n, IsMinBadSeq r rk s n f

Proof state:
case mpr.intro.intro
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x

Tactic:
exact ⟨f, hf1⟩

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ¬∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]

Result:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Proof state:
case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x

Tactic:
rintro ⟨f, hf1, -⟩

Result:
case mpr.intro.intro
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x

Proof state:
case mp
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
apply exists_min_bad_of_exists_bad

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) ↔ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
constructor

Result:
case mp
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ x, IsBadSeq r s x) → ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.iInf_Prop {α} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α]
    (p : Prop) {f : δ → α} (hf : Measurable f) : Measurable fun b => ⨅ _ : p, f b

Proof state:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b => if h : p then f b else sInf ∅

Tactic:
split_ifs with h

Result:
case pos
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable fun b => f b

case neg
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable fun b => sInf ∅

Proof state:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b => ⨅ (_ : p), f b

Tactic:
simp_rw [ciInf_eq_ite]

Result:
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
⊢ Measurable fun b => if h : p then f b else sInf ∅

Proof state:
case neg
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : ¬p
⊢ Measurable fun b => sInf ∅

Tactic:
exact measurable_const

Result:
no goals

Proof state:
case pos
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable fun b => f b

Tactic:
exact hf

Result:
no goals