harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/Basic.lean
theorem invVal_isEmpty {l r : Type u} {b} (L R IHl IHr) (i : InvTy l r b) (x) [IsEmpty l]
    [IsEmpty r] : invVal L R IHl IHr x i = 0

Proof state:
case left₁
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : r
a✝ : InvTy l r false
⊢ invVal L R IHl IHr x (InvTy.left₁ a a✝) = 0

case left₂
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : l
a✝ : InvTy l r true
⊢ invVal L R IHl IHr x (InvTy.left₂ a a✝) = 0

case right₁
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : l
a✝ : InvTy l r false
⊢ invVal L R IHl IHr x (InvTy.right₁ a a✝) = 0

case right₂
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : r
a✝ : InvTy l r true
⊢ invVal L R IHl IHr x (InvTy.right₂ a a✝) = 0

Tactic:
all_goals exact isEmptyElim a

Result:
no goals

Proof state:
l r : Type u
b : Bool
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
i : InvTy l r b
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
⊢ invVal L R IHl IHr x i = 0

Tactic:
obtain - | a | a | a | a := i

Result:
case zero
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
⊢ invVal L R IHl IHr x InvTy.zero = 0

case left₁
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : r
a✝ : InvTy l r false
⊢ invVal L R IHl IHr x (InvTy.left₁ a a✝) = 0

case left₂
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : l
a✝ : InvTy l r true
⊢ invVal L R IHl IHr x (InvTy.left₂ a a✝) = 0

case right₁
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : l
a✝ : InvTy l r false
⊢ invVal L R IHl IHr x (InvTy.right₁ a a✝) = 0

case right₂
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : r
a✝ : InvTy l r true
⊢ invVal L R IHl IHr x (InvTy.right₂ a a✝) = 0

Proof state:
case right₂
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
a : r
a✝ : InvTy l r true
⊢ invVal L R IHl IHr x (InvTy.right₂ a a✝) = 0

Tactic:
exact isEmptyElim a

Result:
no goals

Proof state:
case zero
l r : Type u
L : l → PGame
R : r → PGame
IHl : l → PGame
IHr : r → PGame
x : PGame
inst✝¹ : IsEmpty l
inst✝ : IsEmpty r
⊢ invVal L R IHl IHr x InvTy.zero = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1)

Proof state:
case inr
x : Nat
p : x % 2 = 1
⊢ x.testBit 0 = decide (x % 2 = 1)

Tactic:
simp [testBit, p]

Result:
no goals

Proof state:
x : Nat
⊢ x.testBit 0 = decide (x % 2 = 1)

Tactic:
cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_natCast_nonneg (n : ℕ) : 0 ≤ log n

Proof state:
n : ℕ
hn : ¬n = 0
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn

Result:
n : ℕ
hn : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n

Proof state:
n : ℕ
hn : n = 0
⊢ 0 ≤ log ↑n

Tactic:
simp [hn]

Result:
no goals

Proof state:
n : ℕ
⊢ 0 ≤ log ↑n

Tactic:
if hn : n = 0 then
  simp [hn]
else
  have : (1 : ℝ) ≤ n := mod_cast Nat.one_le_of_lt <| Nat.pos_of_ne_zero hn
  exact log_nonneg this

Result:
no goals

Proof state:
n : ℕ
hn : ¬n = 0
this : 1 ≤ ↑n
⊢ 0 ≤ log ↑n

Tactic:
exact log_nonneg this

Result:
no goals
-- Mathlib/Analysis/Calculus/Rademacher.lean
theorem LipschitzWith.ae_differentiableAt {f : E → F} (h : LipschitzWith C f) :
    ∀ᵐ x ∂μ, DifferentiableAt ℝ f x

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
h : LipschitzOnWith C f univ
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem

Result:
no goals

Proof state:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
h : LipschitzWith C f
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
rw [← lipschitzOnWith_univ] at h

Result:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
h : LipschitzOnWith C f univ
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
-- Mathlib/Data/Matroid/Sum.lean
lemma disjointSum_comm {h} : M.disjointSum N h = N.disjointSum M h.symm

Proof state:
case hE.h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
x✝ : α
⊢ x✝ ∈ (M.disjointSum N h).E ↔ x✝ ∈ (N.disjointSum M ⋯).E

