harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem pow_right_strictMono' (ha : 1 < a) : StrictMono ((a ^ ·) : ℕ → M) :=
  strictMono_nat_of_lt_succ fun n ↦ by rw [pow_succ]; exact lt_mul_of_one_lt_right' (a ^ n) ha

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a

Tactic:
exact lt_mul_of_one_lt_right' (a ^ n) ha

Result:
no goals

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
rw [pow_succ]

Result:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftStrictMono M
a : M
ha : 1 < a
n : ℕ
⊢ a ^ n < a ^ n * a
-- Mathlib/Data/Set/NAry.lean
theorem image2_congr (h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b) : image2 f s t = image2 f' s t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
⊢ image2 f s t = image2 f' s t

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ image2 f' s t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b = f' a b

Tactic:
rw [h a ha b hb]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
f f' : α → β → γ
s : Set α
t : Set β
h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ image2 f' s t

Tactic:
constructor <;> rintro ⟨a, ha, b, hb, rfl⟩ <;> exact ⟨a, ha, b, hb, by rw [h a ha b hb]⟩

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_ordCompl (n p : ℕ) :
    (ordCompl[p] n).factorization = n.factorization.erase p

Proof state:
case h.inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ ¬False ∨ n / q ^ n.factorization q = 0

Tactic:
simp

Result:
no goals

Proof state:
n p : ℕ
hn : ¬n = 0
pp : Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
ext q

Result:
case h
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Proof state:
case h.inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
rw [Finsupp.erase_ne hqp, factorization_div (ordProj_dvd n p)]

Result:
case h.inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q

Proof state:
n p : ℕ
hn : ¬n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
if pp : p.Prime then ?_ else
  rw [Finsupp.erase_of_not_mem_support] <;> simp [pp]

Result:
n p : ℕ
hn : ¬n = 0
pp : Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Proof state:
n p : ℕ
hn : n = 0
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
simp [hn]

Result:
no goals

Proof state:
n p : ℕ
hn : ¬n = 0
pp : ¬Prime p
⊢ (n / p ^ n.factorization p).factorization = Finsupp.erase p n.factorization

Tactic:
rw [Finsupp.erase_of_not_mem_support] <;> simp [pp]

Result:
no goals

Proof state:
case h.inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q

Tactic:
simp only [Finsupp.erase_same, factorization_eq_zero_iff, not_dvd_ordCompl pp hn]

Result:
case h.inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ ¬Prime q ∨ ¬False ∨ n / q ^ n.factorization q = 0

Proof state:
case h.inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n.factorization - (p ^ n.factorization p).factorization) q = n.factorization q

Tactic:
simp [pp.factorization, hqp.symm]

Result:
no goals

Proof state:
case h
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q

Tactic:
rcases eq_or_ne q p with (rfl | hqp)

Result:
case h.inl
n : ℕ
hn : ¬n = 0
q : ℕ
pp : Prime q
⊢ (n / q ^ n.factorization q).factorization q = (Finsupp.erase q n.factorization) q

case h.inr
n p : ℕ
hn : ¬n = 0
pp : Prime p
q : ℕ
hqp : q ≠ p
⊢ (n / p ^ n.factorization p).factorization q = (Finsupp.erase p n.factorization) q
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.emultiplicity_le_of_multiplicity_le (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : multiplicity a b ≤ n) : emultiplicity a b ≤ n

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ ↑(multiplicity a b) ≤ ↑n

Tactic:
assumption_mod_cast

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ emultiplicity a b ≤ ↑n

