harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDerivAux_nonneg (hκη : κ ≤ η) {a : α} {x : γ} : 0 ≤ rnDerivAux κ η a x

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ if hα : Countable α then ((∂κ a/∂η a) x).toReal else (κ.map fun a => (a, ())).density η a x univ

Tactic:
split_ifs with hα

Result:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : Countable α
⊢ 0 ≤ ((∂κ a/∂η a) x).toReal

case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
⊢ 0 ≤ (κ.map fun a => (a, ())).density η a x univ

Proof state:
case pos
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : Countable α
⊢ 0 ≤ ((∂κ a/∂η a) x).toReal

Tactic:
exact ENNReal.toReal_nonneg

Result:
no goals

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
⊢ 0 ≤ (κ.map fun a => (a, ())).density η a x univ

Tactic:
have := hαγ.countableOrCountablyGenerated.resolve_left hα

Result:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ 0 ≤ (κ.map fun a => (a, ())).density η a x univ

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ κ.rnDerivAux η a x

Tactic:
rw [rnDerivAux]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ if hα : Countable α then ((∂κ a/∂η a) x).toReal else (κ.map fun a => (a, ())).density η a x univ

Proof state:
case neg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ 0 ≤ (κ.map fun a => (a, ())).density η a x univ

Tactic:
exact density_nonneg ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem rank_sup_le_of_isAlgebraic
    (halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
    Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K E1 * Module.rank K E2

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

Tactic:
have := E1.toSubalgebra.rank_sup_le_of_free E2.toSubalgebra

Result:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2
this :
  Module.rank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

Proof state:
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic K ↥E1 ∨ Algebra.IsAlgebraic K ↥E2
this :
  Module.rank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

Tactic:
rwa [← sup_toSubalgebra_of_isAlgebraic E1 E2 halg] at this

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma removeNth_insertNth (p : Fin (n + 1)) (a : α p) (f : ∀ i, α (succAbove p i)) :
    removeNth p (insertNth p a f) = f

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ p.removeNth (p.insertNth a f) = f

Tactic:
ext

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.removeNth (p.insertNth a f) x✝ = f x✝

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.insertNth a f (p.succAbove x✝) = f x✝

Tactic:
simp

Result:
no goals

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.removeNth (p.insertNth a f) x✝ = f x✝

Tactic:
unfold removeNth

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
a : α p
f : (i : Fin n) → α (p.succAbove i)
x✝ : Fin n
⊢ p.insertNth a f (p.succAbove x✝) = f x✝
-- Mathlib/Algebra/CharP/Reduced.lean
theorem ExpChar.pow_prime_pow_mul_eq_one_iff (p k m : ℕ) [ExpChar R p] (x : R) :
    x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

Proof state:
case h.e'_1.h.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p k) 1 = 1

Tactic:
apply map_one

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ x ^ (p ^ k * m) = 1 ↔ x ^ m = 1

Tactic:
rw [pow_mul']

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (x ^ m) ^ p ^ k = 1 ↔ x ^ m = 1

Tactic:
convert ← (iterateFrobenius_inj R p k).eq_iff

Result:
case h.e'_1.h.e'_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
x : R
⊢ (iterateFrobenius R p k) 1 = 1
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean
theorem opNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ ≤ 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
R : Type u_3
inst✝³ : NormedField R
inst✝² : NormedAlgebra 𝕜 R
inst✝¹ : NormedSpace R E
inst✝ : IsScalarTower 𝕜 R E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ 1 * ‖x‖

Tactic:
simp_rw [one_mul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
R : Type u_3
inst✝³ : NormedField R
inst✝² : NormedAlgebra 𝕜 R
inst✝¹ : NormedSpace R E
inst✝ : IsScalarTower 𝕜 R E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
R : Type u_3
inst✝³ : NormedField R
inst✝² : NormedAlgebra 𝕜 R
inst✝¹ : NormedSpace R E
inst✝ : IsScalarTower 𝕜 R E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ ‖x‖

Tactic:
exact opNorm_lsmul_apply_le _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
R : Type u_3
inst✝³ : NormedField R
inst✝² : NormedAlgebra 𝕜 R
inst✝¹ : NormedSpace R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ‖lsmul 𝕜 R‖ ≤ 1

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun x => ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
R : Type u_3
inst✝³ : NormedField R
inst✝² : NormedAlgebra 𝕜 R
inst✝¹ : NormedSpace R E
inst✝ : IsScalarTower 𝕜 R E
x : R
⊢ ‖(lsmul 𝕜 R) x‖ ≤ 1 * ‖x‖
-- Mathlib/Algebra/Order/Group/OrderIso.lean
theorem OrderIso.mulLeft_symm (a : α) : (OrderIso.mulLeft a).symm = OrderIso.mulLeft a⁻¹

Proof state:
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a x : α
⊢ (mulLeft a).symm x = (mulLeft a⁻¹) x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a : α
⊢ (mulLeft a).symm = mulLeft a⁻¹

Tactic:
ext x

Result:
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a x : α
⊢ (mulLeft a).symm x = (mulLeft a⁻¹) x
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem neg (q : ℚ) : padicNorm p (-q) = padicNorm p q :=
  if hq : q = 0 then by simp [hq] else by simp [padicNorm, hq]

Proof state:
p : ℕ
q : ℚ
hq : ¬q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
simp [padicNorm, hq]

Result:
no goals

Proof state:
p : ℕ
q : ℚ
hq : q = 0
⊢ padicNorm p (-q) = padicNorm p q

Tactic:
simp [hq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_replicate : (replicate n a).map f = replicate n (f a)

Proof state:
case h
n✝ : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
n : Nat
⊢ Option.map f (if n < n✝ then some a else none) = if n < n✝ then some (f a) else none

Tactic:
split <;> simp

Result:
no goals

Proof state:
case h
n✝ : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
n : Nat
⊢ (map f (replicate n✝ a))[n]? = (replicate n✝ (f a))[n]?

Tactic:
simp only [getElem?_map, getElem?_replicate]

Result:
case h
n✝ : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
n : Nat
⊢ Option.map f (if n < n✝ then some a else none) = if n < n✝ then some (f a) else none

Proof state:
n : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f (replicate n a) = replicate n (f a)

Tactic:
ext1 n

Result:
case h
n✝ : Nat
α✝¹ : Type u_1
a : α✝¹
α✝ : Type u_2
f : α✝¹ → α✝
n : Nat
⊢ (map f (replicate n✝ a))[n]? = (replicate n✝ (f a))[n]?
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem mem_range' {n} : m ∈ range' s n step ↔ ∃ i < n, m = s + step * i

Proof state:
s step m n : Nat
⊢ m ∈ range' s n step ↔ ∃ i, i < n ∧ m = s + step * i

Tactic:
simp [range', Array.mem_range']

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem subsemiringClosure_eq_closure : M.subsemiringClosure = Subsemiring.closure (M : Set R)

Proof state:
case h.refine_1.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2

Tactic:
exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ x✝ ∈ M.subsemiringClosure ↔ x✝ ∈ Subsemiring.closure ↑M

Tactic:
refine
  ⟨fun hx => ?_, fun hx =>
    (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩
<;> rintro - ⟨H1, rfl⟩
<;> rintro - ⟨H2, rfl⟩

Result:
case h.refine_1.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ M.subsemiringClosure
H1 : Subsemiring R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ x✝ ∈ (fun h => ↑H1) H2

case h.refine_2.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2

Proof state:
case h.refine_2.intro.intro
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
hx : x✝ ∈ Subsemiring.closure ↑M
s : R
sM : s ∈ ↑M
H1 : AddSubmonoid R
H2 : H1 ∈ {S | ↑M ⊆ ↑S}
⊢ s ∈ (fun h => ↑H1) H2

Tactic:
exact H2 sM

Result:
no goals

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure = Subsemiring.closure ↑M

Tactic:
ext

Result:
case h
R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
x✝ : R
⊢ x✝ ∈ M.subsemiringClosure ↔ x✝ ∈ Subsemiring.closure ↑M
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem iSup_iterate_eq_nfp (f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}) :
    ⨆ n : ℕ, f^[n] a = nfp f a

Proof state:
case a.a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ n, f^[n] a

Tactic:
exact Ordinal.le_iSup _ _

Result:
no goals

Proof state:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ nfp f a

Tactic:
rw [Ordinal.iSup_le_iff]

Result:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a

Proof state:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a

Tactic:
exact Ordinal.le_iSup _ _

Result:
no goals

Proof state:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a

Tactic:
intro n

Result:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Proof state:
case a.a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : List Unit), List.foldr (fun x => f) a i ≤ ⨆ n, f^[n] a

Tactic:
intro l

Result:
case a.a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ ⨆ n, f^[n] a

Proof state:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← List.length_replicate n Unit.unit, ← List.foldr_const f a]

Result:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
n : ℕ
⊢ List.foldr (fun x => f) a (List.replicate n ()) ≤ nfp f a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a = nfp f a

Tactic:
apply le_antisymm

Result:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ nfp f a

case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ nfp f a ≤ ⨆ n, f^[n] a

Proof state:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ nfp f a ≤ ⨆ n, f^[n] a

Tactic:
apply Ordinal.iSup_le

Result:
case a.a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : List Unit), List.foldr (fun x => f) a i ≤ ⨆ n, f^[n] a

Proof state:
case a.a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ List.foldr (fun x => f) a l ≤ ⨆ n, f^[n] a

Tactic:
rw [List.foldr_const f a l]

Result:
case a.a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
l : List Unit
⊢ f^[l.length] a ≤ ⨆ n, f^[n] a
-- Mathlib/Analysis/Normed/Group/Quotient.lean
theorem quotient_norm_neg {S : AddSubgroup M} (x : M ⧸ S) : ‖-x‖ = ‖x‖

Proof state:
case e_a.h.mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = x} → r ∈ norm '' {m | ↑m = -x}

