harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuation_of_mk' {r : R} {s : nonZeroDivisors R} :
    v.valuation K (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation s

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s)⁻¹ =
    (v.intValuation ↑s)⁻¹

Tactic:
rw [Units.val_inv_eq_inv_val, inv_inj]

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s) = v.intValuation ↑s

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s)⁻¹ =
      (v.intValuation ↑s)⁻¹ ∨
    ↑v.intValuation.toMonoidWithZeroHom r = 0

Tactic:
left

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s)⁻¹ =
    (v.intValuation ↑s)⁻¹

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s) = v.intValuation ↑s

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ (valuation K v) (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation ↑s

Tactic:
erw [valuation_def, (IsLocalization.toLocalizationMap (nonZeroDivisors R) K).lift_mk',
  div_eq_mul_inv, mul_eq_mul_left_iff]

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
s : ↥(nonZeroDivisors R)
⊢ ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict (nonZeroDivisors R)) ⋯) s)⁻¹ =
      (v.intValuation ↑s)⁻¹ ∨
    ↑v.intValuation.toMonoidWithZeroHom r = 0
-- Mathlib/Topology/Constructible.lean
lemma IsRetrocompact.finsetSup {ι : Type*} {s : Finset ι} {t : ι → Set X}
    (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.sup t)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

Tactic:
induction s using Finset.cons_induction with
| empty => simp
| cons i s ih hi =>
  rw [Finset.sup_cons]
  exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

Result:
no goals

Proof state:
case empty
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
ht : ∀ i ∈ ∅, IsRetrocompact (t i)
⊢ IsRetrocompact (∅.sup t)

Tactic:
simp

Result:
no goals

Proof state:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact ((Finset.cons i s ih).sup t)

Tactic:
rw [Finset.sup_cons]

Result:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊔ s.sup t)

Proof state:
case cons
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (t i_1)
⊢ IsRetrocompact (t i ⊔ s.sup t)

Tactic:
exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldl_rev (f : Fin n → α → α) (x) :
    foldl n (fun x i => f i.rev x) x = foldr n f x

Proof state:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), foldl n (fun x i => f i.rev x) x = foldr n f x
f : Fin (n + 1) → α → α
x : α
⊢ foldl n (fun x i => f i.succ.rev x) (f (rev 0) x) = foldl n (fun x i => f i.rev.castSucc x) (f (last n) x)

Tactic:
simp [rev_succ]

Result:
no goals

Proof state:
case zero
α : Sort u_1
f : Fin 0 → α → α
x : α
⊢ foldl 0 (fun x i => f i.rev x) x = foldr 0 f x

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), foldl n (fun x i => f i.rev x) x = foldr n f x
f : Fin (n + 1) → α → α
x : α
⊢ foldl (n + 1) (fun x i => f i.rev x) x = foldr (n + 1) f x

Tactic:
rw [foldl_succ, foldr_succ_last, ← ih]

Result:
case succ
α : Sort u_1
n : Nat
ih : ∀ (f : Fin n → α → α) (x : α), foldl n (fun x i => f i.rev x) x = foldr n f x
f : Fin (n + 1) → α → α
x : α
⊢ foldl n (fun x i => f i.succ.rev x) (f (rev 0) x) = foldl n (fun x i => f i.rev.castSucc x) (f (last n) x)

Proof state:
n : Nat
α : Sort u_1
f : Fin n → α → α
x : α
⊢ foldl n (fun x i => f i.rev x) x = foldr n f x

Tactic:
induction n generalizing x with
| zero => simp
| succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem LieSubalgebra.ad_comp_incl_eq (K : LieSubalgebra R L) (x : K) :
    (ad R L ↑x).comp (K.incl : K →ₗ[R] L) = (K.incl : K →ₗ[R] L).comp (ad R K x)

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x y : ↥K
⊢ ((ad R L) ↑x ∘ₗ ↑K.incl) y = (↑K.incl ∘ₗ (ad R ↥K) x) y

Tactic:
simp only [ad_apply, LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp,
  LieSubalgebra.coe_bracket, Function.comp_apply]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
⊢ (ad R L) ↑x ∘ₗ ↑K.incl = ↑K.incl ∘ₗ (ad R ↥K) x

Tactic:
ext y

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x y : ↥K
⊢ ((ad R L) ↑x ∘ₗ ↑K.incl) y = (↑K.incl ∘ₗ (ad R ↥K) x) y
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc (attr := simp)]
lemma Scheme.homOfLE_homOfLE (X : Scheme.{u}) {U V W : X.Opens} (e₁ : U ≤ V) (e₂ : V ≤ W) :
    X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE (e₁.trans e₂)

