harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@[reassoc (attr := simp)]
lemma ι_isoColimit_hom (g : CostructuredArrow L Y) :
    E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom =
      colimit.ι (CostructuredArrow.proj L Y ⋙ F) g

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_5, u_2} D
inst✝¹ : Category.{u_6, u_3} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
inst✝ : HasColimit (CostructuredArrow.proj L Y ⋙ F)
g : CostructuredArrow L Y
⊢ E.hom.app g.left ≫ E.right.map g.hom ≫ h.isoColimit.hom = colimit.ι (CostructuredArrow.proj L Y ⋙ F) g

Tactic:
simpa using h.comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) g

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iInf (f : ι → UpperSet α) : (⨅ i, f i).compl = ⨅ i, (f i).compl :=
  LowerSet.ext <| by simp only [coe_compl, coe_iInf, compl_iUnion, LowerSet.coe_iInf]

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨅ i, f i).compl = ↑(⨅ i, (f i).compl)

Tactic:
simp only [coe_compl, coe_iInf, compl_iUnion, LowerSet.coe_iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem getKeyD_eq_getKeyDₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a fallback : α) :
    getKeyD m a fallback = getKeyDₘ m a fallback

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

Tactic:
simp [getKeyD, getKeyDₘ, getKey?ₘ, List.getKeyD_eq_getKey?, bucket]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardFactors_multiset_prod {s : Multiset ℕ} (h0 : s.prod ≠ 0) :
    Ω s.prod = (Multiset.map Ω s).sum

Proof state:
s : Multiset ℕ
h0 : s.prod ≠ 0
⊢ Ω s.prod = (Multiset.map (⇑Ω) s).sum

Tactic:
induction s using Multiset.induction_on with
| empty => simp
| cons ih => simp_all [cardFactors_mul, not_or]

Result:
no goals

Proof state:
case empty
h0 : Multiset.prod 0 ≠ 0
⊢ Ω (Multiset.prod 0) = (Multiset.map (⇑Ω) 0).sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
ih : ℕ
s✝ : Multiset ℕ
a✝ : s✝.prod ≠ 0 → Ω s✝.prod = (Multiset.map (⇑Ω) s✝).sum
h0 : (ih ::ₘ s✝).prod ≠ 0
⊢ Ω (ih ::ₘ s✝).prod = (Multiset.map (⇑Ω) (ih ::ₘ s✝)).sum

