harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/EqToHom.lean
theorem ext {F G : C ⥤ D} (h_obj : ∀ X, F.obj X = G.obj X)
    (h_map : ∀ X Y f,
      F.map f = eqToHom (h_obj X) ≫ G.map f ≫ eqToHom (h_obj Y).symm

Proof state:
case e_toPrefunctor.e_map
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
        eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯)
    _auto✝
⊢ map✝¹ = map✝

Tactic:
funext X Y f

Result:
case e_toPrefunctor.e_map.h.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
        eqToHom ⋯ ≫ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯)
    _auto✝
X Y : C
f : X ⟶ Y
⊢ map✝¹ f = map✝ f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
    x.abs.toInt = x.toInt.natAbs

Proof state:
w : Nat
x : BitVec w
hx : x ≠ intMin w
⊢ x.abs.toInt = ↑x.toInt.natAbs

Tactic:
simp [toInt_abs_eq_natAbs, hx]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem oreDiv_smul_oreDiv {r₁ : R} {r₂ : X} {s₁ s₂ : S} :
    (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
with_unfolding_all rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem neg_concaveOn_iff : ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f

Tactic:
rw [← neg_convexOn_iff, neg_neg f]

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
lemma add_rpow_le_rpow_add {p : ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hp1 : 1 ≤ p) :
     a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
lift a to NNReal using ha

Result:
case intro
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p

Proof state:
case intro
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ ↑a ^ p + b ^ p ≤ (↑a + b) ^ p

Tactic:
lift b to NNReal using hb

Result:
case intro.intro
p : ℝ
hp1 : 1 ≤ p
a b : ℝ≥0
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p

Proof state:
case intro.intro
p : ℝ
hp1 : 1 ≤ p
a b : ℝ≥0
⊢ ↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p

Tactic:
exact_mod_cast NNReal.add_rpow_le_rpow_add a b hp1

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem Tape.mk'_left_right₀ {Γ} [Inhabited Γ] (T : Tape Γ) : Tape.mk' T.left T.right₀ = T

Proof state:
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ mk' { head := head✝, left := left✝, right := right✝ }.left { head := head✝, left := left✝, right := right✝ }.right₀ =
    { head := head✝, left := left✝, right := right✝ }

Tactic:
simp only [Tape.right₀, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons, eq_self_iff_true,
  and_self_iff]

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
T : Tape Γ
⊢ mk' T.left T.right₀ = T

Tactic:
cases T

Result:
case mk
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
left✝ right✝ : ListBlank Γ
⊢ mk' { head := head✝, left := left✝, right := right✝ }.left { head := head✝, left := left✝, right := right✝ }.right₀ =
    { head := head✝, left := left✝, right := right✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_flatten (L : List (List α)) :
    L.flatten.reverse = (L.map reverse).reverse.flatten

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten.reverse = (map reverse L).reverse.flatten

Tactic:
induction L <;> simp_all

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem merge' {f g} (hf : Nat.Partrec f) (hg : Nat.Partrec g) :
    ∃ h, Nat.Partrec h ∧
      ∀ a, (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Proof state:
case intro.intro.inl.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
refine ⟨k, x, ?_⟩

Result:
case intro.intro.inl.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)

Proof state:
case intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (cf.eval n).Dom ∨ (cg.eval n).Dom
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
simp only [dom_iff_mem, Code.evaln_complete, Option.mem_def] at h

Result:
case intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (∃ y k, Code.evaln k cf n = Option.some y) ∨ ∃ y k, Code.evaln k cg n = Option.some y
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Proof state:
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
obtain ⟨k, e⟩ := Nat.rfindOpt_spec h

Result:
case intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e : x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n
-- Mathlib/Data/Set/Lattice.lean
lemma kernImage_empty : kernImage f ∅ = (range f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ

Tactic:
rw [kernImage_eq_compl, compl_empty, image_univ]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem absdiscr_prime [IsCyclotomicExtension {p} ℚ K] :
    haveI : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
    NumberField.discr K = (-1) ^ (((p : ℕ) - 1) / 2) * p ^ ((p : ℕ) - 2)

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ NumberField.discr K = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by
  rw [zero_add, pow_one]
  infer_instance

Result:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ NumberField.discr K = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
rw [zero_add, pow_one]

Result:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p} ℚ K

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ NumberField.discr K = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Tactic:
rw [absdiscr_prime_pow_succ p 0 K]

Result:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ (-1) ^ (↑p ^ 0 * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1)) = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
⊢ IsCyclotomicExtension {p} ℚ K

Tactic:
infer_instance

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ ↑↑p ^ (↑p - 1 - 1) = ↑↑p ^ (↑p - 2)

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ (-1) ^ (↑p ^ 0 * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1)) = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)

