harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {fallback : β a} {v : β k} : getValueCastD a (insertEntry k v l) fallback =
      if h : k == a then cast (congrArg β (eq_of_beq h)) v
      else getValueCastD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
fallback : β a
v : β k
⊢ getValueCastD a (insertEntry k v l) fallback = if h : (k == a) = true then cast ⋯ v else getValueCastD a l fallback

Tactic:
simp [getValueCastD_eq_getValueCast?, getValueCast?_insertEntry,
  apply_dite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma ker_eq_top_of_isEmpty (f : X.Hom Y) [IsEmpty X] : f.ker = ⊤ :=
  top_le_iff.mp (le_ofIdeals_iff.mpr fun U x _ ↦ by simpa using Subsingleton.elim _ _)

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : IsEmpty ↑↑X.toPresheafedSpace
U : ↑Y.affineOpens
x : ↑Γ(Y, ↑U)
x✝ : x ∈ ⊤.ideal U
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
simpa using Subsingleton.elim _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basis_singleton (i : ι) : Lagrange.basis {i} v i = 1

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i : ι
⊢ Lagrange.basis {i} v i = 1

Tactic:
rw [Lagrange.basis, erase_singleton, prod_empty]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma IsNClique.erase_of_mem (hs : G.IsNClique n s) (ha : a ∈ s) :
    G.IsNClique (n - 1) (s.erase a) where
  isClique := hs.isClique.subset <| by simp
  card_eq

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ ↑(s.erase a) ⊆ ↑s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
s : Finset α
a : α
inst✝ : DecidableEq α
hs : G.IsNClique n s
ha : a ∈ s
⊢ #(s.erase a) = n - 1

Tactic:
rw [card_erase_of_mem ha, hs.2]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracketWithin_swap : lieBracketWithin 𝕜 V W s = - lieBracketWithin 𝕜 W V s

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
⊢ lieBracketWithin 𝕜 V W s = -lieBracketWithin 𝕜 W V s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 V W s x = (-lieBracketWithin 𝕜 W V s) x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 V W s x = (-lieBracketWithin 𝕜 W V s) x

Tactic:
simp [lieBracketWithin]

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_length_eq {l : List (Option α)} :
    l.reduceOption.length = (l.filter Option.isSome).length

Proof state:
case nil
α : Type u_1
⊢ [].reduceOption.length = (filter Option.isSome []).length

Tactic:
simp_rw [reduceOption_nil, filter_nil, length]

Result:
no goals

Proof state:
case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length

Tactic:
cases hd <;> simp [hl]

Result:
no goals

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length = (filter Option.isSome l).length

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u_1
⊢ [].reduceOption.length = (filter Option.isSome []).length

case cons
α : Type u_1
hd : Option α
tl : List (Option α)
hl : tl.reduceOption.length = (filter Option.isSome tl).length
⊢ (hd :: tl).reduceOption.length = (filter Option.isSome (hd :: tl)).length
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem Cache.Inv_init : Inv ([] : CNF (CNFVar aig)) (mkArray aig.decls.size false) (by simp) where
  hmark

Proof state:
aig : AIG Nat
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool) (idx : Nat) (hbound : idx < aig.decls.size),
    (mkArray aig.decls.size false)[idx] = true →
      ∀ (heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv),
        (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true

Tactic:
intro lhs rhs linv rinv idx hbound hmarked heq

Result:
aig : AIG Nat
lhs rhs : Nat
linv rinv : Bool
idx : Nat
hbound : idx < aig.decls.size
hmarked : (mkArray aig.decls.size false)[idx] = true
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true

Proof state:
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ =
    projectRightAssign assign idx hbound

Tactic:
simp at hmark

Result:
no goals

Proof state:
aig : AIG Nat
⊢ (mkArray aig.decls.size false).size = aig.decls.size

Tactic:
simp

Result:
no goals

Proof state:
aig : AIG Nat
lhs rhs : Nat
linv rinv : Bool
idx : Nat
hbound : idx < aig.decls.size
hmarked : (mkArray aig.decls.size false)[idx] = true
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ (mkArray aig.decls.size false)[lhs] = true ∧ (mkArray aig.decls.size false)[rhs] = true

Tactic:
simp at hmarked

Result:
no goals

Proof state:
aig : AIG Nat
⊢ ∀ (assign : aig.CNFVar → Bool),
    CNF.eval assign [] = true →
      ∀ (idx : Nat) (hbound : idx < aig.decls.size),
        (mkArray aig.decls.size false)[idx] = true →
          ⟦projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ =
            projectRightAssign assign idx hbound

Tactic:
intro assign _ idx hbound hmark

Result:
aig : AIG Nat
assign : aig.CNFVar → Bool
_heval✝ : CNF.eval assign [] = true
idx : Nat
hbound : idx < aig.decls.size
hmark : (mkArray aig.decls.size false)[idx] = true
⊢ ⟦projectLeftAssign assign, { aig := aig, ref := { gate := idx, hgate := hbound } }⟧ =
    projectRightAssign assign idx hbound
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iInf_finset_image {f : γ → α} {g : α → β} {s : Finset γ} :
    ⨅ x ∈ s.image f, g x = ⨅ y ∈ s, g (f y)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : γ → α
g : α → β
s : Finset γ
⊢ ⨅ x ∈ image f s, g x = ⨅ y ∈ s, g (f y)

Tactic:
rw [← iInf_coe, coe_image, iInf_image, iInf_coe]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem Dom.bind {o : Part α} (h : o.Dom) (f : α → Part β) : o.bind f = f (o.get h)

Proof state:
case H.intro.intro
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (o.get h)

Tactic:
rwa [Part.get_eq_of_mem ha]

Result:
no goals

Proof state:
case H
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a ∈ o, b ∈ f a) → b ∈ f (o.get h)