Tactic:
simp_all [cardFactors_mul, not_or]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem dist_lt_iff (C0 : (0 : ℝ) < C) : dist f g < C ↔ ∀ x : α, dist (f x) (g x) < C

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ (∀ (x : α), dist ((mkOfCompact f) x) ((mkOfCompact g) x) < C) ↔ ∀ (x : α), dist (f x) (g x) < C

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ (∀ (x : α), dist ((mkOfCompact f) x) ((mkOfCompact g) x) < C) ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
simp only [mkOfCompact_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive (attr := simp)]
lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
    ∀ {l : List α}, a ∈ l → f a * ((l.erase a).map f).prod = (l.map f).prod
  | b :: l, h => by
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h
    · simp only [map, erase_cons_head, prod_cons]
    · simp only [map, erase_cons_tail (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
        mul_left_comm (f a) (f b)]

Proof state:
case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

Tactic:
simp only [map, erase_cons_head, prod_cons]

Result:
no goals

Proof state:
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h : a ∈ b :: l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h

Result:
case inl
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
l : List α
h : a ∈ a :: l
⊢ f a * (map f ((a :: l).erase a)).prod = (map f (a :: l)).prod

case inr.intro
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Proof state:
case inr.intro
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h✝ : a ∈ b :: l
ne : a ≠ b
h : a ∈ l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
simp only [map, erase_cons_tail (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
  mul_left_comm (f a) (f b)]

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem star_invOf {R : Type*} [Monoid R] [StarMul R] (r : R) [Invertible r]
    [Invertible (star r)] : star (⅟ r) = ⅟ (star r)

Proof state:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r = star 1

Tactic:
rw [← star_mul, mul_invOf_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = star ⅟r * (star r * ⅟(star r))

Tactic:
simp only [mul_invOf_self, mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this✝ : star ⅟r = star ⅟r * (star r * ⅟(star r))
this : star ⅟r * star r = star 1
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)

Tactic:
rw [this, star_one, one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)

Tactic:
have : (star (⅟ r)) * (star r) = star 1 := by rw [← star_mul, mul_invOf_self]

Result:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this✝ : star ⅟r = star ⅟r * (star r * ⅟(star r))
this : star ⅟r * star r = star 1
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)

Proof state:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r = ⅟(star r)

Tactic:
rw [this, ← mul_assoc]

Result:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r * star r * ⅟(star r) = ⅟(star r)

Proof state:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
⊢ star ⅟r = ⅟(star r)

Tactic:
have : star (⅟ r) = star (⅟ r) * ((star r) * ⅟ (star r)) := by
  simp only [mul_invOf_self, mul_one]

Result:
R : Type u_1
inst✝³ : Monoid R
inst✝² : StarMul R
r : R
inst✝¹ : Invertible r
inst✝ : Invertible (star r)
this : star ⅟r = star ⅟r * (star r * ⅟(star r))
⊢ star ⅟r = ⅟(star r)
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem pow_mulRight (a : A) (n : ℕ) : mulRight R a ^ n = mulRight R (a ^ n) :=
  match n with
  | 0 => by rw [pow_zero, pow_zero, mulRight_one, LinearMap.one_eq_id]
  | (n + 1) => by rw [pow_succ, pow_succ', mulRight_mul, LinearMap.mul_eq_comp, pow_mulRight]

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n✝ n : ℕ
⊢ mulRight R a ^ (n + 1) = mulRight R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ', mulRight_mul, LinearMap.mul_eq_comp, pow_mulRight]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
n : ℕ
⊢ mulRight R a ^ 0 = mulRight R (a ^ 0)

Tactic:
rw [pow_zero, pow_zero, mulRight_one, LinearMap.one_eq_id]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_factors_comp_self {W : C} (k : W ⟶ X) : (imageSubobject f).Factors (k ≫ f) :=
  ⟨k ≫ factorThruImage f, by simp⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
⊢ (k ≫ factorThruImage f) ≫ (MonoOver.mk' (image.ι f)).arrow = k ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
simp [← braiding_rightUnitor]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
lemma eventually_prod_self_iff {r : α → α → Prop} :
    (∀ᶠ x in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y :=
  mem_prod_self_iff.trans <| by simp only [prod_subset_iff, mem_setOf_eq]

Proof state:
α : Type u_1
la : Filter α
r : α → α → Prop
⊢ (∃ t ∈ la, t ×ˢ t ⊆ {x | (fun x => r x.1 x.2) x}) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y

Tactic:
simp only [prod_subset_iff, mem_setOf_eq]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
theorem commProb_prod (M' : Type*) [Mul M'] : commProb (M × M') = commProb M * commProb M'

Proof state:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ commProb (M × M') = commProb M * commProb M'

Tactic:
simp_rw [commProb_def, div_mul_div_comm, Nat.card_prod, Nat.cast_mul, mul_pow, ← Nat.cast_mul,
  ← Nat.card_prod, Commute, SemiconjBy, Prod.ext_iff]

Result:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Proof state:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ ↑(Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 }) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2) =
    ↑(Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })) /
      (↑(Nat.card M) ^ 2 * ↑(Nat.card M') ^ 2)

Tactic:
congr 2

Result:
case e_a.e_a
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } =
    Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })

Proof state:
case e_a.e_a
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ Nat.card { p // (p.1 * p.2).1 = (p.2 * p.1).1 ∧ (p.1 * p.2).2 = (p.2 * p.1).2 } =
    Nat.card ({ p // p.1 * p.2 = p.2 * p.1 } × { p // p.1 * p.2 = p.2 * p.1 })

Tactic:
exact Nat.card_congr ⟨fun x => ⟨⟨⟨x.1.1.1, x.1.2.1⟩, x.2.1⟩, ⟨⟨x.1.1.2, x.1.2.2⟩, x.2.2⟩⟩,
  fun x => ⟨⟨⟨x.1.1.1, x.2.1.1⟩, ⟨x.1.1.2, x.2.1.2⟩⟩, ⟨x.1.2, x.2.2⟩⟩, fun x => rfl, fun x => rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Whiskering.lean
theorem triangle (F : A ⥤ B) (G : B ⥤ C) :
    (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom =
      whiskerRight (rightUnitor F).hom G

Proof state:
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : A ⥤ B
G : B ⥤ C
⊢ (F.associator (𝟭 B) G).hom ≫ whiskerLeft F G.leftUnitor.hom = whiskerRight F.rightUnitor.hom G

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_pos : 0 < √x ↔ 0 < x :=
  lt_iff_lt_of_le_iff_le (Iff.trans (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')

Proof state:
x : ℝ
⊢ √x ≤ 0 ↔ √x = 0

Tactic:
simp [le_antisymm_iff, sqrt_nonneg]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem doubleton_eq [DecidableEq α] {x y : α} (h : x ≠ y) : ({x, y} : List α) = [x, y]

Proof state:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ {x, y} = [x, y]

Tactic:
rw [insert_neg, singleton_eq]

Result:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}

Proof state:
α : Type u
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ ¬x ∈ {y}

Tactic:
rwa [singleton_eq, mem_singleton]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem IsOpen.mem_nhdsSet (hU : IsOpen s) : s ∈ 𝓝ˢ t ↔ t ⊆ s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hU : IsOpen s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem forall_mem_target {p : β → Prop} : (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (e x)

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (↑e x)

Tactic:
rw [← image_source_eq_target, forall_mem_image]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem const_smul {𝕜} [TopologicalSpace 𝕜] [AddMonoid β] [Monoid 𝕜]
    [DistribMulAction 𝕜 β] [ContinuousSMul 𝕜 β] (hf : FinStronglyMeasurable f μ) (c : 𝕜) :
    FinStronglyMeasurable (c • f) μ

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_5
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support ⇑((fun n => c • hf.approx n) n)) < ⊤

Tactic:
rw [SimpleFunc.coe_smul]

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_5
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support (c • ⇑(hf.approx n))) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_5
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support (c • ⇑(hf.approx n))) < ⊤

Tactic:
exact (measure_mono (support_const_smul_subset c _)).trans_lt (hf.fin_support_approx n)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_5
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ

Tactic:
refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝⁵ : TopologicalSpace β
𝕜 : Type u_5
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : AddMonoid β
inst✝² : Monoid 𝕜
inst✝¹ : DistribMulAction 𝕜 β
inst✝ : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ μ (support ⇑((fun n => c • hf.approx n) n)) < ⊤
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem iteratedFDeriv_neg_apply {i : ℕ} {f : E → F} :
    iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
⊢ iteratedFDerivWithin 𝕜 i (-f) univ x = -iteratedFDerivWithin 𝕜 i f univ x

Tactic:
exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
i : ℕ
f : E → F
⊢ iteratedFDerivWithin 𝕜 i (-f) univ x = -iteratedFDerivWithin 𝕜 i f univ x
-- Mathlib/RingTheory/Polynomial/Tower.lean
theorem aeval_map_algebraMap (x : B) (p : R[X]) : aeval x (map (algebraMap R A) p) = aeval x p

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
p : R[X]
⊢ (aeval x) (map (algebraMap R A) p) = (aeval x) p

Tactic:
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem adjoin_eq_top_of_gen_mem_adjoin {B : PowerBasis R S} {x : S}
    (hx : B.gen ∈ adjoin R ({x} : Set S)) : adjoin R ({x} : Set S) = ⊤

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {x} = ⊤

Tactic:
rw [_root_.eq_top_iff, ← B.adjoin_gen_eq_top]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {B.gen} ≤ adjoin R {x}

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ adjoin R {B.gen} ≤ adjoin R {x}

Tactic:
refine adjoin_le ?_

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ {B.gen} ⊆ ↑(adjoin R {x})

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
B : PowerBasis R S
x : S
hx : B.gen ∈ adjoin R {x}
⊢ {B.gen} ⊆ ↑(adjoin R {x})

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem Basis.mk_eq_rank (v : Basis ι R M) :
    Cardinal.lift.{v} #ι = Cardinal.lift.{w} (Module.rank R M)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : StrongRankCondition R
v : Basis ι R M
this : Nontrivial R
⊢ Cardinal.lift.{v, w} #ι = Cardinal.lift.{w, v} (Module.rank R M)

Tactic:
rw [← v.mk_range_eq_rank, Cardinal.mk_range_eq_of_injective v.injective]

Result:
no goals
-- Mathlib/Data/Subtype.lean
theorem restrict_apply {α} {β : α → Type*} (f : ∀ x, β x) (p : α → Prop) (x : Subtype p) :
    restrict p f x = f x.1

Proof state:
α : Sort u_5
β : α → Type u_4
f : (x : α) → β x
p : α → Prop
x : Subtype p
⊢ restrict p f x = f ↑x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.closedCell_subset_complex [RelCWComplex C D] (n : ℕ) (j : cell C n) :
    closedCell n j ⊆ C :=
  (closedCell_subset_skeleton n j).trans
    (by simp_rw [← skeleton_top (C := C) (D := D)]; exact skeleton_mono le_top)

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ skeleton C ↑n ⊆ C

Tactic:
simp_rw [← skeleton_top (C := C) (D := D)]

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ skeleton C ↑n ⊆ skeleton C ⊤

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
⊢ skeleton C ↑n ⊆ skeleton C ⊤

Tactic:
exact skeleton_mono le_top

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_ι_mul (a : M) (b : CliffordAlgebra Q) :
    d⌋(ι Q a * b) = d a • b - ι Q a * (d⌋b)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx

Tactic:
exact fun m x fx ↦ contractLeftAux_contractLeftAux Q d m x fx

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ (contractLeft d) ((ι Q) a * b) = d a • b - (ι Q) a * (contractLeft d) b

Tactic:
refine foldr'_ι_mul _ _ ?_ _ _ _

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
a : M
b : CliffordAlgebra Q
⊢ ∀ (m : M) (x fx : CliffordAlgebra Q),
    ((contractLeftAux Q d) m) ((ι Q) m * x, ((contractLeftAux Q d) m) (x, fx)) = Q m • fx
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaarMeasure_eq_volume : addHaarMeasure Icc01 = volume

Proof state:
⊢ addHaarMeasure Icc01 = volume

Tactic:
convert (addHaarMeasure_unique volume Icc01).symm

Result:
case h.e'_2

⊢ addHaarMeasure Icc01 = volume ↑Icc01 • addHaarMeasure Icc01

Proof state:
case h.e'_2

⊢ addHaarMeasure Icc01 = volume ↑Icc01 • addHaarMeasure Icc01

Tactic:
simp [Icc01]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma sUnion_union_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) [DecidableEq (Set α)] :
    ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
inst✝ : DecidableEq (Set α)
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = s

Tactic:
conv_rhs => rw [← sUnion_union_sUnion_disjointOfDiffUnion_of_subset hC hs hI hI_ss]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
inst✝ : DecidableEq (Set α)
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
inst✝ : DecidableEq (Set α)
⊢ ⋃₀ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
rw [sUnion_union]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
inst✝ : DecidableEq (Set α)
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)

Tactic:
simp_rw [coe_union]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
inst✝ : DecidableEq (Set α)
⊢ ⋃₀ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
-- Mathlib/RingTheory/Localization/InvSubmonoid.lean
theorem mem_invSubmonoid_iff_exists_mk' (x : S) :
    x ∈ invSubmonoid M S ↔ ∃ m : M, mk' S 1 m = x

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, ↑((toInvSubmonoid M S) m) = x

Tactic:
exact ⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩,
  fun h => h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, mk' S 1 m = x

Tactic:
simp_rw [← toInvSubmonoid_eq_mk']

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, ↑((toInvSubmonoid M S) m) = x