Tactic:
simp only [Int.reduceNeg, pow_zero, one_mul, zero_add, mul_one, mul_eq_mul_left_iff, gt_iff_lt,
  Nat.cast_pos, PNat.pos, pow_eq_zero_iff', neg_eq_zero, one_ne_zero, ne_eq, false_and, or_false]

Result:
p : ℕ+
K : Type u
inst✝² : Field K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ ↑↑p ^ (↑p - 1 - 1) = ↑↑p ^ (↑p - 2)
-- Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean
theorem multiplicity_le : multiplicity E ≤ 5 ^ finrank ℝ E

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ multiplicity E ≤ 5 ^ finrank ℝ E

Tactic:
apply csSup_le

Result:
case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}.Nonempty

case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ ∀ b ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}, b ≤ 5 ^ finrank ℝ E

Proof state:
case h₂.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
h : (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ≤ 5 ^ finrank ℝ E

Tactic:
exact Besicovitch.card_le_of_separated s h.1 h.2

Result:
no goals

Proof state:
case h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ ∀ b ∈ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}, b ≤ 5 ^ finrank ℝ E

Tactic:
rintro _ ⟨s, ⟨rfl, h⟩⟩

Result:
case h₂.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
h : (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
⊢ s.card ≤ 5 ^ finrank ℝ E

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ ∅.card = 0 ∧ (∀ c ∈ ∅, ‖c‖ ≤ 2) ∧ ∀ c ∈ ∅, ∀ d ∈ ∅, c ≠ d → 1 ≤ ‖c - d‖

Tactic:
simp

Result:
no goals

Proof state:
case h₁
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ {N | ∃ s, s.card = N ∧ (∀ c ∈ s, ‖c‖ ≤ 2) ∧ ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖}.Nonempty

Tactic:
refine ⟨0, ⟨∅, by simp⟩⟩

Result:
no goals
-- Mathlib/Algebra/Lie/UniversalEnveloping.lean
theorem hom_ext {g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A}
    (h :
      (g₁ : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R) =
        (g₂ : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)) :
    g₁ = g₂ :=
  have h' : (lift R).symm g₁ = (lift R).symm g₂

Proof state:
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)
x✝ : L
⊢ ((lift R).symm g₁) x✝ = ((lift R).symm g₂) x✝

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)
⊢ (lift R).symm g₁ = (lift R).symm g₂

Tactic:
ext

Result:
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : g₁.toLieHom.comp (ι R) = g₂.toLieHom.comp (ι R)
x✝ : L
⊢ ((lift R).symm g₁) x✝ = ((lift R).symm g₂) x✝
-- Mathlib/Data/Real/Sign.lean
theorem sign_inv (r : ℝ) : sign r⁻¹ = sign r

Proof state:
r : ℝ
⊢ r⁻¹.sign = r.sign

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)

Result:
case inl
r : ℝ
hn : r < 0
⊢ r⁻¹.sign = r.sign

case inr.inl

⊢ 0⁻¹.sign = sign 0

case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign

Proof state:
case inr.inl

⊢ 0⁻¹.sign = sign 0

Tactic:
rw [sign_zero, inv_zero, sign_zero]

Result:
no goals

Proof state:
case inr.inr
r : ℝ
hp : 0 < r
⊢ r⁻¹.sign = r.sign

Tactic:
rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]

Result:
no goals

Proof state:
case inl
r : ℝ
hn : r < 0
⊢ r⁻¹.sign = r.sign

Tactic:
rw [sign_of_neg hn, sign_of_neg (inv_lt_zero.mpr hn)]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem full_empty : full ∅ = (⊥ : Subgroupoid C)

Proof state:
case arrows.h.h.h
C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full ∅).arrows x✝² x✝¹ ↔ x✝ ∈ ⊥.arrows x✝² x✝¹

Tactic:
simp only [Bot.bot, mem_full_iff, mem_empty_iff_false, and_self_iff]

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
⊢ full ∅ = ⊥

Tactic:
ext

Result:
case arrows.h.h.h
C : Type u
inst✝ : Groupoid C
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ x✝ ∈ (full ∅).arrows x✝² x✝¹ ↔ x✝ ∈ ⊥.arrows x✝² x✝¹
-- Mathlib/Topology/MetricSpace/Basic.lean
theorem isClosedEmbedding_of_pairwise_le_dist {α : Type*} [TopologicalSpace α] [DiscreteTopology α]
    {ε : ℝ} (hε : 0 < ε) {f : α → γ} (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) :
    IsClosedEmbedding f :=
  isClosedEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf

