harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Ici (a : ℕ) : (↑) '' Ici a = Ici (a : ℤ) :=
  (castOrderEmbedding (α := ℤ)).image_Ici (by simp [isUpperSet_Ici]) a

Proof state:
a : ℕ
⊢ IsUpperSet (range ⇑castOrderEmbedding)

Tactic:
simp [isUpperSet_Ici]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_reverse' {l : Vector α n} (i j) (h : i + j + 1 = n) : l.reverse[i]? = l[j]?

Proof state:
case mk
α : Type u_1
i j : Nat
l : Array α
h : i + j + 1 = l.size
⊢ { toArray := l, size_toArray := ⋯ }.reverse[i]? = { toArray := l, size_toArray := ⋯ }[j]?

Tactic:
simpa using Array.getElem?_reverse' i j h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i j : Nat
h : i + j + 1 = n
⊢ l.reverse[i]? = l[j]?

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i j : Nat
l : Array α
h : i + j + 1 = l.size
⊢ { toArray := l, size_toArray := ⋯ }.reverse[i]? = { toArray := l, size_toArray := ⋯ }[j]?
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getKey?_eq [BEq α] {l : AssocList α β} {a : α} :
    l.getKey? a = List.getKey? a l.toList

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : AssocList α β
a : α
⊢ getKey? a l = List.getKey? a l.toList

Tactic:
induction l <;> simp_all [getKey?]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
@[simp] lemma sublist_singleton {l : List α} {a : α} : l <+ [a] ↔ l = [] ∨ l = [a]

Proof state:
α : Type u
l : List α
a : α
⊢ l <+ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor <;> rintro (_ | _) <;> aesop

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem inf_eq_left {a b : CauSeq α abs} (h : a ≤ b) : a ⊓ b ≈ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b : CauSeq α abs
h : a ≤ b
⊢ a ⊓ b ≈ a

Tactic:
simpa only [CauSeq.inf_comm] using CauSeq.inf_eq_right h

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] lemma IsLowerSet.disjoint_upperClosure_right (hs : IsLowerSet s) :
    Disjoint s (upperClosure t) ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : IsLowerSet s
⊢ Disjoint s ↑(upperClosure t) ↔ Disjoint s t

