harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Metrizable/Uniformity.lean
theorem UniformSpace.metrizable_uniformity (X : Type*) [UniformSpace X]
    [IsCountablyGenerated (𝓤 X)] : ∃ I : PseudoMetricSpace X, I.toUniformSpace = ‹_›

Proof state:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
⊢ ((1 / 2) ^ n ≤ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0) ↔ (x, y) ∉ U n

Tactic:
split_ifs with h

Result:
case pos
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
h : ∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ (1 / 2) ^ Nat.find h ↔ (x, y) ∉ U n

case neg
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → Set (X × X)
hU_symm : ∀ (n : ℕ), SymmetricRel (U n)
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : 1 / 2 ∈ Ioo 0 1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
x y : X
n : ℕ
h : ¬∃ n, (x, y) ∉ U n
⊢ (1 / 2) ^ n ≤ 0 ↔ (x, y) ∉ U n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_le_length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
    l.length ≤ (eraseKey k l).length + 1

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ l.length ≤ (if containsKey k l = true then l.length - 1 else l.length) + 1

Tactic:
split <;> omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ l.length ≤ (eraseKey k l).length + 1

Tactic:
rw [length_eraseKey]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
⊢ l.length ≤ (if containsKey k l = true then l.length - 1 else l.length) + 1
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem ext {e e' : PartialEquiv α β} (h : ∀ x, e x = e' x)
    (hsymm : ∀ x, e.symm x = e'.symm x) (hs : e.source = e'.source) : e = e'

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : e'.target = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'

Tactic:
cases e

Result:
case mk
α : Type u_1
β : Type u_2
e' : PartialEquiv α β
I' : ↑e' '' e'.source = e'.target
toFun✝ : α → β
invFun✝ : β → α
source✝ : Set α
target✝ : Set β
map_source'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → toFun✝ x ∈ target✝
map_target'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → invFun✝ x ∈ source✝
left_inv'✝ : ∀ ⦃x : α⦄, x ∈ source✝ → invFun✝ (toFun✝ x) = x
right_inv'✝ : ∀ ⦃x : β⦄, x ∈ target✝ → toFun✝ (invFun✝ x) = x
h :
  ∀ (x : α),
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
            map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }
        x =
      ↑e' x
hsymm :
  ∀ (x : β),
    ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
              map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm
        x =
      ↑e'.symm x
hs :
  { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.source =
    e'.source
A :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
    ↑e'
B :
  ↑{ toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
          map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.symm =
    ↑e'.symm
I :
  e'.target =
    { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
        map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ }.target
⊢ { toFun := toFun✝, invFun := invFun✝, source := source✝, target := target✝, map_source' := map_source'✝,
      map_target' := map_target'✝, left_inv' := left_inv'✝, right_inv' := right_inv'✝ } =
    e'

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : ↑e '' e.source = e.target
⊢ e = e'

Tactic:
have I' : e' '' e'.source = e'.target := e'.image_source_eq_target

Result:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), ↑e x = ↑e' x
hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x
hs : e.source = e'.source
A : ↑e = ↑e'
B : ↑e.symm = ↑e'.symm
I : ↑e '' e.source = e.target
I' : ↑e' '' e'.source = e'.target
⊢ e = e'
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio (f : ℝ → ℝ) {a : ℝ}
    (hf : Tendsto (deriv f) (𝓝[<] a) atTop) : ¬ DifferentiableWithinAt ℝ f (Iio a) a

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ False

Tactic:
have hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot := by
  rw [Pi.neg_def, deriv.neg']
  exact tendsto_neg_atTop_atBot.comp hf

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot
⊢ False

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (fun x => -deriv f x) (𝓝[<] a) atBot

Tactic:
exact tendsto_neg_atTop_atBot.comp hf

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (deriv (-f)) (𝓝[<] a) atBot

Tactic:
rw [Pi.neg_def, deriv.neg']

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ Tendsto (fun x => -deriv f x) (𝓝[<] a) atBot

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
⊢ ¬DifferentiableWithinAt ℝ f (Iio a) a

Tactic:
intro h

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ False

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atTop
h : DifferentiableWithinAt ℝ f (Iio a) a
hf' : Tendsto (deriv (-f)) (𝓝[<] a) atBot
⊢ False

Tactic:
exact not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio (-f) hf' h.neg

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem strictMono_y : StrictMono (yn a1)
  | _, 0, h => absurd h <| Nat.not_lt_zero _
  | m, n + 1, h => by
    have : yn a1 m ≤ yn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_y hl)
        fun e => by rw [e]
    simp only [yn_succ, gt_iff_lt]; refine lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)
    rw [← mul_one (yn a1 m)]
    exact mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a

Tactic:
refine lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ yn a1 m < yn a1 (n + 1)

Tactic:
have : yn a1 m ≤ yn a1 n :=
  Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_y hl)
    fun e => by rw [e]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < yn a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < yn a1 (n + 1)