Proof state:
γ : Type w
inst✝² : MetricSpace γ
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ε : ℝ
hε : 0 < ε
f : α → γ
hf : Pairwise fun x y => ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y => (f x, f y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_nat (a : α) (n : ℕ) : ⌈a + n⌉ = ⌈a⌉ + n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌈a + ↑n⌉ = ⌈a⌉ + ↑n

Tactic:
rw [← Int.cast_natCast, ceil_add_int]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_pow_le {p : R[X]} {n : ℕ} : (p ^ n).natDegree ≤ n * p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).natDegree ≤ n * p.natDegree

Tactic:
induction n with
| zero => simp
| succ i hi =>
  rw [pow_succ, Nat.succ_mul]
  apply le_trans natDegree_mul_le (add_le_add_right hi _)

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).natDegree ≤ i * p.natDegree
⊢ (p ^ i * p).natDegree ≤ i * p.natDegree + p.natDegree

Tactic:
apply le_trans natDegree_mul_le (add_le_add_right hi _)

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).natDegree ≤ i * p.natDegree
⊢ (p ^ (i + 1)).natDegree ≤ (i + 1) * p.natDegree

Tactic:
rw [pow_succ, Nat.succ_mul]

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).natDegree ≤ i * p.natDegree
⊢ (p ^ i * p).natDegree ≤ i * p.natDegree + p.natDegree

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p ^ 0).natDegree ≤ 0 * p.natDegree

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem ofList_nil :
    ofList ([] : List (α × β)) = ∅

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
⊢ ofList [] = ∅

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
⊢ (Raw₀.Const.insertMany Raw₀.empty []).val.val = Raw₀.empty.val

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
⊢ (Raw₀.Const.insertMany Raw₀.empty []).val.val = Raw₀.empty.val

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem pos_eq_endPos {l r it} (h : ValidFor l r it) : it.2 = it.1.endPos ↔ r = []

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l = utf8Len l + utf8Len r ↔ r = []

Tactic:
exact (Nat.add_left_cancel_iff (m := 0)).trans <| eq_comm.trans utf8Len_eq_zero

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.i = it.s.endPos ↔ r = []

Tactic:
simp only [h.pos, h.toString, endPos_eq, utf8Len_reverseAux, Pos.ext_iff]

Result:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ utf8Len l = utf8Len l + utf8Len r ↔ r = []
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_centroidWeightsIndicator_eq_one_of_nonempty [CharZero k] [Fintype ι] (h : s.Nonempty) :
    ∑ i, s.centroidWeightsIndicator k i = 1

Proof state:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i : ι, centroidWeightsIndicator k s i = 1

Tactic:
rw [sum_centroidWeightsIndicator]

Result:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Proof state:
k : Type u_1
inst✝² : DivisionRing k
ι : Type u_4
s : Finset ι
inst✝¹ : CharZero k
inst✝ : Fintype ι
h : s.Nonempty
⊢ ∑ i ∈ s, centroidWeights k s i = 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_nonempty k h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getLast?_attach {xs : List α} :
    xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, mem_of_getLast? h⟩

Proof state:
α : Type u_1
xs : List α
⊢ Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (xs.reverse.head?.pbind fun a h => some ⟨a, ⋯⟩) =
    xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ xs.attach.getLast? = xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
rw [getLast?_eq_head?_reverse, reverse_attach, head?_map, head?_attach]

Result:
α : Type u_1
xs : List α
⊢ Option.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (xs.reverse.head?.pbind fun a h => some ⟨a, ⋯⟩) =
    xs.getLast?.pbind fun a h => some ⟨a, ⋯⟩
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem mapL_opNorm : ‖mapL f‖ ≤ ∏ i, ‖f i‖

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
m : (i : ι) → E i
⊢ ‖((tprodL 𝕜).compContinuousLinearMap f) m‖ ≤ (∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖

Tactic:
simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply]

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
m : (i : ι) → E i
⊢ ‖(tprodL 𝕜) fun i => (f i) (m i)‖ ≤ (∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ ‖mapL f‖ ≤ ∏ i : ι, ‖f i‖

Tactic:
rw [ContinuousLinearMap.opNorm_le_iff (by positivity)]

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ ∀ (x : ⨂[𝕜] (i : ι), E i), ‖(mapL f) x‖ ≤ (∏ i : ι, ‖f i‖) * ‖x‖

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ ∀ (x : ⨂[𝕜] (i : ι), E i), ‖(mapL f) x‖ ≤ (∏ i : ι, ‖f i‖) * ‖x‖

Tactic:
intro x

Result:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
E' : ι → Type u_1
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(mapL f) x‖ ≤ (∏ i : ι, ‖f i‖) * ‖x‖
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.lintegral_kernel {κ : Kernel α β} {f : β → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun a => ∫⁻ b, f b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
f : β → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun a => ∫⁻ (b : β), f b ∂κ a

Tactic:
fun_prop

Result:
no goals