Tactic:
simp [union_comm]

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
⊢ M.disjointSum N h = N.disjointSum M ⋯

Tactic:
ext

Result:
case hE.h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
x✝ : α
⊢ x✝ ∈ (M.disjointSum N h).E ↔ x✝ ∈ (N.disjointSum M ⋯).E

case h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I✝ : Set α
a✝ : I✝ ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I✝ ↔ (N.disjointSum M ⋯).Indep I✝

Proof state:
case h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I✝ : Set α
a✝ : I✝ ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I✝ ↔ (N.disjointSum M ⋯).Indep I✝

Tactic:
repeat simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
  fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

Result:
no goals

Proof state:
case h
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I✝ : Set α
a✝ : I✝ ⊆ (M.disjointSum N h).E
⊢ (M.disjointSum N h).Indep I✝ ↔ (N.disjointSum M ⋯).Indep I✝

Tactic:
simpa [union_comm] using ⟨fun ⟨m, n, h⟩ ↦ ⟨n, m, M.E.union_comm N.E ▸ h⟩,
fun ⟨n, m, h⟩ ↦ ⟨m, n, M.E.union_comm N.E ▸ h⟩⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_unitsSMul_self (w : ι → Rˣ) : e.det (e.unitsSMul w) = ∏ i, (w i : R)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
⊢ e.det ⇑(e.unitsSMul w) = ∏ i : ι, ↑(w i)

Tactic:
simp [Basis.det_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Basic.lean
theorem map_id : map (LinearMap.id : V →ₗ[K] V) (LinearEquiv.refl K V).injective = id

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ map LinearMap.id ⋯ = id

Tactic:
ext ⟨v⟩

Result:
case h.mk
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id ⋯ (Quot.mk (⇑(projectivizationSetoid K V)) v) = id (Quot.mk (⇑(projectivizationSetoid K V)) v)

Proof state:
case h.mk
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id ⋯ (Quot.mk (⇑(projectivizationSetoid K V)) v) = id (Quot.mk (⇑(projectivizationSetoid K V)) v)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
private lemma cobounded_eq_aux :
    cobounded (CStarMatrix m n A) = @cobounded _ Pi.instBornology

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
this : cobounded (CStarMatrix m n A) = Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A))
⊢ cobounded (CStarMatrix m n A) = cobounded (m → n → A)

Tactic:
exact this.trans Filter.comap_id

Result:
no goals

Proof state:
case refine_1
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ cobounded (CStarMatrix m n A) ≤ Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A))

Tactic:
exact antilipschitzWith_toMatrixAux.tendsto_cobounded.le_comap

Result:
no goals

Proof state:
case refine_2
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A)) ≤ cobounded (CStarMatrix m n A)

Tactic:
exact lipschitzWith_toMatrixAux.comap_cobounded_le

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ cobounded (CStarMatrix m n A) = Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A))

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ cobounded (CStarMatrix m n A) ≤ Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A))

case refine_2
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A)) ≤ cobounded (CStarMatrix m n A)
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.epi_f (hS : S.Exact) (hg : S.g = 0) : Epi S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
⊢ Epi S.f

Tactic:
have := hS.hasHomology

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this : S.HasHomology
⊢ Epi S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ S.pOpcycles = 0

Tactic:
rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ Epi S.f

Tactic:
have : S.pOpcycles = 0 := by rw [← cancel_mono S.fromOpcycles, zero_comp, p_fromOpcycles, hg]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ Epi S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this : S.HasHomology
⊢ Epi S.f

Tactic:
have := hS.mono_fromOpcycles

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ Epi S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ Epi S.f

Tactic:
apply Preadditive.epi_of_cancel_zero

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ ∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
⊢ ∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0

Tactic:
intro A x₂ hx₂

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 0
⊢ x₂ = 0

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 0
⊢ x₂ = 0