Tactic:
simp only [yn_succ, gt_iff_lt]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
⊢ yn a1 m ≤ yn a1 n

Tactic:
rw [e]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n * a

Tactic:
rw [← mul_one (yn a1 m)]

Result:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a

Proof state:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a

Tactic:
exact mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
theorem blastShiftLeftConst.go_le_size (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
    (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size

Tactic:
unfold go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ aig.decls.size ≤
    (if hidx : curr < w then
            if hdist : curr < distance then
              let res := aig.mkConstCached false;
              let aig_1 := res.aig;
              let zeroRef := res.ref;
              let_fun hfinal := ⋯;
              let s := s.cast hfinal;
              let input := input.cast hfinal;
              let s := s.push zeroRef;
              go aig_1 input distance (curr + 1) ⋯ s
            else
              let s := s.push (input.get (curr - distance) ⋯);
              go aig input distance (curr + 1) ⋯ s
          else
            let_fun hcurr := ⋯;
            { aig := aig, vec := hcurr ▸ s }).aig.decls.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_eq_countP' {a : α} : count a = countP (· == a)

Proof state:
case h
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ count a l = countP (fun x => x == a) l

Tactic:
apply count_eq_countP

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
⊢ count a = countP fun x => x == a

Tactic:
funext l

Result:
case h
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ count a l = countP (fun x => x == a) l
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.map_desc (c : Cocone G) :
    colimMap α ≫ colimit.desc G c = colimit.desc F ((Cocones.precompose α).obj c)

Proof state:
case w
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
j : J
⊢ ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)

Tactic:
simp [← assoc, colimit.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
⊢ colimMap α ≫ desc G c = desc F ((Cocones.precompose α).obj c)

Tactic:
ext j

Result:
case w
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : Cocone G
j : J
⊢ ι F j ≫ colimMap α ≫ desc G c = ι F j ≫ desc F ((Cocones.precompose α).obj c)
-- Mathlib/RingTheory/LaurentSeries.lean
theorem intValuation_X : (idealX K).intValuationDef X = ↑(Multiplicative.ofAdd (-1 : ℤ))

Proof state:
K : Type u_2
inst✝ : Field K
⊢ (idealX K).intValuationDef X = ↑(Multiplicative.ofAdd (-1))

Tactic:
rw [← Polynomial.coe_X, ← intValuation_apply, ← intValuation_eq_of_coe]

Result:
K : Type u_2
inst✝ : Field K
⊢ (Polynomial.idealX K).intValuation Polynomial.X = ↑(Multiplicative.ofAdd (-1))

Proof state:
K : Type u_2
inst✝ : Field K
⊢ (Polynomial.idealX K).intValuation Polynomial.X = ↑(Multiplicative.ofAdd (-1))

Tactic:
apply intValuation_singleton _ Polynomial.X_ne_zero (by rfl)

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
⊢ (Polynomial.idealX K).asIdeal = Ideal.span {Polynomial.X}

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem indexesValues_eq_filter_enum (p : α → Prop) [DecidablePred p] (as : List α) :
    indexesValues p as = filter (p ∘ Prod.snd) (enum as)

Proof state:
α : Type u
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ indexesValues (fun b => decide (p b)) as = filter ((fun b => decide (p b)) ∘ Prod.snd) as.enum

Tactic:
simp (config := { unfoldPartialApp := true }) [indexesValues, foldrIdx_eq_foldr_enum, uncurry,
  filter_eq_foldr, cond_eq_if]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem srem_eq (x y : BitVec w) : srem x y =
  match x.msb, y.msb with
  | false, false => x % y
  | false, true  => x % (-y)
  | true,  false => - ((-x) % y)
  | true,  true  => -((-x) % (-y))

Proof state:
w : Nat
x y : BitVec w
⊢ x.srem y =
    match x.msb, y.msb with
    | false, false => x % y
    | false, true => x % -y
    | true, false => -(-x % y)
    | true, true => -(-x % -y)

Tactic:
rw [BitVec.srem]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.umod y
    | false, true => x.umod y.neg
    | true, false => (x.neg.umod y).neg
    | true, true => (x.neg.umod y.neg).neg) =
    match x.msb, y.msb with
    | false, false => x % y
    | false, true => x % -y
    | true, false => -(-x % y)
    | true, true => -(-x % -y)

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.umod y
    | false, true => x.umod y.neg
    | true, false => (x.neg.umod y).neg
    | true, true => (x.neg.umod y.neg).neg) =
    match x.msb, y.msb with
    | false, false => x % y
    | false, true => x % -y
    | true, false => -(-x % y)
    | true, true => -(-x % -y)

