harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Equiv.lean
theorem comp_symm (e : A₁ ≃ₐ[R] A₂) : AlgHom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = AlgHom.id R A₂

Proof state:
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x✝ : A₂
⊢ ((↑e).comp ↑e.symm) x✝ = (AlgHom.id R A₂) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (↑e).comp ↑e.symm = AlgHom.id R A₂

Tactic:
ext

Result:
case H
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x✝ : A₂
⊢ ((↑e).comp ↑e.symm) x✝ = (AlgHom.id R A₂) x✝
-- Mathlib/Data/Set/Insert.lean
theorem pair_subset_iff : {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

Proof state:
α : Type u
s : Set α
a b : α
⊢ {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

Tactic:
rw [insert_subset_iff, singleton_subset_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem getElem?_mapIdx (f : Nat → α → β) (as : Array α) (i : Nat) :
    (as.mapIdx f)[i]? =
      as[i]?.map (f i)

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
as : Array α
i : Nat
⊢ (mapIdx f as)[i]? = Option.map (f i) as[i]?

Tactic:
simp [getElem?_def, size_mapIdx, getElem_mapIdx]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_hnot_self : a ∆ (￢a) = ⊤

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ (￢a) = ⊤

Tactic:
rw [symmDiff_comm, hnot_symmDiff_self]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem frontier_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) :
    frontier (closedBall x r) = sphere x r

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (closedBall x r) = sphere x r

Tactic:
rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).isEmpty = false

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insertIfNew k v).isEmpty = false

Tactic:
simp_to_raw using Raw₀.isEmpty_insertIfNew

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
lemma even_iff : Even n ↔ n % 2 = 0 where
  mp := fun ⟨m, hm⟩ ↦ by simp [← Nat.two_mul, hm]
  mpr h := ⟨n / 2, (mod_add_div n 2).symm.trans (by simp [← Nat.two_mul, h])⟩

Proof state:
n : ℕ
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2

Tactic:
simp [← Nat.two_mul, h]

Result:
no goals

Proof state:
n : ℕ
x✝ : Even n
m : ℕ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
simp [← Nat.two_mul, hm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_le_iff_le_sin {x y : ℝ} (hx : x ∈ Icc (-1 : ℝ) 1) (hy : y ∈ Icc (-(π / 2)) (π / 2)) :
    arcsin x ≤ y ↔ x ≤ sin y

Proof state:
x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y

Tactic:
rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- If `a ≠ 0` and `a ≠ ∞`, then division by `a` maps infimum to infimum.

See `ENNReal.iInf_div'` for the general case, and `ENNReal.iInf_div` for another special case that
assumes `Nonempty ι` but does not require `a ≠ ∞`. -/
lemma iInf_div_of_ne (ha₀ : a ≠ 0) (ha : a ≠ ∞) : (⨅ i, f i) / a = ⨅ i, f i / a :=
  iInf_div' (by simp [ha₀]) (by simp [ha])

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
simp [ha₀]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → Nonempty ι

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean
@[reassoc]
lemma cone_π_app_comp_Pi_π_neg (m n : ℕ) (h : ¬(n < m)) : (cone f).π.app ⟨m⟩ ≫ Pi.π _ n =
    Pi.π _ n ≫ f n ≫ eqToHom (functorObj_eq_neg h).symm

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
m n : ℕ
h : ¬n < m
⊢ (cone f).π.app (Opposite.op m) ≫
      Pi.π (fun m_1 => if x : m_1 < Opposite.unop (Opposite.op m) then M m_1 else N m_1) n =
    Pi.π M n ≫ f n ≫ eqToHom ⋯

Tactic:
simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
  Discrete.functor_obj_eq_as, Discrete.natTrans_app]

Result:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
m n : ℕ
h : ¬n < m
⊢ (limit.π (Discrete.functor fun m => M m) { as := n } ≫ if h : n < m then eqToHom ⋯ else f n ≫ eqToHom ⋯) =
    Pi.π M n ≫ f n ≫ eqToHom ⋯