Tactic:
rw [← S.p_descOpcycles x₂ hx₂, this, zero_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
lemma sub (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U]

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : x₁ ≡ y₁ [SMOD U]
hxy₂ : x₂ ≡ y₂ [SMOD U]
⊢ x₁ - x₂ ≡ y₁ - y₂ [SMOD U]

Tactic:
rw [SModEq.def] at hxy₁ hxy₂ ⊢

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk (x₁ - x₂) = Submodule.Quotient.mk (y₁ - y₂)

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x₁ x₂ y₁ y₂ : M
hxy₁ : Submodule.Quotient.mk x₁ = Submodule.Quotient.mk y₁
hxy₂ : Submodule.Quotient.mk x₂ = Submodule.Quotient.mk y₂
⊢ Submodule.Quotient.mk (x₁ - x₂) = Submodule.Quotient.mk (y₁ - y₂)

Tactic:
simp_rw [Quotient.mk_sub, hxy₁, hxy₂]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem ker_toSpanSingleton_one_sub_eq_span :
    LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e)) = Ideal.span {e}

Proof state:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ LinearMap.ker (LinearMap.toSpanSingleton R R (1 - e)) = Ideal.span {e}

Tactic:
rw [ker_toSpanSingleton_eq_span he.one_sub, sub_sub_cancel]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma divInt_div_divInt (n₁ d₁ n₂ d₂) :
    (n₁ /. d₁) / (n₂ /. d₂) = (n₁ * d₂) /. (d₁ * n₂)

Proof state:
n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
rw [div_def, inv_divInt, divInt_mul_divInt']

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `le_div_iff₀'` for a version with multiplication on the other side. -/
lemma le_div_iff₀ (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hc : 0 < c
⊢ a ≤ b / c ↔ a * c ≤ b

Tactic:
rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem closure_singleton (x) : closure ({x} : Set (PrimeSpectrum R)) = zeroLocus x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ closure {x} = zeroLocus ↑x.asIdeal

Tactic:
rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_injective_of_le {m n : ℕ} [nzm : NeZero m] (h : m ≤ n) :
    Function.Injective (@cast (ZMod n) _ m)

Proof state:
case succ.mk.mk.h
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ↑⟨x, hx⟩ = ↑⟨y, hy⟩

Tactic:
exact f

Result:
no goals

Proof state:
m n : ℕ
nzm : NeZero m
h : m ≤ n
⊢ Injective cast

Tactic:
cases m with
| zero => cases nzm; simp_all
| succ m =>
  rintro ⟨x, hx⟩ ⟨y, hy⟩ f
  simp only [cast, val, natCast_eq_natCast_iff',
    Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f
  apply Fin.ext
  exact f

Result:
no goals

Proof state:
case succ
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
⊢ Injective cast

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ f

Result:
case succ.mk.mk
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : cast ⟨x, hx⟩ = cast ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Proof state:
case succ.mk.mk
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : cast ⟨x, hx⟩ = cast ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simp only [cast, val, natCast_eq_natCast_iff',
  Nat.mod_eq_of_lt (hx.trans_le h), Nat.mod_eq_of_lt (hy.trans_le h)] at f

Result:
case succ.mk.mk
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Proof state:
case zero
n : ℕ
nzm : NeZero 0
h : 0 ≤ n
⊢ Injective cast

Tactic:
cases nzm

Result:
case zero.mk
n : ℕ
h : 0 ≤ n
out✝ : 0 ≠ 0
⊢ Injective cast

Proof state:
case zero.mk
n : ℕ
h : 0 ≤ n
out✝ : 0 ≠ 0
⊢ Injective cast

Tactic:
simp_all

Result:
no goals

Proof state:
case succ.mk.mk
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
apply Fin.ext

Result:
case succ.mk.mk.h
n m : ℕ
nzm : NeZero (m + 1)
h : m + 1 ≤ n
x : ℕ
hx : x < m + 1
y : ℕ
hy : y < m + 1
f : x = y
⊢ ↑⟨x, hx⟩ = ↑⟨y, hy⟩
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem sign_of_cycleType (f : Perm α) :
    sign f = (-1 : ℤˣ) ^ (f.cycleType.sum + Multiset.card f.cycleType)

Proof state:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n => -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (Multiset.map (fun n => -(-1) ^ n) (a ::ₘ s)).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]

Result:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n => -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (-1) ^ (s.sum + s.card) = (-1) ^ (a + s.sum + (s.card + 1))

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n => -(-1) ^ n) f.cycleType).prod = (-1) ^ (f.cycleType.sum + f.cycleType.card)