Tactic:
rw [emultiplicity_eq_multiplicity hfin]

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ ↑(multiplicity a b) ≤ ↑n
-- Mathlib/Algebra/Jordan/Basic.lean
theorem aux0 {a b c : A} : ⁅L (a + b + c), L ((a + b + c) * (a + b + c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) +
    2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Proof state:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * (a + b + c) + b * (a + b + c) + c * (a + b + c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆

Tactic:
iterate 6 rw [mul_add]

Result:
A : Type u_1
inst✝ : NonUnitalNonAssocCommRing A
a b c : A
⊢ ⁅L (a + b + c), L (a * a + a * b + a * c + (b * a + b * b + b * c) + (c * a + c * b + c * c))⁆ =
    ⁅L a + L b + L c, L (a * a) + L (b * b) + L (c * c) + 2 • L (a * b) + 2 • L (c * a) + 2 • L (b * c)⁆
-- Mathlib/Data/Set/Prod.lean
theorem prod_empty : s ×ˢ (∅ : Set β) = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
⊢ s ×ˢ ∅ = ∅

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅

Tactic:
exact iff_of_eq (and_false _)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem borel_eq_top_of_countable {α : Type*} [TopologicalSpace α] [T0Space α] [Countable α] :
    borel α = ⊤

Proof state:
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ MeasurableSet s

Tactic:
exact .of_discrete

Result:
no goals

Proof state:
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
borelize α

Result:
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ MeasurableSet s

Proof state:
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
⊢ borel α = ⊤

Tactic:
refine top_unique fun s _ ↦ ?_

Result:
α : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet s
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma alternatingMapLinearEquiv_ιMulti :
    alternatingMapLinearEquiv (ιMulti R n (M := M)) = LinearMap.id

Proof state:
case heq.H.a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Fin n → M
⊢ ↑(((alternatingMapLinearEquiv (ιMulti R n)).compAlternatingMap (ιMulti R n)) x✝) =
    ↑((LinearMap.id.compAlternatingMap (ιMulti R n)) x✝)

Tactic:
simp only [alternatingMapLinearEquiv_comp_ιMulti, ιMulti_apply_coe,
  LinearMap.compAlternatingMap_apply, LinearMap.id_coe, id_eq]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ alternatingMapLinearEquiv (ιMulti R n) = LinearMap.id

Tactic:
ext

Result:
case heq.H.a
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : Fin n → M
⊢ ↑(((alternatingMapLinearEquiv (ιMulti R n)).compAlternatingMap (ιMulti R n)) x✝) =
    ↑((LinearMap.id.compAlternatingMap (ιMulti R n)) x✝)
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₁_eq' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) :
    K.d₁ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.d i₁ i₁').f i₂ ≫
      K.toGradedObject.ιMapObjOrZero (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁', i₂⟩ i₁₂)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ i₁' : I₁
h : c₁.Rel i₁ i₁'
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂

Tactic:
obtain rfl := c₁.next_eq' h

Result:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Sbtw.oangle₃₂₁_eq_pi {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∡ p₃ p₂ p₁ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∡ p₃ p₂ p₁ = ↑π

Tactic:
rw [oangle_eq_pi_iff_oangle_rev_eq_pi, ← h.oangle₁₂₃_eq_pi]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[simp]
lemma image_top_eq_opensRange : f ''ᵁ ⊤ = f.opensRange

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
⊢ f ''ᵁ ⊤ = f.opensRange

Tactic:
apply Opens.ext

Result:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
⊢ ↑(f ''ᵁ ⊤) = ↑f.opensRange

Proof state:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
⊢ ↑(f ''ᵁ ⊤) = ↑f.opensRange

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem add_eq_max_of_ne {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) :
    padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

Tactic:
wlog hlt : padicNorm p r < padicNorm p q

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
this :
  ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
    padicNorm p q ≠ padicNorm p r → padicNorm p r < padicNorm p q → padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r
hlt : ¬padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r

p✝ p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hne : padicNorm p q ≠ padicNorm p r
hlt : padicNorm p r < padicNorm p q
⊢ padicNorm p (q + r) = padicNorm p q ⊔ padicNorm p r
-- Mathlib/RingTheory/Regular/RegularSequence.lean
@[simp]
lemma isRegular_cons_iff (r : R) (rs : List R) :
    IsRegular M (r :: rs) ↔
      IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ IsRegular (QuotSMulTop r M) rs

Tactic:
rw [isRegular_iff, isRegular_iff, isWeaklyRegular_cons_iff M r rs,
  ne_eq, top_eq_ofList_cons_smul_iff, and_assoc]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem balRight_toList {l : RBNode α} {v r} :
    (l.balRight v r).toList = l.toList ++ v :: r.toList

Proof state:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
⊢ (match l with
      | node black a x b => (node red a x b).balance1 v r
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r)
      | l => node red l v r).toList =
    l.toList ++ v :: r.toList

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balRight v r).toList = l.toList ++ v :: r.toList

Tactic:
unfold balRight

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match r with
      | node red b y c => node red l v (node black b y c)
      | r =>
        match l with
        | node black a x b => (node red a x b).balance1 v r
        | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r)
        | l => node red l v r).toList =
    l.toList ++ v :: r.toList

Proof state:
case h_1
α : Type u_1
l : RBNode α
v : α
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ (node red l v (node black a✝ x✝ b✝)).toList = l.toList ++ v :: (node red a✝ x✝ b✝).toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match r with
      | node red b y c => node red l v (node black b y c)
      | r =>
        match l with
        | node black a x b => (node red a x b).balance1 v r
        | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r)
        | l => node red l v r).toList =
    l.toList ++ v :: r.toList

Tactic:
split <;> (try simp)

Result:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
⊢ (match l with
      | node black a x b => (node red a x b).balance1 v r
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r)
      | l => node red l v r).toList =
    l.toList ++ v :: r.toList

Proof state:
case h_1
α : Type u_1
l : RBNode α
v : α
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ (node red l v (node black a✝ x✝ b✝)).toList = l.toList ++ v :: (node red a✝ x✝ b✝).toList

Tactic:
try simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_mul_left : ∑' i, a * f i = a * ∑' i, f i

Proof state:
case pos
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
simp [hf]

Result:
no goals

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ Tendsto (fun s => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
simp only [← Finset.mul_sum]

Result:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ Tendsto (fun s => a * ∑ i ∈ s, f i) atTop (𝓝 (a * ∑' (i : α), f i))

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ Tendsto (fun s => a * ∑ i ∈ s, f i) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)

Result:
no goals

Proof state:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) := by
  simp only [← Finset.mul_sum]
  exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)