Proof state:
X : Scheme
U V W : X.Opens
e₁ : U ≤ V
e₂ : V ≤ W
⊢ X.homOfLE e₁ ≫ X.homOfLE e₂ = X.homOfLE ⋯

Tactic:
rw [← cancel_mono W.ι, Category.assoc, Scheme.homOfLE_ι, Scheme.homOfLE_ι, Scheme.homOfLE_ι]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_two : cos (π / 2) = 0

Proof state:
⊢ cos (π / 2) = 0

Tactic:
rw [Real.pi, mul_div_cancel_left₀ _ (two_ne_zero' ℝ)]

Result:
⊢ cos (Classical.choose exists_cos_eq_zero) = 0

Proof state:
⊢ cos (Classical.choose exists_cos_eq_zero) = 0

Tactic:
exact (Classical.choose_spec exists_cos_eq_zero).2

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem map_congr {f g : α → β} {s : Sym2 α} (h : ∀ x ∈ s, f x = g x) : map f s = map g s

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
⊢ map f s = map g s

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s

Proof state:
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ ∃ a ∈ s, f a = g w

Tactic:
exact ⟨w, hw, by simp [hw, h]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ f w = g w

Tactic:
simp [hw, h]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ y ∈ map f s ↔ y ∈ map g s

Tactic:
simp only [mem_map]

Result:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) ↔ ∃ a ∈ s, g a = y

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y

Tactic:
rintro ⟨w, hw, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
w : α
hw : w ∈ s
⊢ ∃ a ∈ s, f a = g w
-- Mathlib/Analysis/Seminorm.lean
lemma uniformity_eq_of_hasBasis
    {ι} [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul 𝕜 E]
    {p' : ι → Prop} {s : ι → Set E} (p : Seminorm 𝕜 E) (hb : (𝓝 0 : Filter E).HasBasis p' s)
    (h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0) (h₂ : ∀ i, p' i → ∃ r > 0, p.ball 0 r ⊆ s i) :
    𝓤 E = ⨅ r > 0, 𝓟 {x | p (x.1 - x.2) < r}

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
ι : Sort u_12
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : (𝓝 0).HasBasis p' s
h₁ : ∃ r, p.closedBall 0 r ∈ 𝓝 0
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ r, ⨅ (_ : r > 0), 𝓟 {x | p (x.1 - x.2) < r}

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_strictAnti₀` for the implication from right-to-left with one fewer assumption. -/
lemma inv_lt_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b⁻¹ ↔ b < a

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b : G₀
inst✝¹ : MulPosStrictMono G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean
@[simp, norm_cast]
lemma coe_iSup {ι : Sort*} (f : ι → G.Finsubgraph) : ⨆ i, f i = (⨆ i, f i : G.Subgraph)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
rw [iSup, coe_sSup, iSup_range]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem natDegree_mem_support_of_nonzero (H : p ≠ 0) : p.natDegree ∈ p.support

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.coeff p.natDegree ≠ 0

Tactic:
exact (not_congr leadingCoeff_eq_zero).mpr H

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.natDegree ∈ p.support

Tactic:
rw [mem_support_iff]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
H : p ≠ 0
⊢ p.coeff p.natDegree ≠ 0
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem Wequiv.abs' (x y : q.P.W) (h : QPF.abs x.dest = QPF.abs y.dest) : Wequiv x y

Proof state:
case mk.mk.a
F : Type u → Type u
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ QPF.abs ⟨a✝¹, f✝¹⟩ = QPF.abs ⟨a✝, f✝⟩

Tactic:
apply h

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
x y : (P F).W
h : QPF.abs x.dest = QPF.abs y.dest
⊢ Wequiv x y

Tactic:
cases x

Result:
case mk
F : Type u → Type u
q : QPF F
y : (P F).W
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝)) = QPF.abs y.dest
⊢ Wequiv (WType.mk a✝ f✝) y

Proof state:
case mk
F : Type u → Type u
q : QPF F
y : (P F).W
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝)) = QPF.abs y.dest
⊢ Wequiv (WType.mk a✝ f✝) y

Tactic:
cases y

Result:
case mk.mk
F : Type u → Type u
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Wequiv (WType.mk a✝¹ f✝¹) (WType.mk a✝ f✝)

Proof state:
case mk.mk
F : Type u → Type u
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ Wequiv (WType.mk a✝¹ f✝¹) (WType.mk a✝ f✝)

Tactic:
apply Wequiv.abs

Result:
case mk.mk.a
F : Type u → Type u
q : QPF F
a✝¹ : (P F).A
f✝¹ : (P F).B a✝¹ → WType (P F).B
a✝ : (P F).A
f✝ : (P F).B a✝ → WType (P F).B
h : QPF.abs (PFunctor.W.dest (WType.mk a✝¹ f✝¹)) = QPF.abs (PFunctor.W.dest (WType.mk a✝ f✝))
⊢ QPF.abs ⟨a✝¹, f✝¹⟩ = QPF.abs ⟨a✝, f✝⟩
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem lift_comp_inl : (lift fn fg h).comp inl = fn

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
⊢ (lift fn fg h).comp inl = fn

Tactic:
ext

Result:
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : N
⊢ ((lift fn fg h).comp inl) x✝ = fn x✝

Proof state:
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
x✝ : N
⊢ ((lift fn fg h).comp inl) x✝ = fn x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma π_comp_leftHomologyIso_inv :
    h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ

Tactic:
simp only [← cancel_epi h.cyclesIso.hom, ← cancel_mono h.leftHomologyIso.hom, assoc,
  Iso.inv_hom_id, comp_id, Iso.hom_inv_id_assoc,
  LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem Monotone.le_map_sSup [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) :
    ⨆ a ∈ s, f a ≤ f (sSup s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (sSup s)

Tactic:
rw [sSup_eq_iSup]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (⨆ a ∈ s, a)

Tactic:
exact hf.le_map_iSup₂ _

Result:
no goals
-- Mathlib/SetTheory/Game/Domineering.lean
theorem moveLeft_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ left b) :
    Finset.card (moveLeft b m) / 2 < Finset.card b / 2

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ left b
⊢ Finset.card (moveLeft b m) / 2 < Finset.card b / 2

Tactic:
simp [← moveLeft_card h, lt_add_one]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma expCoeff_cast (n : ℕ) : (expCoeff n : ℚ) = if Even n then (n / 2 : ℚ) else n

Proof state:
n : ℕ
⊢ ↑(WeierstrassCurve.expCoeff n) = if Even n then ↑n / 2 else ↑n

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩ <;> simp [expCoeff, n.not_even_two_mul_add_one]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- The L-function of an odd function vanishes at negative odd integers. -/
@[simp] lemma LFunction_neg_two_mul_nat_sub_one (hΦ : Φ.Odd) (n : ℕ) :
    LFunction Φ (-(2 * n) - 1) = 0

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
n : ℕ
⊢ LFunction Φ (-(2 * ↑n) - 1) = 0

Tactic:
simp only [LFunction_def_odd hΦ, hurwitzZetaOdd_neg_two_mul_nat_sub_one, mul_zero, ← neg_mul,
  sum_const_zero]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_one_moveRight (x) : (nim 1).moveRight x = nim 0

Proof state:
x : (nim 1).RightMoves
⊢ (nim 1).moveRight x = nim 0

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_Ψ₂Sq : (W.map f).Ψ₂Sq = W.Ψ₂Sq.map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq

Tactic:
simp only [Ψ₂Sq, map_b₂, map_b₄, map_b₆]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ C 4 * X ^ 3 + C (f W.b₂) * X ^ 2 + C (2 * f W.b₄) * X + C (f W.b₆) =
    Polynomial.map f (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
⊢ C 4 * X ^ 3 + C (f W.b₂) * X ^ 2 + C (2 * f W.b₄) * X + C (f W.b₆) =
    Polynomial.map f (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆)

Tactic:
map_simp

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.of_finite [Finite M] : FG L M

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
inst✝ : Finite M
⊢ FG L M

Tactic:
simp only [fg_def, Substructure.FG.of_finite, topEquiv.toEquiv.finite_iff]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem expNear_succ (n x r) : expNear (n + 1) x r = expNear n x (1 + x / (n + 1) * r)

Proof state:
n : ℕ
x r : ℝ
⊢ expNear (n + 1) x r = expNear n x (1 + x / (↑n + 1) * r)

Tactic:
simp [expNear, range_succ, mul_add, add_left_comm, add_assoc, pow_succ, div_eq_mul_inv,
    mul_inv, Nat.factorial]

Result:
n : ℕ
x r : ℝ
⊢ x ^ n * x * ((↑n.factorial)⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑n.factorial)⁻¹ * (x * (↑n + 1)⁻¹ * r)

Proof state:
n : ℕ
x r : ℝ
⊢ x ^ n * x * ((↑n.factorial)⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑n.factorial)⁻¹ * (x * (↑n + 1)⁻¹ * r)

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem isSuccPrelimit_aleph0 : IsSuccPrelimit ℵ₀ :=
  isSuccPrelimit_of_succ_lt fun a ha => by
    rcases lt_aleph0.1 ha with ⟨n, rfl⟩
    rw [← nat_succ]
    apply nat_lt_aleph0

Proof state:
case intro
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑n.succ < ℵ₀

Tactic:
apply nat_lt_aleph0

Result:
no goals

Proof state:
case intro
n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀

Tactic:
rw [← nat_succ]

Result:
case intro
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑n.succ < ℵ₀

Proof state:
a : Cardinal.{u_1}
ha : a < ℵ₀
⊢ succ a < ℵ₀

Tactic:
rcases lt_aleph0.1 ha with ⟨n, rfl⟩

Result:
case intro
n : ℕ
ha : ↑n < ℵ₀
⊢ succ ↑n < ℵ₀
-- Mathlib/LinearAlgebra/BilinearForm/Basic.lean
lemma smul_left_of_tower (r : S) (x y : M) : B (r • x) y = r • B x y

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
⊢ (B (r • x)) y = r • (B x) y

Tactic:
rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Erase.lean
theorem eraseIdx_set_eq {l : List α} {i : Nat} {a : α} :
    (l.set i a).eraseIdx i = l.eraseIdx i

Proof state:
case h.isFalse
α : Type u_1
l : List α
i : Nat
a : α
n : Nat
h₁ : n < ((l.set i a).eraseIdx i).length
h₂ : n < (l.eraseIdx i).length
h✝ : ¬n < i
⊢ (l.set i a)[n + 1] = l[n + 1]

Tactic:
rw [getElem_set_ne]

Result:
case h.isFalse.h
α : Type u_1
l : List α
i : Nat
a : α
n : Nat
h₁ : n < ((l.set i a).eraseIdx i).length
h₂ : n < (l.eraseIdx i).length
h✝ : ¬n < i
⊢ i ≠ n + 1

Proof state:
case hl
α : Type u_1
l : List α
i : Nat
a : α
⊢ ((l.set i a).eraseIdx i).length = (l.eraseIdx i).length

Tactic:
simp [length_eraseIdx]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.set i a).eraseIdx i = l.eraseIdx i

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
l : List α
i : Nat
a : α
⊢ ((l.set i a).eraseIdx i).length = (l.eraseIdx i).length

case h
α : Type u_1
l : List α
i : Nat
a : α
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < ((l.set i a).eraseIdx i).length) (h₂ : i_1 < (l.eraseIdx i).length),
    ((l.set i a).eraseIdx i)[i_1] = (l.eraseIdx i)[i_1]

Proof state:
case h.isFalse.h
α : Type u_1
l : List α
i : Nat
a : α
n : Nat
h₁ : n < ((l.set i a).eraseIdx i).length
h₂ : n < (l.eraseIdx i).length
h✝ : ¬n < i
⊢ i ≠ n + 1

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
i : Nat
a : α
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < ((l.set i a).eraseIdx i).length) (h₂ : i_1 < (l.eraseIdx i).length),
    ((l.set i a).eraseIdx i)[i_1] = (l.eraseIdx i)[i_1]

Tactic:
intro n h₁ h₂

Result:
case h
α : Type u_1
l : List α
i : Nat
a : α
n : Nat
h₁ : n < ((l.set i a).eraseIdx i).length
h₂ : n < (l.eraseIdx i).length
⊢ ((l.set i a).eraseIdx i)[n] = (l.eraseIdx i)[n]

Proof state:
case h
α : Type u_1
l : List α
i : Nat
a : α
n : Nat
h₁ : n < ((l.set i a).eraseIdx i).length
h₂ : n < (l.eraseIdx i).length
⊢ ((l.set i a).eraseIdx i)[n] = (l.eraseIdx i)[n]

Tactic:
rw [getElem_eraseIdx, getElem_eraseIdx]

Result:
case h
α : Type u_1
l : List α
i : Nat
a : α
n : Nat
h₁ : n < ((l.set i a).eraseIdx i).length
h₂ : n < (l.eraseIdx i).length
⊢ (if h' : n < i then (l.set i a)[n] else (l.set i a)[n + 1]) = if h' : n < i then l[n] else l[n + 1]