Tactic:
rintro ⟨m, hm, rfl⟩

Result:
case e_a.h.mpr.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ ‖m‖ ∈ norm '' {m | ↑m = -x}

Proof state:
case e_a.h.mpr.intro.intro
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ ‖m‖ ∈ norm '' {m | ↑m = -x}

Tactic:
use -m

Result:
case h
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ -m ∈ {m | ↑m = -x} ∧ ‖-m‖ = ‖m‖

Proof state:
case h
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ -m ∈ {m | ↑m = -x} ∧ ‖-m‖ = ‖m‖

Tactic:
simpa [neg_eq_iff_eq_neg] using hm

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
⊢ ‖-x‖ = ‖x‖

Tactic:
simp only [AddSubgroup.quotient_norm_eq]

Result:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
⊢ sInf (norm '' {m | ↑m = -x}) = sInf (norm '' {m | ↑m = x})

Proof state:
case e_a.h
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} ↔ r ∈ norm '' {m | ↑m = x}

Tactic:
constructor <;> { rintro ⟨m, hm, rfl⟩; use -m; simpa [neg_eq_iff_eq_neg] using hm }

Result:
no goals

Proof state:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
⊢ sInf (norm '' {m | ↑m = -x}) = sInf (norm '' {m | ↑m = x})