Tactic:
rintro ⟨a, ha, hb⟩

Result:
case H.intro.intro
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
a : α
ha : a ∈ o
hb : b ∈ f a
⊢ b ∈ f (o.get h)

Proof state:
case H
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ o.bind f ↔ b ∈ f (o.get h)

Tactic:
simp only [Part.mem_bind_iff, exists_prop]

Result:
case H
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a ∈ o, b ∈ f a) ↔ b ∈ f (o.get h)

Proof state:
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
⊢ o.bind f = f (o.get h)

Tactic:
ext b

Result:
case H
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ b ∈ o.bind f ↔ b ∈ f (o.get h)

Proof state:
case H
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a ∈ o, b ∈ f a) ↔ b ∈ f (o.get h)

Tactic:
refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩

Result:
case H
α : Type u_1
β : Type u_2
o : Part α
h : o.Dom
f : α → Part β
b : β
⊢ (∃ a ∈ o, b ∈ f a) → b ∈ f (o.get h)
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem isCyclic_iff_exists_zpowers_eq_top [Group α] : IsCyclic α ↔ ∃ g : α, zpowers g = ⊤

Proof state:
α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, zpowers g = ⊤

Tactic:
simp only [eq_top_iff', mem_zpowers_iff]

Result:
α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, ∀ (x : α), ∃ k, g ^ k = x

Proof state:
α : Type u_1
inst✝ : Group α
⊢ IsCyclic α ↔ ∃ g, ∀ (x : α), ∃ k, g ^ k = x

Tactic:
exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem findEntryP?_eq (p : α → β → Bool) (l : AssocList α β) :
    findEntryP? p l = l.toList.find? fun (a, b) => p a b

Proof state:
α : Type u_1
β : Type u_2
p : α → β → Bool
l : AssocList α β
⊢ findEntryP? p l =
    List.find?
      (fun x =>
        match x with
        | (a, b) => p a b)
      l.toList

Tactic:
induction l <;> simp [findEntryP?, List.find?_cons]

Result:
case cons
α : Type u_1
β : Type u_2
p : α → β → Bool
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  findEntryP? p tail✝ =
    List.find?
      (fun x =>
        match x with
        | (a, b) => p a b)
      tail✝.toList
⊢ (bif p key✝ value✝ then some (key✝, value✝) else findEntryP? p tail✝) =
    match p key✝ value✝ with
    | true => some (key✝, value✝)
    | false => List.find? (fun x => p x.fst x.snd) tail✝.toList

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → β → Bool
key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ :
  findEntryP? p tail✝ =
    List.find?
      (fun x =>
        match x with
        | (a, b) => p a b)
      tail✝.toList
⊢ (bif p key✝ value✝ then some (key✝, value✝) else findEntryP? p tail✝) =
    match p key✝ value✝ with
    | true => some (key✝, value✝)
    | false => List.find? (fun x => p x.fst x.snd) tail✝.toList

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
theorem CostructuredArrow.overEquivPresheafCostructuredArrow_inverse_map_toOverCompYoneda
    {A : Cᵒᵖ ⥤ Type v} {T : Over A} {X : CostructuredArrow yoneda A}
    (f : (CostructuredArrow.toOver yoneda A).obj X ⟶ T) :
    (overEquivPresheafCostructuredArrow A).inverse.map
      (((CostructuredArrow.toOverCompYoneda A T).hom.app (op X) f)) =
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
        f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : (toOver yoneda A).obj X ⟶ T
⊢ (overEquivPresheafCostructuredArrow A).inverse.map ((toOverCompYoneda A T).hom.app (op X) f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
      f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Tactic:
simp [CostructuredArrow.toOverCompYoneda]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma ext_to (i j : ℤ) (hij : i + 1 = j) {A : C} {f g : A ⟶ (mappingCone φ).X i}
    (h₁ : f ≫ (fst φ).1.v i j hij = g ≫ (fst φ).1.v i j hij)
    (h₂ : f ≫ (snd φ).v i i (add_zero i) = g ≫ (snd φ).v i i (add_zero i)) :
    f = g :=
  homotopyCofiber.ext_to_X φ i j hij h₁ (by simpa [snd] using h₂)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
A : C
f g : A ⟶ (mappingCone φ).X i
h₁ : f ≫ (↑(fst φ)).v i j hij = g ≫ (↑(fst φ)).v i j hij
h₂ : f ≫ (snd φ).v i i ⋯ = g ≫ (snd φ).v i i ⋯
⊢ f ≫ homotopyCofiber.sndX φ i = g ≫ homotopyCofiber.sndX φ i

Tactic:
simpa [snd] using h₂

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
protected lemma _root_.Filter.HasBasis.uniformSpace_eq_bot {ι p} {s : ι → Set (α × α)}
    {u : UniformSpace α} (h : 𝓤[u].HasBasis p s) :
    u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y : α ↦ (x, y) ∉ s i

Proof state:
α : Type ua
ι : Sort u_2
p : ι → Prop
s : ι → Set (α × α)
u : UniformSpace α
h : (𝓤 α).HasBasis p s
⊢ u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y => (x, y) ∉ s i

Tactic:
simp [uniformSpace_eq_bot, h.mem_iff, subset_def, Pairwise, not_imp_not]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem coeff_hsum_eq_sum_of_subset {s : SummableFamily Γ R α} {g : Γ} {t : Finset α}
    (h : { a | (s a).coeff g ≠ 0 } ⊆ t) : s.hsum.coeff g = ∑ i ∈ t, (s i).coeff g

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ s.hsum.coeff g = ∑ i ∈ t, (s i).coeff g

Tactic:
simp only [coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)]

Result:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ ∑ i ∈ ⋯.toFinset, (s i).coeff g = ∑ i ∈ t, (s i).coeff g

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ ∑ i ∈ ⋯.toFinset, (s i).coeff g = ∑ i ∈ t, (s i).coeff g

Tactic:
exact sum_subset (Set.Finite.toFinset_subset.mpr h) (by simp)

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
t : Finset α
h : {a | (s a).coeff g ≠ 0} ⊆ ↑t
⊢ ∀ x ∈ t, x ∉ ⋯.toFinset → (s x).coeff g = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
theorem go_get_aux (aig : AIG BVBit) (a : Nat) (curr : Nat) (hcurr : curr ≤ w)
    (s : AIG.RefVec aig curr) :
    -- `hfoo` makes it possible to `generalize` below. With a concrete proof term this
    -- `generalize` would produce a type incorrect term as the proof term would talk about
    -- a `go` application instead of the fresh variable.
    ∀ (idx : Nat) (hidx : idx < curr) (hfoo),
        (go aig w a curr s hcurr).vec.get idx (by omega) = (s.get idx hidx).cast hfoo

Proof state:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
res : RefVecEntry BVBit w
h✝ : ¬curr < w
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ curr = w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig w a curr s hcurr).aig.decls.size),
    (go aig w a curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast hfoo

Tactic:
intro idx hidx

Result:
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig w a curr s hcurr).aig.decls.size),
    (go aig w a curr s hcurr).vec.get idx ⋯ = (s.get idx hidx).cast hfoo