Result:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
this : Tendsto (fun s => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Proof state:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
rw [← ENNReal.tsum_eq_zero] at hf

Result:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
by_cases hf : ∀ i, f i = 0

Result:
case pos
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Proof state:
case neg
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∑' (i : α), f i = 0
this : Tendsto (fun s => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
exact HasSum.tsum_eq this

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_empty_right : s ○ ∅ = ∅

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s : Finset α
⊢ s ○ ∅ = ∅

Tactic:
simp [disjSups]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_fun [Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α

Tactic:
rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem sq_mul_squarefree_of_pos' {n : ℕ} (h : 0 < n) :
    ∃ a b : ℕ, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)

Proof state:
case intro.intro.intro.intro.intro
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
refine ⟨a₁.pred, b₁.pred, ?_, ?_⟩ <;> simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]

Result:
no goals

Proof state:
n : ℕ
h : 0 < n
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)

Tactic:
obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h

Result:
case intro.intro.intro.intro.intro
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma inv_hom_apply {R S : CommSemiRingCat} (e : R ≅ S) (r : R) : e.inv (e.hom r) = r

Proof state:
R S : CommSemiRingCat
e : R ≅ S
r : ↑R
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_le_one_of_mem {x : E} (hx : x ∈ s) : gauge s x ≤ 1 :=
  gauge_le_of_mem zero_le_one <| by rwa [one_smul]

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
hx : x ∈ s
⊢ x ∈ 1 • s

Tactic:
rwa [one_smul]

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem pairwise_le_finRange (n : ℕ) : Pairwise (· ≤ ·) (finRange n)

Proof state:
n : ℕ
⊢ ∀ x ∈ range n, x < n

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ Pairwise (fun x1 x2 => x1 ≤ x2) (pmap Fin.mk (range n) ⋯)

Tactic:
exact (List.pairwise_le_range n).pmap (by simp) (by simp)

Result:
no goals

Proof state:
n : ℕ
⊢ Pairwise (fun x1 x2 => x1 ≤ x2) (finRange n)

Tactic:
rw [finRange_eq_pmap_range]

Result:
n : ℕ
⊢ Pairwise (fun x1 x2 => x1 ≤ x2) (pmap Fin.mk (range n) ⋯)

Proof state:
n : ℕ
⊢ ∀ ⦃x : ℕ⦄ (hx : x < n) ⦃y : ℕ⦄ (hy : y < n), x ≤ y → ⟨x, hx⟩ ≤ ⟨y, hy⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem acc (f : r ↪r s) (a : α) : Acc s (f a) → Acc r a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
⊢ Acc s (f a) → Acc r a

Tactic:
generalize h : f a = b

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a

Tactic:
induction ac generalizing a with | intro _ H IH => ?_

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a

Tactic:
exact ⟨_, fun a' h => IH (f a') (f.map_rel_iff.2 h) _ rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b x✝ : β
H : ∀ (y : β), s y x✝ → Acc s y
IH : ∀ (y : β), s y x✝ → ∀ (a : α), f a = y → Acc r a
a : α
h : f a = x✝
⊢ Acc r a

Tactic:
subst h

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
b : β
a : α
H : ∀ (y : β), s y (f a) → Acc s y
IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a
⊢ Acc r a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
⊢ Acc s b → Acc r a

Tactic:
intro ac

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ↪r s
a : α
b : β
h : f a = b
ac : Acc s b
⊢ Acc r a
-- Mathlib/Order/WellQuasiOrder.lean
theorem WellQuasiOrdered.prod [IsPreorder α r] (hr : WellQuasiOrdered r) (hs : WellQuasiOrdered s) :
    WellQuasiOrdered fun a b : α × β ↦ r a.1 b.1 ∧ s a.2 b.2

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
m n : ℕ
h : m < n
hf : s ((Prod.snd ∘ f ∘ ⇑g) m) ((Prod.snd ∘ f ∘ ⇑g) n)
⊢ ∃ m n, m < n ∧ (fun a b => r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono h, h₁ _ _ h.le, hf⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
⊢ ∃ m n, m < n ∧ (fun a b => r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
obtain ⟨m, n, h, hf⟩ := hs (Prod.snd ∘ f ∘ g)

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
m n : ℕ
h : m < n
hf : s ((Prod.snd ∘ f ∘ ⇑g) m) ((Prod.snd ∘ f ∘ ⇑g) n)
⊢ ∃ m n, m < n ∧ (fun a b => r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
⊢ WellQuasiOrdered fun a b => r a.1 b.1 ∧ s a.2 b.2

Tactic:
intro f

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
⊢ ∃ m n, m < n ∧ (fun a b => r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
⊢ ∃ m n, m < n ∧ (fun a b => r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)

Result:
case intro
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
⊢ ∃ m n, m < n ∧ (fun a b => r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)