Tactic:
congr 1 with r

Result:
case e_a.h
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} ↔ r ∈ norm '' {m | ↑m = x}
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.image_castSucc (n : ℕ) :
    (univ : Finset (Fin n)).image Fin.castSucc = {Fin.last n}ᶜ

Proof state:
n : ℕ
⊢ image castSucc univ = {last n}ᶜ

Tactic:
rw [← Fin.succAbove_last, Fin.image_succAbove_univ]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem le_floor_add_floor (a b : α) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ b - 1

Tactic:
rw [sub_le_iff_le_add', ← add_sub_assoc, sub_le_sub_iff_right]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ ≤ a + b

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ ↑⌊b⌋

Tactic:
refine le_trans ?_ (sub_one_lt_floor _).le

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ b - 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

Tactic:
rw [← sub_le_iff_le_add, le_floor, Int.cast_sub, sub_le_comm, Int.cast_sub, Int.cast_one]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ - 1 - a ≤ ↑⌊b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ ↑⌊a + b⌋ ≤ a + b

Tactic:
exact floor_le _

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Defs.lean
lemma one_add_le_one_sub_mul_one_add (h : a + b + b * c ≤ c) : 1 + a ≤ (1 - b) * (1 + c)

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : a + b + b * c ≤ c
⊢ 1 + a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, le_sub_iff_add_le, add_assoc, ← add_assoc a]

