harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomial (P : Fin 3 → R) : eval P W'.polynomial =
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2
      - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomial =
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)

Tactic:
rw [polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
      (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)
-- Mathlib/RingTheory/Valuation/Integers.lean
theorem isUnit_of_one (hv : Integers v O) {x : O} (hx : IsUnit (algebraMap O R x))
    (hvx : v (algebraMap O R x) = 1) : IsUnit x :=
  let ⟨u, hu⟩ := hx
  have h1 : v u ≤ 1 := hu.symm ▸ hv.2 x
  have h2 : v (u⁻¹ : Rˣ) ≤ 1

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) (r2 * r1) = (algebraMap O R) 1

Tactic:
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.inv_mul]

Result:
no goals

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
⊢ v ↑u⁻¹ ≤ 1

Tactic:
rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]

Result:
no goals

Proof state:
R : Type u
Γ₀ : Type v
inst✝³ : CommRing R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : v.Integers O
x : O
hx : IsUnit ((algebraMap O R) x)
hvx : v ((algebraMap O R) x) = 1
u : Rˣ
hu : ↑u = (algebraMap O R) x
h1 : v ↑u ≤ 1
h2 : v ↑u⁻¹ ≤ 1
r1 : O
hr1 : (algebraMap O R) r1 = ↑u
r2 : O
hr2 : (algebraMap O R) r2 = ↑u⁻¹
⊢ (algebraMap O R) (r1 * r2) = (algebraMap O R) 1

Tactic:
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.mul_inv]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem splitMin_eq :
    ∀ (s l) (x : α) (r), splitMin' l x r = (findMin' l x, eraseMin (node s l x r))
  | _, nil, _, _ => rfl
  | _, node ls ll lx lr, x, r => by rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]

Proof state:
α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x✝ (node ls ll lx lr) x r).eraseMin)

Tactic:
rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_add [AddMonoidWithOne α] (m n) : ((m + n : PosNum) : α) = m + n

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
m n : PosNum
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem lt_of_le_of_finrank_lt_finrank {s t : Submodule R M} (le : s ≤ t)
    (lt : finrank R s < finrank R t) : s < t :=
  lt_of_le_of_ne le fun h => ne_of_lt lt (by rw [h])

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Submodule R M
le : s ≤ t
lt : finrank R ↥s < finrank R ↥t
h : s = t
⊢ finrank R ↥s = finrank R ↥t

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem strongDownwardInductionOn_eq {p : Finset α → Sort*} (s : Finset α)
    (H : ∀ t₁, (∀ {t₂ : Finset α}, #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁) :
    s.strongDownwardInductionOn H = H s fun {t} ht _ => t.strongDownwardInductionOn H ht

Proof state:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht x => strongDownwardInduction H t ht

Tactic:
rw [strongDownwardInduction]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht x => t.strongDownwardInductionOn H ht

Tactic:
dsimp only [strongDownwardInductionOn]

Result:
α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht x => strongDownwardInduction H t ht
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_eq_fallback_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {a fallback : α} :
    m.contains a = false → m.getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
⊢ m.contains a = false → m.getKeyD a fallback = fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_eq_fallback

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
/-- Formula for `ζ 1`. Note that mathematically `ζ 1` is undefined, but our construction ascribes
this particular value to it. -/
lemma _root_.riemannZeta_one : riemannZeta 1 = (γ - Complex.log (4 * ↑π)) / 2

Proof state:
this : Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))
⊢ riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2

Tactic:
exact tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_Gammaℝ

Result:
no goals

Proof state:
⊢ riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2

Tactic:
have := (HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one 0).mono_left
  <| nhdsWithin_le_nhds (s := {1}ᶜ)

Result:
this :
  Tendsto (fun s => HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
    (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))
⊢ riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2

Proof state:
this :
  Tendsto (fun s => HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
    (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))
⊢ riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2

