harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma norm_term_le_of_re_le_re (f : ℕ → ℂ) {s s' : ℂ} (h : s.re ≤ s'.re) (n : ℕ) :
    ‖term f s' n‖ ≤ ‖term f s n‖

Proof state:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ (if n = 0 then 0 else ‖f n‖ / ↑n ^ s'.re) ≤ if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Tactic:
split

Result:
case isTrue
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : n = 0
⊢ 0 ≤ 0

case isFalse
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s'.re ≤ ‖f n‖ / ↑n ^ s.re

Proof state:
case isFalse
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s'.re ≤ ‖f n‖ / ↑n ^ s.re

Tactic:
next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn

Result:
no goals

Proof state:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : n = 0
⊢ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
h✝ : n = 0
⊢ 0 ≤ 0

Tactic:
next => rfl

Result:
no goals

Proof state:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ ‖f n‖ / ↑n ^ s'.re ≤ ‖f n‖ / ↑n ^ s.re

Tactic:
gcongr

Result:
case h.hx
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n

Proof state:
case h.hx
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n

Tactic:
exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn

Result:
no goals

Proof state:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ ‖term f s' n‖ ≤ ‖term f s n‖

Tactic:
simp only [norm_term_eq]

Result:
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
⊢ (if n = 0 then 0 else ‖f n‖ / ↑n ^ s'.re) ≤ if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
-- Mathlib/Data/Nat/PartENat.lean
theorem coe_succ_le_iff {n : ℕ} {e : PartENat} : ↑n.succ ≤ e ↔ ↑n < e

Proof state:
n : ℕ
e : PartENat
⊢ ↑n.succ ≤ e ↔ ↑n < e

Tactic:
rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, add_one_le_iff_lt (natCast_ne_top n)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma resLE_id (i : V ≤ V') : resLE (𝟙 X) V' V i = X.homOfLE i

Proof state:
X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ X.homOfLE i ≫ 𝟙 ↑(𝟙 X ⁻¹ᵁ V') = X.homOfLE i

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ resLE (𝟙 X) V' V i = X.homOfLE i

Tactic:
simp only [resLE, morphismRestrict_id]

Result:
X : Scheme
V V' : X.Opens
i : V ≤ V'
⊢ X.homOfLE i ≫ 𝟙 ↑(𝟙 X ⁻¹ᵁ V') = X.homOfLE i
-- Mathlib/Order/Hom/Bounded.lean
theorem cancel_left {g : TopHom β γ} {f₁ f₂ : TopHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => TopHom.ext fun a => hg <| by rw [← TopHom.comp_apply, h, TopHom.comp_apply],
    congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Top α
inst✝¹ : Top β
inst✝ : Top γ
g : TopHom β γ
f₁ f₂ : TopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← TopHom.comp_apply, h, TopHom.comp_apply]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_zero : catalan 0 = 1

Proof state:
⊢ catalan 0 = 1

Tactic:
rw [catalan]

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

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

Tactic:
rw [sub_eq_add_neg]

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

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

Tactic:
exact hf.add hg.neg

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem iUnion_Ico_coe_nat : ⋃ n : ℕ, Ico a n = Ici a \ {∞}

Proof state:
a : ℝ≥0∞
⊢ ⋃ n, Ico a ↑n = Ici a \ {⊤}

Tactic:
simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_C (t : R) :
    reverse (C t) = C t

Proof state:
R : Type u_1
inst✝ : Semiring R
t : R
⊢ (C t).reverse = C t

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/Order/Max.lean
theorem NoTopOrder.to_noMaxOrder (α : Type*) [LinearOrder α] [NoTopOrder α] : NoMaxOrder α :=
  { exists_gt := fun a => by simpa [not_le] using exists_not_le a }

Proof state:
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoTopOrder α
a : α
⊢ ∃ b, a < b

Tactic:
simpa [not_le] using exists_not_le a

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : Filter α) ^ n = ⊤
  | 0 => fun h => (h rfl).elim
  | 1 => fun _ => pow_one _
  | n + 2 => fun _ => by rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]

Proof state:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 2) = ⊤

Tactic:
rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@[reassoc (attr := simp), elementwise (attr := simp)]
lemma isoZeroCocycles_hom_comp_subtype :
    (isoZeroCocycles A).hom ≫ ModuleCat.ofHom A.ρ.invariants.subtype =
      iCocycles A 0 ≫ (zeroCochainsLequiv A).toModuleIso.hom

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (isoZeroCocycles A).hom ≫ ModuleCat.ofHom A.ρ.invariants.subtype =
    iCocycles A 0 ≫ (zeroCochainsLequiv A).toModuleIso.hom

Tactic:
dsimp [isoZeroCocycles]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel
        (dZeroArrowIso A).hom ≫
      ModuleCat.ofHom A.ρ.invariants.subtype =
    iCocycles A 0 ≫ ModuleCat.ofHom ↑(zeroCochainsLequiv A)

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (KernelFork.ofι (HomologicalComplex.iCycles (inhomogeneousCochains A) 0) ⋯).mapOfIsLimit ⋯.fIsKernel
        (dZeroArrowIso A).hom ≫
      ModuleCat.ofHom A.ρ.invariants.subtype =
    iCocycles A 0 ≫ ModuleCat.ofHom ↑(zeroCochainsLequiv A)

Tactic:
apply KernelFork.mapOfIsLimit_ι

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
/-- Given `m, n ≥ 2` and `f m = m ^ s`, `f n = n ^ t` for `s, t > 0`, we have `t ≤ s`. -/
private lemma le_of_eq_pow {s t : ℝ} (hfm : f m = m ^ s) (hfn : f n = n ^ t) : t ≤ s

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ f ↑n ≤ ↑n ^ s

Tactic:
apply le_trans <| le_pow_log hm hn notbdd

Result:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ f ↑m ^ logb ↑m ↑n ≤ ↑n ^ s

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ f ↑m ^ logb ↑m ↑n ≤ ↑n ^ s

Tactic:
rw [hfm, ← rpow_mul (Nat.cast_nonneg m), mul_comm, rpow_mul (Nat.cast_nonneg m),
  rpow_logb (mod_cast zero_lt_of_lt hm) (mod_cast hm.ne') (mod_cast zero_lt_of_lt hn)]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ t ≤ s

Tactic:
rw [← rpow_le_rpow_left_iff (x := n) (mod_cast hn), ← hfn]

Result:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ f ↑n ≤ ↑n ^ s
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
theorem le_or_le_of_mul_le_mul [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

Tactic:
contrapose!

Result:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Mul α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
⊢ a₂ < a₁ ∧ b₂ < b₁ → a₂ * b₂ < a₁ * b₁

Tactic:
exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_rightUnitor {p f pf : C} (η_f : p ⊗ f ≅ pf) :
    p ◁ (ρ_ f) ≪≫ η_f = normalizeIsoComp η_f (ρ_ pf) :=
  Iso.ext (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f pf : C
η_f : p ⊗ f ≅ pf
⊢ (p ◁ ρ_ f ≪≫ η_f).hom = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem MeasurableSet.image_inclusion' {s t : Set α} (h : s ⊆ t) {u : Set s}
    (hs : MeasurableSet (Subtype.val ⁻¹' s : Set t)) (hu : MeasurableSet u) :
    MeasurableSet (inclusion h '' u)

Proof state:
case h.e'_3
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion h '' (Subtype.val ⁻¹' u) = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s

Tactic:
ext ⟨x, hx⟩

Result:
case h.e'_3.h.mk
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ inclusion h '' (Subtype.val ⁻¹' u) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' (Subtype.val ⁻¹' u))

Tactic:
convert (measurable_subtype_coe hu).inter hs

Result:
case h.e'_3
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion h '' (Subtype.val ⁻¹' u) = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s

Proof state:
case h.e'_3.h.mk
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ inclusion h '' (Subtype.val ⁻¹' u) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s

Tactic:
simpa [@and_comm _ (_ = x)] using and_comm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
u : Set ↑s
hs : MeasurableSet (Subtype.val ⁻¹' s)
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' u)

Tactic:
rcases hu with ⟨u, hu, rfl⟩

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' (Subtype.val ⁻¹' u))
-- Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
theorem μ_forget_apply {G H : AddCommGrp.{u}} (p : G) (q : H) :
    Functor.LaxMonoidal.μ (forget AddCommGrp.{u}) G H (p, q) = (p, q)

Proof state:
case fst
G H : AddCommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddCommGrp) G H (p, q)).1 = (p, q).1

Tactic:
exact congrFun (Functor.Monoidal.μ_fst (forget AddCommGrp.{u}) G H) (p, q)

Result:
no goals

Proof state:
G H : AddCommGrp
p : ↑G
q : ↑H
⊢ Functor.LaxMonoidal.μ (forget AddCommGrp) G H (p, q) = (p, q)

Tactic:
apply Prod.ext

Result:
case fst
G H : AddCommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddCommGrp) G H (p, q)).1 = (p, q).1

case snd
G H : AddCommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddCommGrp) G H (p, q)).2 = (p, q).2

Proof state:
case snd
G H : AddCommGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddCommGrp) G H (p, q)).2 = (p, q).2

Tactic:
exact congrFun (Functor.Monoidal.μ_snd (forget AddCommGrp.{u}) G H) (p, q)

Result:
no goals
-- Mathlib/Combinatorics/Additive/SmallTripling.lean
@[to_additive]
private lemma small_pos_pos_neg_mul (hA : #(A ^ 3) ≤ K * #A) : #(A * A * A⁻¹) ≤ K ^ 2 * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)) ≤ K ^ 2 * ↑(#A)

Tactic:
rw [← card_inv]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)⁻¹) ≤ K ^ 2 * ↑(#A)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)⁻¹) ≤ K ^ 2 * ↑(#A)

Tactic:
simpa [mul_assoc] using small_pos_neg_neg_mul (A := A) (K := K) (by simpa)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A ^ 3)) ≤ K * ↑(#A)

Tactic:
simpa

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem le_of_le_of_eq {α} [OrderedSemiring α] {a b : α} (ha : a ≤ 0) (hb : b = 0) : a + b ≤ 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Basic.lean
lemma max_min (S₁ S₂ T : Subpresheaf F) :
    (S₁ ⊔ S₂) ⊓ T = (S₁ ⊓ T) ⊔ (S₂ ⊓ T)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
S₁ S₂ T : Subpresheaf F
⊢ (S₁ ⊔ S₂) ⊓ T = S₁ ⊓ T ⊔ S₂ ⊓ T

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma Continuous.preimage_coborder_subset (hf : Continuous f) (s : Set Y) :
    f ⁻¹' (coborder s) ⊆ coborder (f ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
s : Set Y
⊢ f ⁻¹' coborder s ⊆ coborder (f ⁻¹' s)

Tactic:
rw [coborder, coborder, preimage_compl, preimage_diff, compl_subset_compl]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
s : Set Y
⊢ closure (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure s \ f ⁻¹' s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
s : Set Y
⊢ closure (f ⁻¹' s) \ f ⁻¹' s ⊆ f ⁻¹' closure s \ f ⁻¹' s

Tactic:
apply diff_subset_diff_left

Result:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
s : Set Y
⊢ closure (f ⁻¹' s) ⊆ f ⁻¹' closure s

Proof state:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
s : Set Y
⊢ closure (f ⁻¹' s) ⊆ f ⁻¹' closure s

Tactic:
exact hf.closure_preimage_subset s

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive nsmul_left_comm]
lemma pow_right_comm (a : M) (m n : ℕ) : (a ^ m) ^ n = (a ^ n) ^ m

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
rw [← pow_mul, Nat.mul_comm, pow_mul]

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

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

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_lt_range n).pmap (by simp) (by simp)

Result:
no goals
-- Mathlib/Probability/Integration.lean
theorem lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' (h_meas_f : AEMeasurable f μ)
    (h_meas_g : AEMeasurable g μ) (h_indep_fun : IndepFun f g μ) :
    (∫⁻ ω, (f * g) ω ∂μ) = (∫⁻ ω, f ω ∂μ) * ∫⁻ ω, g ω ∂μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
rw [lintegral_congr_ae h_meas_f.ae_eq_mk, lintegral_congr_ae h_meas_g.ae_eq_mk,
  lintegral_congr_ae fg_ae]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (a : Ω), (AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g) a ∂μ =
    (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (a : Ω), (AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g) a ∂μ =
    (∫⁻ (a : Ω), AEMeasurable.mk f h_meas_f a ∂μ) * ∫⁻ (a : Ω), AEMeasurable.mk g h_meas_g a ∂μ

Tactic:
apply lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun h_meas_f.measurable_mk
    h_meas_g.measurable_mk

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ IndepFun (AEMeasurable.mk f h_meas_f) (AEMeasurable.mk g h_meas_g) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ IndepFun (AEMeasurable.mk f h_meas_f) (AEMeasurable.mk g h_meas_g) μ

Tactic:
exact h_indep_fun.ae_eq h_meas_f.ae_eq_mk h_meas_g.ae_eq_mk

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

Tactic:
have fg_ae : f * g =ᵐ[μ] h_meas_f.mk _ * h_meas_g.mk _ := h_meas_f.ae_eq_mk.mul h_meas_g.ae_eq_mk

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ≥0∞
h_meas_f : AEMeasurable f μ
h_meas_g : AEMeasurable g μ
h_indep_fun : IndepFun f g μ
fg_ae : f * g =ᶠ[ae μ] AEMeasurable.mk f h_meas_f * AEMeasurable.mk g h_meas_g
⊢ ∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
/-- A point in the antidiagonal is determined by its second coordinate.

See also `Finset.antidiagonal_congr`. -/
lemma antidiagonal_congr' (hp : p ∈ antidiagonal n) (hq : q ∈ antidiagonal n) :
    p = q ↔ p.2 = q.2

Proof state:
A : Type u_1
inst✝¹ : AddCancelCommMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p.swap = q.swap ↔ p.2 = q.2

Tactic:
exact antidiagonal_congr (swap_mem_antidiagonal.2 hp) (swap_mem_antidiagonal.2 hq)

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : AddCancelCommMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p = q ↔ p.2 = q.2

Tactic:
rw [← Prod.swap_inj]

Result:
A : Type u_1
inst✝¹ : AddCancelCommMonoid A
inst✝ : HasAntidiagonal A
p q : A × A
n : A
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p.swap = q.swap ↔ p.2 = q.2
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem setIntegral_dirac' {mα : MeasurableSpace α} {f : α → E} (hf : StronglyMeasurable f) (a : α)
    {s : Set α} (hs : MeasurableSet s) [Decidable (a ∈ s)] :
    ∫ x in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ ∫ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac' hs]

Result:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
exact integral_dirac' _ _ hf

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
exact integral_zero_measure _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

case neg
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
lemma map_rightHomologyMap' : F.map (ShortComplex.rightHomologyMap' φ hr₁ hr₂) =
    ShortComplex.rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hr₁.IsPreservedBy F
inst✝ : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)

Tactic:
rw [γ.rightHomologyMap'_eq, (γ.map F).rightHomologyMap'_eq,
  ShortComplex.RightHomologyMapData.map_φH]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem mul_zero : φ * 0 = 0 :=
  ext fun n => by classical simp [coeff_mul]

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ * 0) = (coeff R n) 0

Tactic:
simp [coeff_mul]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (φ * 0) = (coeff R n) 0

Tactic:
classical simp [coeff_mul]

Result:
no goals