harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIso.inv_snd_snd :
    (pullbackDiagonalMapIso f i i₁ i₂).inv ≫ pullback.snd _ _ ≫ pullback.snd _ _ =
      pullback.snd _ _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    snd i₁ i₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    snd i₁ i₂

Tactic:
delta pullbackDiagonalMapIso

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv ≫
      snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) =
    snd i₁ i₂
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_X_mul (p : R[X]) : reverse (X * p) = reverse p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (X * p).reverse = p.reverse

Tactic:
rw [commute_X p, reverse_mul_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
    (h : m.WF) : k ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
⊢ k ∈ alter m k f ↔ (f (get? m k)).isSome = true

Tactic:
rw [mem_iff_contains, contains_alter_self h]

Result:
no goals
-- Mathlib/Algebra/Ring/Commute.lean
protected lemma sq_eq_sq_iff_eq_or_eq_neg {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_insertIfNew [LawfulBEq α] {k a : α} [Inhabited (β a)] {v : β k} :
    (m.insertIfNew k v).get! a =
      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v else m.get! a

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get! a

Tactic:
exact Raw₀.get!_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get! a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ (m.insertIfNew k v).get! a = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get! a
-- Mathlib/Algebra/Group/Subgroup/MulOpposite.lean
theorem unop_normalizer (H : Subgroup Gᵐᵒᵖ) : H.normalizer.unop = H.unop.normalizer

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.normalizer.unop = H.unop.normalizer

Tactic:
rw [← op_inj, op_unop, op_normalizer, op_unop]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_sq_div_one_add_tan_sq {x : ℝ} (hx : cos x ≠ 0) :
    tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2

Proof state:
x : ℝ
hx : cos x ≠ 0
⊢ tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2

Tactic:
simp only [← tan_mul_cos hx, mul_pow, ← inv_one_add_tan_sq hx, div_eq_mul_inv, one_mul]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma covBy_iff_card_sdiff_eq_one : t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1

Proof state:
case mp
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1

Tactic:
rintro ⟨a, ha, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
t : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ t
⊢ t ⊆ insert a t ∧ #(insert a t \ t) = 1

Proof state:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s

Tactic:
simp_rw [card_eq_one]

Result:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (t ⊆ s ∧ ∃ a, s \ t = {a}) → ∃ a ∉ t, insert a t = s

Proof state:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (t ⊆ s ∧ ∃ a, s \ t = {a}) → ∃ a ∉ t, insert a t = s

Tactic:
rintro ⟨hts, a, ha⟩

Result:
case mpr.intro.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ ∃ a ∉ t, insert a t = s

Proof state:
case mp.intro.intro
α : Type u_1
t : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ t
⊢ t ⊆ insert a t ∧ #(insert a t \ t) = 1

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⋖ s ↔ t ⊆ s ∧ #(s \ t) = 1

Tactic:
rw [covBy_iff_exists_insert]

Result:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1

Proof state:
case mpr.intro.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ ∃ a ∉ t, insert a t = s

Tactic:
refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩

Result:
case mpr.intro.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ insert a t = s

Proof state:
case mpr.intro.intro
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ insert a t = s

Tactic:
rw [insert_eq, ← ha, sdiff_union_of_subset hts]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1

Tactic:
constructor

Result:
case mp
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1

case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_zero_one_iff {x : R} : Sbtw R 0 x 1 ↔ x ∈ Set.Ioo (0 : R) 1

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ Sbtw R 0 x 1 ↔ x ∈ Set.Ioo 0 1

Tactic:
rw [Sbtw, wbtw_zero_one_iff, Set.mem_Icc, Set.mem_Ioo]

Result:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ (0 ≤ x ∧ x ≤ 1) ∧ x ≠ 0 ∧ x ≠ 1 ↔ 0 < x ∧ x < 1

Tactic:
exact
  ⟨fun h => ⟨h.1.1.lt_of_ne (Ne.symm h.2.1), h.1.2.lt_of_ne h.2.2⟩, fun h =>
    ⟨⟨h.1.le, h.2.le⟩, h.1.ne', h.2.ne⟩⟩

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma le_min (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : ¬a ≤ b
⊢ c ≤ min a b

Tactic:
simpa [min_def, if_neg h] using h₂

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : a ≤ b
⊢ c ≤ min a b

Tactic:
simpa [min_def, if_pos h] using h₁

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ min a b

Tactic:
if h : a ≤ b
then simpa [min_def, if_pos h] using h₁
else simpa [min_def, if_neg h] using h₂

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_le_max_abs_abs (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max |a| |c| :=
  abs_le'.2
    ⟨by simp [hbc.trans (le_abs_self c)], by
      simp [(neg_le_neg_iff.mpr hab).trans (neg_le_abs a)]⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ≤ |a| ⊔ |c|

Tactic:
simp [hbc.trans (le_abs_self c)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ -b ≤ |a| ⊔ |c|

Tactic:
simp [(neg_le_neg_iff.mpr hab).trans (neg_le_abs a)]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
lemma Codisjoint.eq_iff (hab : Codisjoint a b) : a = b ↔ a = ⊤ ∧ b = ⊤

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a b : α
hab : Codisjoint a b
⊢ a = b ↔ a = ⊤ ∧ b = ⊤

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
@[gcongr] lemma take_prefix_take_left (h : m ≤ n) : a.take m <+: a.take n

Proof state:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a = List.take m (take n a)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a

Tactic:
apply List.take_prefix

Result:
no goals

Proof state:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ take m a <+: take n a

Tactic:
rw [(by simp [h] : a.take m = (a.take n).take m)]

Result:
α : Type u
m n : ℕ
a : Stream' α
h : m ≤ n
⊢ List.take m (take n a) <+: take n a
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.Represents.zero : (0 : Matrix ι ι R).Represents b 0

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ Represents b 0 0

Tactic:
delta Matrix.Represents

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ (PiToModule.fromMatrix R b) 0 = (PiToModule.fromEnd R b) 0

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
⊢ (PiToModule.fromMatrix R b) 0 = (PiToModule.fromEnd R b) 0

Tactic:
rw [map_zero, map_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Yoneda.lean
lemma preadditiveYoneda_shiftMap_apply (B : C) {X Y : Cᵒᵖ} (n : ℤ) (f : X ⟶ Y⟦n⟧)
    (a a' : ℤ) (h : n + a = a') (z : X.unop ⟶ B⟦a⟧) :
    (preadditiveYoneda.obj B).shiftMap f a a' h z =
      ((ShiftedHom.opEquiv _).symm f).comp z (show a + n = a' by omega)

Proof state:
C : Type u_1
inst✝³ : Category.{?u.23756, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ a + n = a'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ ((ShiftedHom.opEquiv n).symm f).comp z ⋯ = (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z

Tactic:
apply ShiftedHom.opEquiv_symm_apply_comp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z = ((ShiftedHom.opEquiv n).symm f).comp z ⋯

Tactic:
symm

Result:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
X Y : Cᵒᵖ
n : ℤ
f : X ⟶ (shiftFunctor Cᵒᵖ n).obj Y
a a' : ℤ
h : n + a = a'
z : unop X ⟶ (shiftFunctor C a).obj B
⊢ ((ShiftedHom.opEquiv n).symm f).comp z ⋯ = (ConcreteCategory.hom ((preadditiveYoneda.obj B).shiftMap f a a' h)) z
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem denote_input_entry (entry : Entrypoint α) {input : β entry.aig len} {h} :
    ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign ⟧
      =
    ⟦entry, assign⟧ :=  by
  apply denote.eq_of_isPrefix
  apply isPrefix_aig

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ ⟦assign, { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧

Tactic:
apply denote.eq_of_isPrefix

Result:
case hprefix
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls

Proof state:
case hprefix
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls

Tactic:
apply isPrefix_aig

Result:
no goals
-- Mathlib/Analysis/SumOverResidueClass.lean
lemma Finset.sum_indicator_mod {R : Type*} [AddCommMonoid R] (m : ℕ) [NeZero m] (f : ℕ → R) :
    f = ∑ a : ZMod m, {n : ℕ | (n : ZMod m) = a}.indicator f

Proof state:
case h
R : Type u_1
inst✝¹ : AddCommMonoid R
m : ℕ
inst✝ : NeZero m
f : ℕ → R
n : ℕ
⊢ f n = (∑ a : ZMod m, {n | ↑n = a}.indicator f) n

Tactic:
simp only [Finset.sum_apply, Set.indicator_apply, Set.mem_setOf_eq, Finset.sum_ite_eq,
  Finset.mem_univ, ↓reduceIte]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : AddCommMonoid R
m : ℕ
inst✝ : NeZero m
f : ℕ → R
⊢ f = ∑ a : ZMod m, {n | ↑n = a}.indicator f

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝¹ : AddCommMonoid R
m : ℕ
inst✝ : NeZero m
f : ℕ → R
n : ℕ
⊢ f n = (∑ a : ZMod m, {n | ↑n = a}.indicator f) n
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_measure_zero {f : α → ε} : eLpNorm f p (0 : Measure α) = 0

Proof state:
case neg
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : ¬p = 0
⊢ eLpNorm f p 0 = 0

Tactic:
by_cases h_top : p = ∞

Result:
case pos
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm f p 0 = 0

case neg
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm f p 0 = 0

Proof state:
case pos
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : p = 0
⊢ eLpNorm f p 0 = 0

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : ¬p = 0
h_top : ¬p = ⊤
⊢ eLpNorm f p 0 = 0

Tactic:
rw [← Ne] at h0

Result:
case neg
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm f p 0 = 0

Proof state:
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
⊢ eLpNorm f p 0 = 0

Tactic:
by_cases h0 : p = 0

Result:
case pos
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : p = 0
⊢ eLpNorm f p 0 = 0

case neg
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : ¬p = 0
⊢ eLpNorm f p 0 = 0

Proof state:
case neg
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : p ≠ 0
h_top : ¬p = ⊤
⊢ eLpNorm f p 0 = 0

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm', ENNReal.toReal_pos h0 h_top]

Result:
no goals

Proof state:
case pos
α : Type u_1
ε : Type u_2
p : ℝ≥0∞
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
h0 : ¬p = 0
h_top : p = ⊤
⊢ eLpNorm f p 0 = 0

Tactic:
simp [h_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
    a.pred ha ≤ b.pred hb ↔ a ≤ b

Proof state:
n : Nat
a b : Fin n.succ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.pred ha ≤ b.pred hb ↔ a ≤ b

Tactic:
rw [← succ_le_succ_iff, succ_pred, succ_pred]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_le {s₁ s₂ : AffineSubspace k P} (h : s₁ ≤ s₂) : s₁.direction ≤ s₂.direction

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ≤ s₂
⊢ s₁.direction ≤ s₂.direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ≤ s₂
⊢ Submodule.span k (↑s₁ -ᵥ ↑s₁) ≤ Submodule.span k (↑s₂ -ᵥ ↑s₂)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ≤ s₂
⊢ Submodule.span k (↑s₁ -ᵥ ↑s₁) ≤ Submodule.span k (↑s₂ -ᵥ ↑s₂)

Tactic:
exact vectorSpan_mono k h

Result:
no goals
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
@[fun_prop]
lemma continuous_choose (k : ℕ) : Continuous (fun x : ℤ_[p] ↦ Ring.choose x k)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x => Ring.choose x k

Tactic:
simp only [Ring.choose]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x => Ring.multichoose (x - ↑k + 1) k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x => Ring.multichoose (x - ↑k + 1) k

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_ne {a a' : α} {f : α →₀ M} (h : a' ≠ a) : (f.erase a) a' = f a'

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ (erase a f) a' = f a'

Tactic:
classical simp only [erase, coe_mk, h, ite_false]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a a' : α
f : α →₀ M
h : a' ≠ a
⊢ (erase a f) a' = f a'

Tactic:
simp only [erase, coe_mk, h, ite_false]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem smul_univ [Fintype β] {s : Finset α} (hs : s.Nonempty) : s • (univ : Finset β) = univ :=
  coe_injective <| by
    push_cast
    exact Set.smul_univ hs

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑(s • univ) = ↑univ

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑s • Set.univ = Set.univ

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : s.Nonempty
⊢ ↑s • Set.univ = Set.univ

Tactic:
exact Set.smul_univ hs

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma divisors_filter_dvd_of_dvd {n m : ℕ} (hn : n ≠ 0) (hm : m ∣ n) :
    {d ∈ n.divisors | d ∣ m} = m.divisors

Proof state:
case h
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ k ∈ filter (fun d => d ∣ m) n.divisors ↔ k ∈ m.divisors

Tactic:
simp_rw [mem_filter, mem_divisors]

Result:
case h
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0

Proof state:
case h
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0

Tactic:
exact ⟨fun ⟨_, hkm⟩ ↦ ⟨hkm, ne_zero_of_dvd_ne_zero hn hm⟩, fun ⟨hk, _⟩ ↦ ⟨⟨hk.trans hm, hn⟩, hk⟩⟩

Result:
no goals

Proof state:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
⊢ filter (fun d => d ∣ m) n.divisors = m.divisors

Tactic:
ext k

Result:
case h
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ k ∈ filter (fun d => d ∣ m) n.divisors ↔ k ∈ m.divisors
-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_isSubordinate [NormalSpace X] [ParacompactSpace X] (hs : IsClosed s) (U : ι → Set X)
    (ho : ∀ i, IsOpen (U i)) (hU : s ⊆ ⋃ i, U i) : ∃ f : BumpCovering ι X s, f.IsSubordinate U

Proof state:
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, f.IsSubordinate U

Tactic:
rcases exists_isSubordinate_of_locallyFinite hs V hVo hVf hsV with ⟨f, hf⟩

Result:
case intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : f.IsSubordinate V
⊢ ∃ f, f.IsSubordinate U

Proof state:
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
⊢ ∃ f, f.IsSubordinate U

Tactic:
rcases precise_refinement_set hs _ ho hU with ⟨V, hVo, hsV, hVf, hVU⟩

Result:
case intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
⊢ ∃ f, f.IsSubordinate U

Proof state:
case intro.intro.intro.intro.intro
ι : Type u
X : Type v
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : NormalSpace X
inst✝ : ParacompactSpace X
hs : IsClosed s
U : ι → Set X
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ i, U i
V : ι → Set X
hVo : ∀ (i : ι), IsOpen (V i)
hsV : s ⊆ ⋃ i, V i
hVf : LocallyFinite V
hVU : ∀ (i : ι), V i ⊆ U i
f : BumpCovering ι X s
hf : f.IsSubordinate V
⊢ ∃ f, f.IsSubordinate U

Tactic:
exact ⟨f, hf.mono hVU⟩

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Under/Basic.lean
@[ext]
lemma mkUnder_ext {A : Type u} [CommRing A] [Algebra R A] {B : Under R}
    {f g : mkUnder R A ⟶ B} (h : ∀ a : A, f.right a = g.right a) :
    f = g

Proof state:
R : CommRingCat
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra (↑R) A
B : Under R
f g : R.mkUnder A ⟶ B
h : ∀ (a : A), (ConcreteCategory.hom f.right) a = (ConcreteCategory.hom g.right) a
⊢ f = g

Tactic:
ext x

Result:
case h.hf.a
R : CommRingCat
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra (↑R) A
B : Under R
f g : R.mkUnder A ⟶ B
h : ∀ (a : A), (ConcreteCategory.hom f.right) a = (ConcreteCategory.hom g.right) a
x : ↑(R.mkUnder A).right
⊢ (Hom.hom f.right) x = (Hom.hom g.right) x

Proof state:
case h.hf.a
R : CommRingCat
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra (↑R) A
B : Under R
f g : R.mkUnder A ⟶ B
h : ∀ (a : A), (ConcreteCategory.hom f.right) a = (ConcreteCategory.hom g.right) a
x : ↑(R.mkUnder A).right
⊢ (Hom.hom f.right) x = (Hom.hom g.right) x

Tactic:
exact h x

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
/-- This is a special case of `tsub_le_iff_left`, which should be used instead of this. -/
protected lemma sub_le_iff_le_add' : s - t ≤ u ↔ s ≤ t + u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s - t ≤ u ↔ s ≤ t + u

Tactic:
rw [Multiset.sub_le_iff_le_add, Multiset.add_comm]

Result:
no goals