Tactic:
induction' f.cycleType using Multiset.induction_on with a s ihs

Result:
case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n => -(-1) ^ n) 0).prod = (-1) ^ (Multiset.sum 0 + card 0)

case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n => -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (Multiset.map (fun n => -(-1) ^ n) (a ::ₘ s)).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Proof state:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n => -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (-1) ^ (s.sum + s.card) = (-1) ^ (a + s.sum + (s.card + 1))

Tactic:
simp only [pow_add, pow_one, mul_neg_one, neg_mul, mul_neg, mul_assoc, mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ sign f = (-1) ^ (f.cycleType.sum + f.cycleType.card)

Tactic:
rw [sign_of_cycleType']

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n => -(-1) ^ n) f.cycleType).prod = (-1) ^ (f.cycleType.sum + f.cycleType.card)

Proof state:
case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ (Multiset.map (fun n => -(-1) ^ n) 0).prod = (-1) ^ (Multiset.sum 0 + card 0)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem next_eq (f : Hom C₁ C₂) {i j : ι} (w : c.Rel i j) :
    f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i : ι
w : c.Rel i (c.next i)
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv

Tactic:
simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv

Tactic:
obtain rfl := c.next_eq' w

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i : ι
w : c.Rel i (c.next i)
⊢ f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_neg (f : E →SL[σ₁₂] F) : ‖-f‖ = ‖f‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
⊢ ‖-f‖ = ‖f‖

Tactic:
simp only [norm_def, neg_apply, norm_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- The difference `log (1-z)⁻¹ - z` is bounded by `‖z‖^2/(2*(1-‖z‖))` when `‖z‖ < 1`. -/
lemma norm_log_one_sub_inv_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

Proof state:
case h.e'_3.h.e'_3
z : ℂ
hz : ‖z‖ < 1
⊢ log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (1 + 1) (-z)

Tactic:
simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]

Result:
no goals

Proof state:
case h.e'_4.h.e'_6
z : ℂ
hz : ‖z‖ < 1
⊢ 2 = ↑1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 - z)⁻¹ - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

Tactic:
convert norm_log_one_sub_inv_add_logTaylor_neg_le 1 hz using 2

Result:
case h.e'_3.h.e'_3
z : ℂ
hz : ‖z‖ < 1
⊢ log (1 - z)⁻¹ - z = log (1 - z)⁻¹ + logTaylor (1 + 1) (-z)

case h.e'_4.h.e'_6
z : ℂ
hz : ‖z‖ < 1
⊢ 2 = ↑1 + 1
-- Mathlib/Order/WithBot.lean
lemma untop_lt_iff (hx : x ≠ ⊤) : x.untop hx < b ↔ x < b

Proof state:
α : Type u_1
b : α
inst✝ : LT α
x : WithTop α
hx : x ≠ ⊤
⊢ x.untop hx < b ↔ x < ↑b

Tactic:
lift x to α using id hx

Result:
case intro
α : Type u_1
b : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊤
⊢ (↑x).untop hx < b ↔ ↑x < ↑b

Proof state:
case intro
α : Type u_1
b : α
inst✝ : LT α
x : α
hx : ↑x ≠ ⊤
⊢ (↑x).untop hx < b ↔ ↑x < ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem mem_of_mem_inter_right (h : a ∈ l₁ ∩ l₂) : a ∈ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂

Tactic:
simpa using of_mem_filter h

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem add_moveLeft_inr (x : PGame) {y : PGame} (i) :
    (x + y).moveLeft (toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i

Proof state:
case mk
y : PGame
i : y.LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveLeft (toLeftMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + y.moveLeft i

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + (mk α✝ β✝ a✝¹ a✝).moveLeft i

Proof state:
x y : PGame
i : y.LeftMoves
⊢ (x + y).moveLeft (toLeftMovesAdd (Sum.inr i)) = x + y.moveLeft i

Tactic:
cases x

Result:
case mk
y : PGame
i : y.LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveLeft (toLeftMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + y.moveLeft i

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + (mk α✝ β✝ a✝¹ a✝).moveLeft i

Tactic:
rfl

Result:
no goals