Tactic:
simpa only [disjoint_comm] using hs.disjoint_upperClosure_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem not_congr (x x' : Bool) (h : x' = x) : (!x') = (!x)

Proof state:
x x' : Bool
h : x' = x
⊢ (!x') = !x

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsLT {a : H} : Tendsto Inv.inv (𝓝[<] a) (𝓝[>] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Iio a)) (𝓟 (Ioi a⁻¹))

Tactic:
simp [tendsto_principal_principal]

Result:
no goals
-- Mathlib/Order/Lattice.lean
@[simp] lemma inf_lt_sup : a ⊓ b < a ⊔ b ↔ a ≠ b

Proof state:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b

Tactic:
rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n

Proof state:
n : ℤ
⊢ Squarefree n.natAbs ↔ Squarefree n

Tactic:
simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
  isUnit_iff_natAbs_eq, Nat.isUnit_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem inv_rpow (hx : 0 ≤ x) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ x⁻¹ ^ y = (x ^ y)⁻¹

Tactic:
simp only [← rpow_neg_one, ← rpow_mul hx, mul_comm]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.node4L_lemma₃ {b c d : ℕ} (mr₁ : 2 * d ≤ b + c + 1) (mm₁ : b ≤ 3 * c) :
    d ≤ 3 * c

Proof state:
b c d : ℕ
mr₁ : 2 * d ≤ b + c + 1
mm₁ : b ≤ 3 * c
⊢ d ≤ 3 * c

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem log_pos_iff {b n : ℕ} : 0 < log b n ↔ b ≤ n ∧ 1 < b

Proof state:
b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem mul_conj (z : ℂ) : z * conj z = normSq z :=
  Complex.ext_iff.2 <| by simp [normSq, mul_comm, sub_eq_neg_add, add_comm, ofReal]

Proof state:
z : ℂ
⊢ (z * (starRingEnd ℂ) z).re = (↑(normSq z)).re ∧ (z * (starRingEnd ℂ) z).im = (↑(normSq z)).im

Tactic:
simp [normSq, mul_comm, sub_eq_neg_add, add_comm, ofReal]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Ioc : (fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Ioc b c = Ioc (b + a) (c + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_compContinuousLinearMap_le (g : ContinuousMultilinearMap 𝕜 E₁ G)
    (f : ∀ i, E i →L[𝕜] E₁ i) : ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖ :=
  opNorm_le_bound (by positivity) fun m =>
    calc
      ‖g fun i => f i (m i)‖ ≤ ‖g‖ * ∏ i, ‖f i (m i)‖ := g.le_opNorm _
      _ ≤ ‖g‖ * ∏ i, ‖f i‖ * ‖m i‖ :=
        (mul_le_mul_of_nonneg_left
          (prod_le_prod (fun _ _ => norm_nonneg _) fun i _ => (f i).le_opNorm (m i))
          (norm_nonneg g))
      _ = (‖g‖ * ∏ i, ‖f i‖) * ∏ i, ‖m i‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
m : (i : ι) → E i
⊢ ‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖ = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖

Tactic:
rw [prod_mul_distrib, mul_assoc]

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ 0 ≤ ‖g‖ * ∏ i : ι, ‖f i‖

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConvexOn.neg (hf : UniformConvexOn s φ f) : UniformConcaveOn s φ (-f)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
⊢ UniformConcaveOn s φ (-f)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)

Tactic:
simpa [add_comm, -neg_le_neg_iff, le_sub_iff_add_le'] using hf.2 hx hy ha hb hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKeyD_val [BEq α] [Hashable α] {m : Raw₀ α β} {a fallback : α} :
    m.val.getKeyD a fallback = m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a fallback : α
⊢ m.val.getKeyD a fallback = m.getKeyD a fallback

Tactic:
simp [Raw.getKeyD, m.2]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasFDerivAtFilter.sub (hf : HasFDerivAtFilter f f' x L) (hg : HasFDerivAtFilter g g' x L) :
    HasFDerivAtFilter (fun x => f x - g x) (f' - g') x L

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
L : Filter E
hf : HasFDerivAtFilter f f' x L
hg : HasFDerivAtFilter g g' x L
⊢ HasFDerivAtFilter (fun x => f x - g x) (f' - g') x L

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_of_re_neg_of_im_nonneg {x : ℂ} (hx_re : x.re < 0) (hx_im : 0 ≤ x.im) :
    arg x = Real.arcsin ((-x).im / ‖x‖) + π

Proof state:
x : ℂ
hx_re : x.re < 0
hx_im : 0 ≤ x.im
⊢ x.arg = Real.arcsin ((-x).im / ‖x‖) + π

Tactic:
simp only [arg, hx_re.not_le, hx_im, if_true, if_false]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toPMF_toMeasure : μ.toPMF.toMeasure = μ :=
  Measure.ext fun s hs => by
    rw [μ.toPMF.toMeasure_apply s hs, ← μ.tsum_indicator_apply_singleton s hs]
    rfl

Proof state:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (⇑μ.toPMF) x = ∑' (x : α), s.indicator (fun x => μ {x}) x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ μ.toPMF.toMeasure s = μ s

Tactic:
rw [μ.toPMF.toMeasure_apply s hs, ← μ.tsum_indicator_apply_singleton s hs]

Result:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
s : Set α
hs : MeasurableSet s
⊢ ∑' (x : α), s.indicator (⇑μ.toPMF) x = ∑' (x : α), s.indicator (fun x => μ {x}) x
-- Mathlib/Order/Monotone/Basic.lean
theorem antitone_dual_iff : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Antitone f

Tactic:
rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_const {C : E} : IntegrableOn (fun _ => C) s μ ↔ C = 0 ∨ μ s < ∞ :=
  integrable_const_iff.trans <| by rw [isFiniteMeasure_restrict, lt_top_iff_ne_top]

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
s : Set α
μ : Measure α
C : E
⊢ C = 0 ∨ IsFiniteMeasure (μ.restrict s) ↔ C = 0 ∨ μ s < ⊤

Tactic:
rw [isFiniteMeasure_restrict, lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem piEquivOfFintype_apply (x : AdicCompletion I (∀ j, M j)) :
    piEquivOfFintype I M x = pi I M x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : AdicCompletion I ((j : ι) → M j)
⊢ (piEquivOfFintype I M) x = (pi I M) x

Tactic:
simp [piEquivOfFintype, sumInv, map_comp_apply]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_union [DecidableEq α] (hs : s.Finite) (ht : t.Finite)
    (h : (s ∪ t).Finite) : h.toFinset = hs.toFinset ∪ ht.toFinset

Proof state:
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
⊢ h.toFinset = hs.toFinset ∪ ht.toFinset

Tactic:
ext

Result:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∪ ht.toFinset

Proof state:
case h
α : Type u
s t : Set α
inst✝ : DecidableEq α
hs : s.Finite
ht : t.Finite
h : (s ∪ t).Finite
a✝ : α
⊢ a✝ ∈ h.toFinset ↔ a✝ ∈ hs.toFinset ∪ ht.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_sub (n₁ n₂ : ℤ) :
    (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Proof state:
n₁ n₂ : ℤ
⊢ (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow

Tactic:
simp only [sub_eq_add_neg, negOnePow_add, negOnePow_neg]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_biUnion (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset β) :
    interedges r (s.biUnion f) (t.biUnion g) =
      (s ×ˢ t).biUnion fun ab ↦ interedges r (f ab.1) (g ab.2)

Proof state:
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
⊢ interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => interedges r (f ab.1) (g ab.2)

Tactic:
simp_rw [product_biUnion, interedges_biUnion_left, interedges_biUnion_right]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma image_pow [MonoidHomClass F α β] (f : F) (s : Set α) : ∀ n, f '' (s ^ n) = (f '' s) ^ n
  | 0 => by simp [singleton_one]
  | n + 1 => image_pow_of_ne_zero n.succ_ne_zero ..

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
s : Set α
⊢ ⇑f '' (s ^ 0) = (⇑f '' s) ^ 0

Tactic:
simp [singleton_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem edist_lt_ofReal {x y : α} {r : ℝ} : edist x y < ENNReal.ofReal r ↔ dist x y < r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r

Tactic:
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_Icc_of_le (h : a ≤ b + 1) : (#(Icc a b) : ℤ) = b + 1 - a

Proof state:
a b : ℤ
h : a ≤ b + 1
⊢ ↑(#(Icc a b)) = b + 1 - a

Tactic:
rw [card_Icc, toNat_sub_of_le h]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem toCotangent_eq {x y : I} : I.toCotangent x = I.toCotangent y ↔ (x - y : R) ∈ I ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x y : ↥I
⊢ I.toCotangent x - I.toCotangent y = 0 ↔ ↑x - ↑y ∈ I ^ 2

Tactic:
exact I.mem_toCotangent_ker

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x y : ↥I
⊢ I.toCotangent x = I.toCotangent y ↔ ↑x - ↑y ∈ I ^ 2

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
x y : ↥I
⊢ I.toCotangent x - I.toCotangent y = 0 ↔ ↑x - ↑y ∈ I ^ 2
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_ne_bot : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Proof state:
α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc]
lemma counitIso_inv_app_comp_functor_map_η_inverse :
    e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = ε e.functor

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
e : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = ε e.functor

Tactic:
rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
  Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem mk_natCast (m : ℕ) : (mk m 1 : Localization M) = m

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
m : ℕ
⊢ mk (↑m) 1 = ↑m

Tactic:
simpa using mk_algebraMap (R := R) (A := ℕ) _

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem cancel_iso_hom_right {X Y Z : C} (f f' : X ⟶ Y) (g : Y ≅ Z) :
    f ≫ g.hom = f' ≫ g.hom ↔ f = f'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f f' : X ⟶ Y
g : Y ≅ Z
⊢ f ≫ g.hom = f' ≫ g.hom ↔ f = f'

Tactic:
simp only [cancel_mono]

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem sign_of_pos {r : ℝ} (hr : 0 < r) : sign r = 1

Proof state:
r : ℝ
hr : 0 < r
⊢ r.sign = 1

Tactic:
rw [sign, if_pos hr, if_neg hr.not_lt]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem eval₂_restriction {p : R[X]} :
    eval₂ f x p =
      eval₂ (f.comp (Subring.subtype (Subring.closure (p.coeffs : Set R)))) x p.restriction

Proof state:
R : Type u
S : Type u_1
inst✝¹ : Ring R
inst✝ : Semiring S
f : R →+* S
x : S
p : R[X]
⊢ eval₂ f x p = eval₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction

Tactic:
simp only [eval₂_eq_sum, sum, support_restriction, ← @coeff_restriction _ _ p, RingHom.comp_apply,
  Subring.coe_subtype]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_map_map_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
    {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} :
    map m₁ f₁ ×ˢ map m₂ f₂ = map (fun p : α₁ × α₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂) :=
  le_antisymm
    (fun s hs =>
      let ⟨s₁, hs₁, s₂, hs₂, h⟩ := mem_prod_iff.mp hs
      mem_of_superset (prod_mem_prod (image_mem_map hs₁) (image_mem_map hs₂)) <|
        by rwa [prod_image_image_eq, image_subset_iff])
    ((tendsto_map.comp tendsto_fst).prod_mk (tendsto_map.comp tendsto_snd))

Proof state:
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p => (m₁ p.1, m₂ p.2)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p => (m₁ p.1, m₂ p.2)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s

Tactic:
rwa [prod_image_image_eq, image_subset_iff]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma compls_infs_eq_diffs (s t : Finset α) : sᶜˢ ⊼ t = t \\ s

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ sᶜˢ ⊼ t = t \\ s

Tactic:
rw [infs_comm, infs_compls_eq_diffs]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Mat.lean
theorem id_apply_of_ne (M : Mat R) (i j : M) (h : i ≠ j) : (𝟙 M : Matrix M M R) i j = 0

Proof state:
R : Type u
inst✝ : Semiring R
M : Mat R
i j : M.carrier
h : i ≠ j
⊢ 𝟙 M i j = 0

Tactic:
simp [id_apply, h]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_zero : basicOpen (0 : R) = ⊥ :=
  TopologicalSpace.Opens.ext <| by simp

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ ↑(basicOpen 0) = ↑⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma div_zero_subset (s : Finset α) : s / 0 ⊆ 0

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ s / 0 ⊆ 0

Tactic:
simp [subset_iff, mem_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/OfFn.lean
theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).toList = #[].toList ↔ n = 0

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ ofFn f = #[] ↔ n = 0

Tactic:
rw [← Array.toList_inj]

Result:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).toList = #[].toList ↔ n = 0
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem equalizerSubobject_arrow' :
    (equalizerSubobjectIso f g).inv ≫ (equalizerSubobject f g).arrow = equalizer.ι f g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).inv ≫ (equalizerSubobject f g).arrow = equalizer.ι f g

Tactic:
simp [equalizerSubobjectIso]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_eq_principal_iff : 𝓝ˢ s = 𝓟 s ↔ IsOpen s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen s

Tactic:
rw [← principal_le_nhdsSet.le_iff_eq, le_principal_iff, mem_nhdsSet_iff_forall,
  isOpen_iff_mem_nhds]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem sndPiMap_π (b) : I.sndPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.snd b

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b : J.R
⊢ I.sndPiMap ≫ Pi.π I.right b = Pi.π I.left (J.snd b) ≫ I.snd b

Tactic:
simp [sndPiMap]

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma isColimitLocallyConstantPresheaf_desc_apply (hc : IsLimit c) [∀ i, Epi (c.π.app i)]
    (s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X))
    (n : ℕᵒᵖ) (f : LocallyConstant (toLightProfinite.obj (F.obj n)) X) :
    (isColimitLocallyConstantPresheaf c X hc).desc s (f.comap (c.π.app n).hom) = s.ι.app ⟨n⟩ f

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop) X
⊢ (isColimitLocallyConstantPresheaf c X hc).desc s (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n)) f) =
    s.ι.app (Opposite.op n) f

Tactic:
change ((((locallyConstantPresheaf X).mapCocone c.op).ι.app ⟨n⟩) ≫
  (isColimitLocallyConstantPresheaf c X hc).desc s) _ = _

Result:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop) X
⊢ (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op n) ≫
        (isColimitLocallyConstantPresheaf c X hc).desc s)
      f =
    s.ι.app (Opposite.op n) f

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
s : Cocone ((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X)
n : ℕᵒᵖ
f : LocallyConstant (↑(toLightProfinite.obj (F.obj n)).toTop) X
⊢ (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op n) ≫
        (isColimitLocallyConstantPresheaf c X hc).desc s)
      f =
    s.ι.app (Opposite.op n) f

Tactic:
rw [(isColimitLocallyConstantPresheaf c X hc).fac]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_inv_natCast_pow {n : ℕ} (hn : n ≠ 0) (x : ℝ≥0∞) : (x ^ (n⁻¹ : ℝ)) ^ n = x

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
rw [← rpow_natCast, ← rpow_mul, inv_mul_cancel₀ (by positivity), rpow_one]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
x : ℝ≥0∞
⊢ ↑n ≠ 0

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem ne_zero_iff_exists_coeff_ne_zero_and_degree :
    f ≠ 0 ↔ (∃ n : ℕ, ∃ d : σ →₀ ℕ, coeff R d f ≠ 0 ∧ degree d = n)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff R d) f ≠ 0 ∧ d.degree = n

Tactic:
simp_rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff R d) f ≠ 0 ∧ (weight fun x => 1) d = n

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ n d, (coeff R d) f ≠ 0 ∧ (weight fun x => 1) d = n

Tactic:
exact ne_zero_iff_exists_coeff_ne_zero_and_weight (fun _ => 1)

Result:
no goals
-- Mathlib/Control/Bifunctor.lean
theorem snd_fst {α₀ α₁ β₀ β₁} (f : α₀ → α₁) (f' : β₀ → β₁) (x : F α₀ β₀) :
    snd f' (fst f x) = bimap f f' x

Proof state:
F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α₀ α₁ : Type u₀
β₀ β₁ : Type u₁
f : α₀ → α₁
f' : β₀ → β₁
x : F α₀ β₀
⊢ snd f' (fst f x) = bimap f f' x

Tactic:
simp [snd, bimap_bimap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ => pure ⟨⟩) = x

Proof state:
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m PUnit
⊢ (do
      x
      pure PUnit.unit) =
    x

Tactic:
rw [bind_pure]

Result:
no goals