-- Mathlib/Data/Nat/Factorial/Basic.lean
lemma two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n) !

Proof state:
case zero

⊢ 2 ^ 0 * 0! ≤ (2 * 0)!

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!

Tactic:
calc
  _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
    Nat.mul_le_mul_left _ (pow_le_pow_of_le_left (le_add_left _ _) _)
  _ ≤ _ := Nat.factorial_mul_pow_le_factorial

Result:
no goals

Proof state:
case succ
n : ℕ
⊢ 2 ^ (n + 1) * (n + 1)! ≤ (2 * (n + 1))!

Tactic:
rw [Nat.mul_comm, Nat.two_mul]

Result:
case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!

Proof state:
n : ℕ
⊢ 2 ^ n * n ! ≤ (2 * n)!

Tactic:
obtain _ | n := n

Result:
case zero

⊢ 2 ^ 0 * 0! ≤ (2 * 0)!

case succ
n : ℕ
⊢ 2 ^ (n + 1) * (n + 1)! ≤ (2 * (n + 1))!
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_int_mul_two_pi_sub_pi (n : ℤ) : cos (n * (2 * π) - π) = -1

Proof state:
n : ℤ
⊢ cos (↑n * (2 * π) - π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → R}
    (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
    Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
⊢ Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Tactic:
refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)