Tactic:
simp only [HurwitzZeta.hurwitzZetaEven_zero, div_right_comm _ _ (Gammaℝ _)] at this

Result:
this : Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))
⊢ riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem mateEquiv_counit (α : TwoSquare G L₁ L₂ H) (d : D) :
    L₂.map ((mateEquiv adj₁ adj₂ α).app _) ≫ adj₂.counit.app _ =
      α.app _ ≫ H.map (adj₁.counit.app d)

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
d : D
⊢ L₂.map (((mateEquiv adj₁ adj₂) α).app d) ≫ adj₂.counit.app (H.obj d) = α.app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
lemma ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq
    {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : ProjectiveResolution X) :
    (NatTrans.leftDerivedToHomotopyCategory α).app X =
      (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.quotient _ _).map
          ((NatTrans.mapHomologicalComplex α _).app P.complex) ≫
          (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (NatTrans.leftDerivedToHomotopyCategory α).app X ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)

Tactic:
dsimp [isoLeftDerivedToHomotopyCategoryObj, Functor.mapHomotopyCategoryFactors,
  NatTrans.leftDerivedToHomotopyCategory]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) =
    ((F.mapHomotopyCategory (ComplexShape.down ℕ)).map P.iso.hom ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex))) ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
-- Mathlib/Data/ENat/Basic.lean
lemma coe_lt_coe {n m : ℕ} : (n : ℕ∞) < (m : ℕ∞) ↔ n < m