Proof state:
C : Type u_1
M N : ℕ → C
inst✝¹ : Category.{u_2, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst✝ : HasProductsOfShape ℕ C
m n : ℕ
h : ¬n < m
⊢ (limit.π (Discrete.functor fun m => M m) { as := n } ≫ if h : n < m then eqToHom ⋯ else f n ≫ eqToHom ⋯) =
    Pi.π M n ≫ f n ≫ eqToHom ⋯

Tactic:
rw [dif_neg h]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive (attr := simp)]
lemma inv_smul_smul (g : G) (a : α) : g⁻¹ • g • a = a

Proof state:
G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g⁻¹ • g • a = a

Tactic:
rw [smul_smul, inv_mul_cancel, one_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Adjunction.lean
lemma ε_app (X₁ : C₁) :
    (ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
      L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫
        F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{u_6, u_1} C₁
inst✝⁵ : Category.{u_8, u_2} C₂
inst✝⁴ : Category.{u_5, u_3} D₁
inst✝³ : Category.{u_7, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }
⊢ (ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫
      (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Tactic:
simp only [ε, liftNatTrans_app, Lifting.iso, Iso.symm,
  Functor.id_obj, Functor.comp_obj, Lifting.id_iso', Functor.rightUnitor_hom_app,
    whiskerRight_app, CatCommSq.hComp_iso'_hom_app, id_comp]

Result:
no goals

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{u_6, u_1} C₁
inst✝⁵ : Category.{u_8, u_2} C₂
inst✝⁴ : Category.{u_5, u_3} D₁
inst✝³ : Category.{u_7, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ (ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫
      (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Tactic:
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') :=
  Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{u_6, u_1} C₁
inst✝⁵ : Category.{u_8, u_2} C₂
inst✝⁴ : Category.{u_5, u_3} D₁
inst✝³ : Category.{u_7, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }
⊢ (ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫
      (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
@[simp]
protected lemma continuousAt_inv : ContinuousAt Inv.inv x ↔ x ≠ 0

Proof state:
𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
⊢ ContinuousAt Inv.inv x ↔ x ≠ 0

Tactic:
simpa using NormedField.continuousAt_zpow (n := -1) (x := x)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma lintegral_le_const [IsProbabilityMeasure μ] {f : α → ℝ≥0∞} {c : ℝ≥0∞}
    (hf : ∀ᵐ x ∂μ, f x ≤ c) : ∫⁻ x, f x ∂μ ≤ c :=
  (lintegral_mono_ae hf).trans_eq (by simp)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
f : α → ℝ≥0∞
c : ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≤ c
⊢ ∫⁻ (a : α), c ∂μ = c

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Iio : (fun x => a - x) '' Iio b = Ioi (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Iio b = Ioi (a - b)
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_coord_zero {m : ∀ i, M₁ i} (i : ι) (h : m i = 0) : f m = 0

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : 0 • 0 = 0
⊢ f m = 0

Tactic:
rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul R (M := M₂)]

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ f m = 0

Tactic:
classical
  have : (0 : R) • (0 : M₁ i) = 0 := by simp
  rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul R (M := M₂)]

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ 0 • 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ f m = 0

Tactic:
have : (0 : R) • (0 : M₁ i) = 0 := by simp

Result:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : 0 • 0 = 0
⊢ f m = 0
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.div {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ : f₁ =Θ[l] g₁) (h₂ : f₂ =Θ[l] g₂) :
    (fun x ↦ f₁ x / f₂ x) =Θ[l] fun x ↦ g₁ x / g₂ x

Proof state:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f₁ f₂ : α → 𝕜
g₁ g₂ : α → 𝕜'
h₁ : f₁ =Θ[l] g₁
h₂ : f₂ =Θ[l] g₂
⊢ (fun x => f₁ x / f₂ x) =Θ[l] fun x => g₁ x / g₂ x

Tactic:
simpa only [div_eq_mul_inv] using h₁.mul h₂.inv

Result:
no goals
-- Mathlib/CategoryTheory/GlueData.lean
theorem t'_iji (i j : D.J) : D.t' i j i = pullback.fst _ _ ≫ D.t i j ≫ inv (pullback.snd _ _)

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
rw [← Category.assoc, ← D.t_fac]

Result:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (pullback.snd (D.f j i) (D.f j i))

Proof state:
C : Type u₁
inst✝ : Category.{v, u₁} C
D : GlueData C
i j : D.J
⊢ D.t' i j i = (D.t' i j i ≫ pullback.snd (D.f j i) (D.f j i)) ≫ inv (pullback.snd (D.f j i) (D.f j i))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem bind₂_C_left : bind₂ (C : R →+* MvPolynomial σ R) = RingHom.id _

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
⊢ bind₂ C = RingHom.id (MvPolynomial σ R)

Tactic:
ext : 2 <;> simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySum_isBounded : Bornology.IsBounded (convexBodySum K B)

Proof state:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ ‖y‖ ≤ B

Tactic:
exact le_trans (norm_le_convexBodySumFun y) hy

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ Bornology.IsBounded (convexBodySum K B)

Tactic:
refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ dist x y ≤ B + B

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ dist x y ≤ B + B

Tactic:
refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)

Result:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ ‖x‖ ≤ B

case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ ‖y‖ ≤ B

Proof state:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
y : mixedSpace K
hy : y ∈ convexBodySum K B
⊢ ‖x‖ ≤ B

Tactic:
exact le_trans (norm_le_convexBodySumFun x) hx

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
theorem flatten_drop_length_sub_one {L : List (List α)} (h : L ≠ []) :
    (L.drop (L.length - 1)).flatten = L.getLast h

Proof state:
α : Type u_1
L : List (List α)
h : L ≠ []
⊢ (drop (L.length - 1) L).flatten = L.getLast h

Tactic:
induction L using List.reverseRecOn

Result:
case nil
α : Type u_1
h : [] ≠ []
⊢ (drop ([].length - 1) []).flatten = [].getLast h

case append_singleton
α : Type u_1
l✝ : List (List α)
a✝¹ : List α
a✝ : ∀ (h : l✝ ≠ []), (drop (l✝.length - 1) l✝).flatten = l✝.getLast h
h : l✝ ++ [a✝¹] ≠ []
⊢ (drop ((l✝ ++ [a✝¹]).length - 1) (l✝ ++ [a✝¹])).flatten = (l✝ ++ [a✝¹]).getLast h

Proof state:
case nil
α : Type u_1
h : [] ≠ []
⊢ (drop ([].length - 1) []).flatten = [].getLast h

Tactic:
cases h rfl

Result:
no goals

Proof state:
case append_singleton
α : Type u_1
l✝ : List (List α)
a✝¹ : List α
a✝ : ∀ (h : l✝ ≠ []), (drop (l✝.length - 1) l✝).flatten = l✝.getLast h
h : l✝ ++ [a✝¹] ≠ []
⊢ (drop ((l✝ ++ [a✝¹]).length - 1) (l✝ ++ [a✝¹])).flatten = (l✝ ++ [a✝¹]).getLast h

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem algEquivAevalXAddC_symm {R : Type*} [CommRing R] (t : R) :
    (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

Proof state:
R : Type u_3
inst✝ : CommRing R
t : R
⊢ (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

Tactic:
simp [algEquivAevalXAddC, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem restrict_preimage {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β}
    (hs : MeasurableSet s) : MeasurePreserving f (μa.restrict (f ⁻¹' s)) (μb.restrict s) :=
  ⟨hf.measurable, by rw [← hf.map_eq, restrict_map hf.measurable hs]⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : MeasurableSet s
⊢ map f (μa.restrict (f ⁻¹' s)) = μb.restrict s

Tactic:
rw [← hf.map_eq, restrict_map hf.measurable hs]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem sSup_apply {Ss : Set (Sieve X)} {Y} (f : Y ⟶ X) :
    sSup Ss f ↔ ∃ (S : Sieve X) (_ : S ∈ Ss), S f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Ss : Set (Sieve X)
Y : C
f : Y ⟶ X
⊢ (sSup Ss).arrows f ↔ ∃ S, ∃ (_ : S ∈ Ss), S.arrows f

Tactic:
simp [sSup, Sieve.sup, setOf]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Tower.lean
theorem adjoin_range_toAlgHom (t : Set A) :
    (Algebra.adjoin (toAlgHom R S A).range t).restrictScalars R =
      (Algebra.adjoin S t).restrictScalars R :=
  Subalgebra.ext fun z ↦
    show z ∈ Subsemiring.closure (Set.range (algebraMap (toAlgHom R S A).range A) ∪ t : Set A) ↔
         z ∈ Subsemiring.closure (Set.range (algebraMap S A) ∪ t : Set A) by
      suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by
        rw [this]
      ext z
      exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩

Proof state:
case h
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z✝ z : A
⊢ z ∈ Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) ↔ z ∈ Set.range ⇑(algebraMap S A)

Tactic:
exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
this : Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) = Set.range ⇑(algebraMap S A)
⊢ z ∈ Subsemiring.closure (Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ⇑(algebraMap S A) ∪ t)

Tactic:
rw [this]

Result:
no goals

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
⊢ z ∈ Subsemiring.closure (Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ⇑(algebraMap S A) ∪ t)

Tactic:
suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by
  rw [this]

Result:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
⊢ Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) = Set.range ⇑(algebraMap S A)

Proof state:
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
⊢ Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) = Set.range ⇑(algebraMap S A)

Tactic:
ext z

Result:
case h
R : Type u
S : Type v
A : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z✝ z : A
⊢ z ∈ Set.range ⇑(algebraMap (↥(toAlgHom R S A).range) A) ↔ z ∈ Set.range ⇑(algebraMap S A)
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph1_eq_lift {c : Cardinal.{u}} : ℵ₁ = lift.{v} c ↔ ℵ₁ = c

Proof state:
c : Cardinal.{u}
⊢ ℵ_ 1 = lift.{v, u} c ↔ ℵ_ 1 = c

Tactic:
simpa using lift_inj (a := ℵ₁)

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The cardinality of the set of `k`-rough numbers `≤ N` is bounded by the sum of `⌊N/p⌋`
over the primes `k ≤ p ≤ N`. -/
lemma roughNumbersUpTo_card_le (N k : ℕ) :
    (roughNumbersUpTo N k).card ≤ (N.succ.primesBelow \ k.primesBelow).sum (fun p ↦ N / p)

Proof state:
N k : ℕ
⊢ (N.roughNumbersUpTo k).card ≤ ∑ p ∈ N.succ.primesBelow \ k.primesBelow, N / p

Tactic:
rw [roughNumbersUpTo_eq_biUnion]

Result:
N k : ℕ
⊢ ((N.succ.primesBelow \ k.primesBelow).biUnion fun p =>
        Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)).card ≤
    ∑ p ∈ N.succ.primesBelow \ k.primesBelow, N / p

Proof state:
N k : ℕ
⊢ ((N.succ.primesBelow \ k.primesBelow).biUnion fun p =>
        Finset.filter (fun m => m ≠ 0 ∧ p ∣ m) (Finset.range N.succ)).card ≤
    ∑ p ∈ N.succ.primesBelow \ k.primesBelow, N / p

Tactic:
exact Finset.card_biUnion_le.trans <| Finset.sum_le_sum fun p _ ↦ (card_multiples' N p).le

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/IsOpenComapC.lean
theorem isOpen_imageOfDf : IsOpen (imageOfDf f)

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})

Tactic:
exact isOpen_iUnion fun i => isOpen_basicOpen

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)

Tactic:
rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]

Result:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (⋃ i, {x | f.coeff i ∉ x.asIdeal})
-- Mathlib/Logic/Function/Defs.lean
theorem Injective.beq_eq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {f : α → β}
    (I : Injective f) {a b : α} : (f a == f b) = (a == b)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)

Tactic:
by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem back?_filterMap (f : α → Option β) (l : Array α) : (l.filterMap f).back? = l.findSomeRev? f

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).back? = findSomeRev? f { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ (filterMap f l).back? = findSomeRev? f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).back? = findSomeRev? f { toList := toList✝ }