Result:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖

Tactic:
calc
  ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ :=
    norm_sum_le _ _
  _ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖ := by gcongr; apply norm_mul_le

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Tactic:
have :=
  summable_sum_mul_antidiagonal_of_summable_mul
    (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)

Result:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
⊢ Summable fun n => ‖∑ kl ∈ antidiagonal n, f kl.1 * g kl.2‖

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
⊢ ∑ kl ∈ antidiagonal n, ‖f kl.1 * g kl.2‖ ≤ ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖

Tactic:
gcongr

Result:
case h
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
i✝ : ℕ × ℕ
a✝ : i✝ ∈ antidiagonal n
⊢ ‖f i✝.1 * g i✝.2‖ ≤ ‖f i✝.1‖ * ‖g i✝.2‖

Proof state:
case h
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
this : Summable fun n => ∑ kl ∈ antidiagonal n, ‖f kl.1‖ * ‖g kl.2‖
n : ℕ
i✝ : ℕ × ℕ
a✝ : i✝ ∈ antidiagonal n
⊢ ‖f i✝.1 * g i✝.2‖ ≤ ‖f i✝.1‖ * ‖g i✝.2‖

Tactic:
apply norm_mul_le

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem nnnorm_changeOriginSeries_apply_le_tsum (k l : ℕ) (x : E) :
    ‖p.changeOriginSeries k l fun _ => x‖₊ ≤
      ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ * ‖x‖₊ ^ l

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ ‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ (∑' (x : { s // s.card = l }), ‖p (k + l)‖₊) * ∏ _i : Fin l, ‖x‖₊

Tactic:
exact (p.changeOriginSeries k l).le_of_opNNNorm_le (p.nnnorm_changeOriginSeries_le_tsum _ _) _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ ‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ ∑' (x_1 : { s // s.card = l }), ‖p (k + l)‖₊ * ‖x‖₊ ^ l

Tactic:
rw [NNReal.tsum_mul_right, ← Fin.prod_const]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ ‖(p.changeOriginSeries k l) fun x_1 => x‖₊ ≤ (∑' (x : { s // s.card = l }), ‖p (k + l)‖₊) * ∏ _i : Fin l, ‖x‖₊
-- Mathlib/Data/Fin/Parity.lean
lemma odd_iff_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : Odd k ↔ Odd k.val

Proof state:
case intro
n : ℕ
inst✝ : NeZero (n + n)
k : Fin (n + n)
⊢ Odd k → Odd ↑k

Tactic:
rintro ⟨l, rfl⟩

Result:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ↑(2 * l + 1)

Proof state:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Even (2 * ↑l)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ (2 * ↑l + 1) % (n + n) % 2 = 1

Tactic:
rw [Nat.mod_mod_of_dvd _ ⟨n, (two_mul n).symm⟩, ← Nat.odd_iff, Nat.odd_add_one,
  Nat.not_odd_iff_even]

Result:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Even (2 * ↑l)

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ Odd k ↔ Odd ↑k

Tactic:
rcases hn with ⟨n, rfl⟩

Result:
case intro
n : ℕ
inst✝ : NeZero (n + n)
k : Fin (n + n)
⊢ Odd k ↔ Odd ↑k

Proof state:
case intro
n : ℕ
inst✝ : NeZero (n + n)
k : Fin (n + n)
⊢ Odd k ↔ Odd ↑k

Tactic:
refine ⟨?_, odd_of_val⟩

Result:
case intro
n : ℕ
inst✝ : NeZero (n + n)
k : Fin (n + n)
⊢ Odd k → Odd ↑k

Proof state:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ↑(2 * l + 1)

Tactic:
rw [val_add, val_mul, val_one', show Fin.val 2 = 2 % _ from rfl]

Result:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ((2 % (n + n) * ↑l % (n + n) + 1 % (n + n)) % (n + n))

Proof state:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ((2 % (n + n) * ↑l % (n + n) + 1 % (n + n)) % (n + n))

Tactic:
simp only [Nat.mod_mul_mod, Nat.add_mod_mod, Nat.mod_add_mod, Nat.odd_iff]

Result:
case intro.intro
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ (2 * ↑l + 1) % (n + n) % 2 = 1
-- Mathlib/Data/Nat/Init.lean
/-- The product of two natural numbers is greater than 1 if and only if
  at least one of them is greater than 1 and both are positive. -/
lemma one_lt_mul_iff : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

Proof state:
case mp
m n : ℕ
h : 1 < m * n
h' : ¬(0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n))
⊢ False

Tactic:
simp only [Nat.le_zero, Decidable.not_and_iff_or_not_not, not_or, Nat.not_lt] at h'

Result:
case mp
m n : ℕ
h : 1 < m * n
h' : m = 0 ∨ n = 0 ∨ m ≤ 1 ∧ n ≤ 1
⊢ False

Proof state:
case mp
m n : ℕ
h : 1 < m * n
⊢ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

Tactic:
by_contra h'

Result:
case mp
m n : ℕ
h : 1 < m * n
h' : ¬(0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n))
⊢ False

Proof state:
case mpr.inl
m n : ℕ
h : 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
hm : 1 < m
⊢ 1 < m * n

Tactic:
exact Nat.mul_lt_mul_of_lt_of_le' hm h.2.1 Nat.zero_lt_one

Result:
no goals

Proof state:
case mpr
m n : ℕ
h : 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
⊢ 1 < m * n

Tactic:
obtain hm | hn := h.2.2

Result:
case mpr.inl
m n : ℕ
h : 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
hm : 1 < m
⊢ 1 < m * n

case mpr.inr
m n : ℕ
h : 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
hn : 1 < n
⊢ 1 < m * n

Proof state:
m n : ℕ
⊢ 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

Tactic:
constructor <;> intro h

Result:
case mp
m n : ℕ
h : 1 < m * n
⊢ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

case mpr
m n : ℕ
h : 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
⊢ 1 < m * n

Proof state:
case mp.inr.inl
m : ℕ
h : 1 < m * 0
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case mp.inr.inr
m n : ℕ
h : 1 < m * n
h' : m ≤ 1 ∧ n ≤ 1
⊢ False

Tactic:
exact Nat.not_lt_of_le (Nat.mul_le_mul h'.1 h'.2) h

Result:
no goals

Proof state:
case mp.inl
n : ℕ
h : 1 < 0 * n
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case mp
m n : ℕ
h : 1 < m * n
h' : m = 0 ∨ n = 0 ∨ m ≤ 1 ∧ n ≤ 1
⊢ False

Tactic:
obtain rfl | rfl | h' := h'

Result:
case mp.inl
n : ℕ
h : 1 < 0 * n
⊢ False

case mp.inr.inl
m : ℕ
h : 1 < m * 0
⊢ False

case mp.inr.inr
m n : ℕ
h : 1 < m * n
h' : m ≤ 1 ∧ n ≤ 1
⊢ False

Proof state:
case mpr.inr
m n : ℕ
h : 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
hn : 1 < n
⊢ 1 < m * n

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt h.1 hn h.1

Result:
no goals