Proof state:
n m : ℕ
⊢ ↑n < ↑m ↔ n < m

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
theorem not_dvd_of_between_consec_multiples (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m

Proof state:
m n k : ℕ
h1 : n * k < m
h2 : m < n * (k + 1)
⊢ ¬n ∣ m

Tactic:
rintro ⟨d, rfl⟩

Result:
case intro
n k d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
⊢ False

Proof state:
case intro
n k d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
this : k < d
⊢ False

Tactic:
have := Nat.lt_of_mul_lt_mul_left h2

Result:
case intro
n k d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
this✝ : k < d
this : d < k + 1
⊢ False

Proof state:
case intro
n k d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
this✝ : k < d
this : d < k + 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case intro
n k d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
⊢ False

Tactic:
have := Nat.lt_of_mul_lt_mul_left h1

Result:
case intro
n k d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
this : k < d
⊢ False
-- Mathlib/CategoryTheory/Linear/Basic.lean
@[simp]
lemma comp_units_smul {X Y Z : C} (f : X ⟶ Y) (r : Rˣ) (g : Y ⟶ Z) :
    f ≫ (r • g) = r • f ≫ g

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
X Y Z : C
f : X ⟶ Y
r : Rˣ
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
apply Linear.comp_smul

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem ofNat'_eq : ∀ n, Num.ofNat' n = n :=
  Nat.binaryRec (by simp) fun b n IH => by tauto

Proof state:
⊢ ofNat' 0 = ↑0

Tactic:
simp

Result:
no goals

Proof state:
b : Bool
n : ℕ
IH : ofNat' n = ↑n
⊢ ofNat' (Nat.bit b n) = ↑(Nat.bit b n)

Tactic:
tauto

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_id (l : List α) : map (id : α → α) l = l

Proof state:
α : Type u_1
l : List α
⊢ map id l = l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem maxPowDiv_eq_emultiplicity {p n : ℕ} (hp : 1 < p) (hn : 0 < n) :
    p.maxPowDiv n = emultiplicity p n

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ ↑(p.maxPowDiv n) = emultiplicity p n

Tactic:
apply (emultiplicity_eq_of_dvd_of_not_dvd (pow_dvd p n) _).symm

Result:
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ ¬p ^ (p.maxPowDiv n + 1) ∣ n

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ (p.maxPowDiv n + 1) ∣ n
⊢ False

Tactic:
apply Nat.not_lt.mpr <| le_of_dvd hp hn h

Result:
p n : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ (p.maxPowDiv n + 1) ∣ n
⊢ p.maxPowDiv n < p.maxPowDiv n + 1

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ (p.maxPowDiv n + 1) ∣ n
⊢ p.maxPowDiv n < p.maxPowDiv n + 1

Tactic:
simp

Result:
no goals

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ ¬p ^ (p.maxPowDiv n + 1) ∣ n

Tactic:
intro h

Result:
p n : ℕ
hp : 1 < p
hn : 0 < n
h : p ^ (p.maxPowDiv n + 1) ∣ n
⊢ False
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isClosed_infty : IsClosed ({∞} : Set (OnePoint X))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed {∞}

Tactic:
rw [← compl_range_coe, isClosed_compl_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsOpen (range some)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsOpen (range some)

Tactic:
exact isOpen_range_coe

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem Irreducible.coprime_iff_not_dvd {p n : R} (hp : Irreducible p) :
    IsCoprime p n ↔ ¬p ∣ n

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n

Tactic:
rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_le_of_ball {f : E →SL[σ₁₂] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
    (hf : ∀ x ∈ ball (0 : E) ε, ‖f x‖ ≤ C * ‖x‖) : ‖f‖ ≤ C

Proof state:
case intro
𝕜 : 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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
x : E
x✝ : ε / ‖c‖ ≤ ‖x‖
hx : ‖x‖ < ε
⊢ x ∈ ball 0 ε

Tactic:
rwa [ball_zero_eq]

Result:
no goals

Proof state:
case intro
𝕜 : 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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖f‖ ≤ C

Tactic:
refine opNorm_le_of_shell ε_pos hC hc fun x _ hx => hf x ?_

Result:
case intro
𝕜 : 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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
x : E
x✝ : ε / ‖c‖ ≤ ‖x‖
hx : ‖x‖ < ε
⊢ x ∈ ball 0 ε

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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖
⊢ ‖f‖ ≤ C

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Result:
case intro
𝕜 : 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
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
ε C : ℝ
ε_pos : 0 < ε
hC : 0 ≤ C
hf : ∀ x ∈ ball 0 ε, ‖f x‖ ≤ C * ‖x‖
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖f‖ ≤ C
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma comp_apply {X Y T : Grp} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y T : Grp
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem HasSum.const_div (h :  HasSum (fun x ↦ 1 / f x) a) (b : α) :
    HasSum (fun i ↦ b / f i) (b * a)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum (fun x => 1 / f x) a
b : α
⊢ HasSum (fun i => b / f i) (b * a)

Tactic:
have := h.mul_left b

Result:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum (fun x => 1 / f x) a
b : α
this : HasSum (fun i => b * (1 / f i)) (b * a)
⊢ HasSum (fun i => b / f i) (b * a)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum (fun x => 1 / f x) a
b : α
this : HasSum (fun i => b * (1 / f i)) (b * a)
⊢ HasSum (fun i => b / f i) (b * a)

Tactic:
simpa only [div_eq_mul_inv, one_mul] using this

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_eq_zero_iff {x : ℝ} : sin x = 0 ↔ ∃ n : ℤ, (n : ℝ) * π = x :=
  ⟨fun h =>
    ⟨⌊x / π⌋,
      le_antisymm (sub_nonneg.1 (Int.sub_floor_div_mul_nonneg _ pi_pos))
        (sub_nonpos.1 <|
          le_of_not_gt fun h₃ =>
            (sin_pos_of_pos_of_lt_pi h₃ (Int.sub_floor_div_mul_lt _ pi_pos)).ne
              (by simp [sub_eq_add_neg, sin_add, h, sin_int_mul_pi]))⟩,
    fun ⟨_, hn⟩ => hn ▸ sin_int_mul_pi _⟩

Proof state:
x : ℝ
h : sin x = 0
h₃ : x - ↑⌊x / π⌋ * π > 0
⊢ 0 = sin (x - ↑⌊x / π⌋ * π)

Tactic:
simp [sub_eq_add_neg, sin_add, h, sin_int_mul_pi]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_eval [Inhabited Γ] (l : List Γ) : TM0.eval (tr M) l = TM1.eval M l :=
  (congr_arg _ (tr_eval' _ _ _ (tr_respects M) ⟨some _, _, _⟩)).trans
    (by
      rw [Part.map_eq_map, Part.map_map, TM1.eval]
      congr with ⟨⟩)

Proof state:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
l : List Γ
⊢ Part.map ((fun c => c.Tape.right₀) ∘ trCfg M)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    Part.map (fun c => c.Tape.right₀) (eval (TM1.step M) (TM1.init l))

Tactic:
congr with ⟨⟩

Result:
no goals

Proof state:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
l : List Γ
⊢ Part.map (fun c => c.Tape.right₀)
      (trCfg M <$> eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    TM1.eval M l

Tactic:
rw [Part.map_eq_map, Part.map_map, TM1.eval]

Result:
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Inhabited Γ
l : List Γ
⊢ Part.map ((fun c => c.Tape.right₀) ∘ trCfg M)
      (eval (TM1.step M) { l := some default, var := default, Tape := Tape.mk₁ l }) =
    Part.map (fun c => c.Tape.right₀) (eval (TM1.step M) (TM1.init l))
-- Mathlib/Algebra/CharP/Basic.lean
/-- We have `2 ≠ 0` in a nontrivial ring whose characteristic is not `2`. -/
protected lemma Ring.two_ne_zero {R : Type*} [NonAssocSemiring R] [Nontrivial R]
    (hR : ringChar R ≠ 2) : (2 : R) ≠ 0

Proof state:
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 = ↑2

Tactic:
norm_cast

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)

Tactic:
exact mt (or_iff_left hR).mp CharP.ringChar_ne_one

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ 2 ≠ 0

Tactic:
rw [Ne, (by norm_cast : (2 : R) = (2 : ℕ)), ringChar.spec, Nat.dvd_prime Nat.prime_two]

Result:
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬(ringChar R = 1 ∨ ringChar R = 2)
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_inter_Ico : Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ici_inter_Iio.symm, Ici_inter_Ici.symm, Iio_inter_Iio.symm]

Result:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iio b₁ ∩ (Ici a₂ ∩ Iio b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iio b₁ ∩ Iio b₂)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iio b₁ ∩ (Ici a₂ ∩ Iio b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iio b₁ ∩ Iio b₂)

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem filterMap_attachWith {q : α → Prop} {l : Array α} {f : {x // q x} → Option β} (H)
    (w : stop = (l.attachWith q H).size) :
    (l.attachWith q H).filterMap f 0 stop = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩)

Proof state:
case mk
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → Option β
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → q x
⊢ filterMap f ({ toList := toList✝ }.attachWith q H) =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      { toList := toList✝ }.attach

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
q : α → Prop
l : Array α
f : { x // q x } → Option β
H : ∀ (x : α), x ∈ l → q x
⊢ filterMap f (l.attachWith q H) =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → Option β
toList✝ : List α
H : ∀ (x : α), x ∈ { toList := toList✝ } → q x
⊢ filterMap f ({ toList := toList✝ }.attachWith q H) =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      { toList := toList✝ }.attach

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
q : α → Prop
l : Array α
f : { x // q x } → Option β
H : ∀ (x : α), x ∈ l → q x
w : stop = (l.attachWith q H).size
⊢ filterMap f (l.attachWith q H) 0 stop =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
q : α → Prop
l : Array α
f : { x // q x } → Option β
H : ∀ (x : α), x ∈ l → q x
⊢ filterMap f (l.attachWith q H) =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_target_subset_range : (f.extend I).target ⊆ range I

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).target ⊆ range ↑I

Tactic:
simp only [mfld_simps]

Result:
no goals