Result:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : a + b + b * c ≤ c
⊢ 1 + (a + b + b * c) ≤ 1 + c

Proof state:
α : Type u
inst✝ : OrderedRing α
a b c : α
h : a + b + b * c ≤ c
⊢ 1 + (a + b + b * c) ≤ 1 + c

Tactic:
gcongr

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
@[simp]
lemma count_sub (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t :=
  Quotient.inductionOn₂ s t <| by simp [List.count_diff]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ ∀ (a_1 b : List α), count a (⟦a_1⟧ - ⟦b⟧) = count a ⟦a_1⟧ - count a ⟦b⟧

Tactic:
simp [List.count_diff]

Result:
no goals
-- Mathlib/ModelTheory/Complexity.lean
theorem IsPrenex.relabel {m : ℕ} {φ : L.BoundedFormula α m} (h : φ.IsPrenex)
    (f : α → β ⊕ (Fin n)) : (φ.relabel f).IsPrenex :=
  IsPrenex.recOn h (fun h => (h.relabel f).isPrenex) (fun _ h => by simp [h.all])
    fun _ h => by simp [h.ex]

Proof state:
L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h✝ : φ.IsPrenex
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
x✝ : φ✝.IsPrenex
h : (BoundedFormula.relabel f φ✝).IsPrenex
⊢ (BoundedFormula.relabel f (∀'φ✝)).IsPrenex

Tactic:
simp [h.all]

Result:
no goals

Proof state:
L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h✝ : φ.IsPrenex
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
x✝ : φ✝.IsPrenex
h : (BoundedFormula.relabel f φ✝).IsPrenex
⊢ (BoundedFormula.relabel f (∃'φ✝)).IsPrenex

Tactic:
simp [h.ex]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem disjoint_univ_pi : Disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)

Proof state:
ι : Type u_1
α : ι → Type u_2
t₁ t₂ : (i : ι) → Set (α i)
⊢ Disjoint (univ.pi t₁) (univ.pi t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)

Tactic:
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem abs_im_le_norm (z : K) : |im z| ≤ ‖z‖

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| ≤ ‖z‖

Tactic:
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ normSq z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ normSq z

Tactic:
apply im_sq_le_normSq

Result:
no goals
-- Mathlib/RingTheory/Ideal/Basic.lean
theorem sum_pow_mem_span_pow {ι} (s : Finset ι) (f : ι → α) (n : ℕ) :
    (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' s)

Proof state:
α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' ↑s)

Tactic:
simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map,
  Finset.coe_image, Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommSemiring α
ι : Type u_5
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (s.card * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' ↑s)

Tactic:
classical
simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map,
  Finset.coe_image, Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
@[simp] lemma cast_nonpos : (n : α) ≤ 0 ↔ n = 0

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n ≤ 0 ↔ n = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ 0 ↔ n = 0

Tactic:
norm_cast

Result:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ n ≤ 0 ↔ n = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_map (f : α → γ) (g : β → δ) :
    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
  | [], _ => rfl
  | _, [] => by simp only [map, zip_nil_right]
  | _ :: _, _ :: _ => by simp only [map, zip_cons_cons, zip_map, Prod.map]

Proof state:
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
x✝ : List α
⊢ (map f x✝).zip (map g []) = map (Prod.map f g) (x✝.zip [])

Tactic:
simp only [map, zip_nil_right]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
β : Type u_3
δ : Type u_4
f : α → γ
g : β → δ
head✝¹ : α
tail✝¹ : List α
head✝ : β
tail✝ : List β
⊢ (map f (head✝¹ :: tail✝¹)).zip (map g (head✝ :: tail✝)) = map (Prod.map f g) ((head✝¹ :: tail✝¹).zip (head✝ :: tail✝))

Tactic:
simp only [map, zip_cons_cons, zip_map, Prod.map]

Result:
no goals