Tactic:
rcases x.msb <;> rcases y.msb <;> simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_insert [TopologicalSpace α] {x : α} {s : Set α} {C : ℝ} {g : α → E} {g' : α → F}
    (h : ‖g x‖ ≤ C * ‖g' x‖) : IsBigOWith C (𝓝[insert x s] x) g g' ↔
    IsBigOWith C (𝓝[s] x) g g'

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : TopologicalSpace α
x : α
s : Set α
C : ℝ
g : α → E
g' : α → F
h : ‖g x‖ ≤ C * ‖g' x‖
⊢ IsBigOWith C (𝓝[insert x s] x) g g' ↔ IsBigOWith C (𝓝[s] x) g g'

Tactic:
simp_rw [IsBigOWith_def, nhdsWithin_insert, eventually_sup, eventually_pure, h, true_and]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
@[to_additive]
lemma isBlock_iff_smul_eq_smul_of_nonempty :
    IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
⊢ IsBlock G B ↔ ∀ ⦃g₁ g₂ : G⦄, (g₁ • B ∩ g₂ • B).Nonempty → g₁ • B = g₂ • B

Tactic:
simp_rw [IsBlock, ← not_disjoint_iff_nonempty_inter, not_imp_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem neg {f : ∀ i, E i} (hf : Memℓp f p) : Memℓp (-f) p

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
⊢ Memℓp (-f) p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ Memℓp (-f) 0

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ⊤
⊢ Memℓp (-f) ⊤

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Memℓp (-f) p

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Memℓp (-f) p

Tactic:
apply memℓp_gen

Result:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Summable fun i => ‖(-f) i‖ ^ p.toReal

Proof state:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
hp : 0 < p.toReal
⊢ Summable fun i => ‖(-f) i‖ ^ p.toReal

Tactic:
simpa using hf.summable hp

Result:
no goals

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ {i | (-f) i ≠ 0}.Finite

Tactic:
simp [hf.finite_dsupport]

Result:
no goals

Proof state:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ⊤
⊢ BddAbove (Set.range fun i => ‖(-f) i‖)

Tactic:
simpa using hf.bddAbove

Result:
no goals

Proof state:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ⊤
⊢ Memℓp (-f) ⊤

Tactic:
apply memℓp_infty

Result:
case inr.inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f ⊤
⊢ BddAbove (Set.range fun i => ‖(-f) i‖)

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ Memℓp (-f) 0

Tactic:
apply memℓp_zero

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ {i | (-f) i ≠ 0}.Finite
-- Mathlib/GroupTheory/CoprodI.lean
theorem empty_of_word_prod_eq_one {w : Word H} (h : lift f w.prod = 1) :
    w = Word.empty

Proof state:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
h : (lift f) w.prod = 1
hnotempty : ¬w = Word.empty
⊢ False

Tactic:
obtain ⟨i, j, w, rfl⟩ := NeWord.of_word w hnotempty

Result:
case intro.intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
h : (lift f) w.toWord.prod = 1
hnotempty : ¬w.toWord = Word.empty
⊢ False

Proof state:
case intro.intro.intro
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
h : (lift f) w.toWord.prod = 1
hnotempty : ¬w.toWord = Word.empty
⊢ False

Tactic:
exact lift_word_prod_nontrivial_of_not_empty f hcard X hXnonempty hXdisj hpp w h

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
h : (lift f) w.prod = 1
⊢ w = Word.empty

Tactic:
by_contra hnotempty

Result:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
h : (lift f) w.prod = 1
hnotempty : ¬w = Word.empty
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
    a ∈ m → get? m a = some (get! m a)

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
a : α
⊢ a ∈ m → get? m a = some (get! m a)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_get!_of_contains

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma mulConst_inv_right (A B : Finset G) : σₘ[A, B⁻¹] = δₘ[A, B]

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A, B⁻¹] = δₘ[A, B]

Tactic:
rw [mulConst, divConst, ← div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/List/InsertIdx.lean
theorem getElem_insertIdx_add_succ (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length)
    (hk : n + k + 1 < (insertIdx n x l).length := (by
      rwa [length_insertIdx_of_le_length (by omega), Nat.succ_lt_succ_iff])) :
    (insertIdx n x l)[n + k + 1] = l[n + k]

Proof state:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < (insertIdx n x l).length

Tactic:
rwa [length_insertIdx_of_le_length (by omega), Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : optParam (n + k + 1 < (insertIdx n x l).length) ⋯
⊢ (insertIdx n x l)[n + k + 1] = l[n + k]

Tactic:
rw [getElem_insertIdx_of_ge (by omega)]

Result:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : optParam (n + k + 1 < (insertIdx n x l).length) ⋯
⊢ l[n + k + 1 - 1] = l[n + k]

Proof state:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n ≤ l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : optParam (n + k + 1 < (insertIdx n x l).length) ⋯
⊢ n + 1 ≤ n + k + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : optParam (n + k + 1 < (insertIdx n x l).length) ⋯
⊢ l[n + k + 1 - 1] = l[n + k]

Tactic:
simp only [Nat.add_one_sub_one]

Result:
no goals