harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_seven [CommMonoid β] (f : Fin 7 → β) :
    ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 7 → β
⊢ ∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
rw [prod_univ_castSucc, prod_univ_six]

Result:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 7 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (last 6) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 7 → β
⊢ f (castSucc 0) * f (castSucc 1) * f (castSucc 2) * f (castSucc 3) * f (castSucc 4) * f (castSucc 5) * f (last 6) =
    f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitFlipCompLimIsoLimitCompLim_hom_π_π (j) (k) :
    (limitFlipCompLimIsoLimitCompLim F).hom ≫ limit.π _ j ≫ limit.π _ k =
      (limit.π _ k ≫ limit.π _ j : limit (_ ⋙ lim) ⟶ _)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_6, u_1} J
inst✝³ : Category.{u_5, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
j : J
k : K
⊢ ((limitUncurryIsoLimitCompLim F.flip).inv ≫
        (HasLimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫
            (limitUncurryIsoLimitCompLim F).hom) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j

Tactic:
simp [Equivalence.counit]

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_6, u_1} J
inst✝³ : Category.{u_5, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
j : J
k : K
⊢ (limitFlipCompLimIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j

Tactic:
dsimp [limitFlipCompLimIsoLimitCompLim]

Result:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_6, u_1} J
inst✝³ : Category.{u_5, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
j : J
k : K
⊢ ((limitUncurryIsoLimitCompLim F.flip).inv ≫
        (HasLimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents (fun x => Iso.refl ((F.obj x.2).obj x.1)) ⋯)).hom ≫
            (limitUncurryIsoLimitCompLim F).hom) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (F.flip ⋙ lim) k ≫ limit.π (F.flip.obj k) j
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_iUnion (s : ι → Set (Set α)) : ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i

Proof state:
α : Type u_1
ι : Sort u_5
s : ι → Set (Set α)
⊢ ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i

Tactic:
simp only [sInter_eq_biInter, biInter_iUnion]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_subset_Ioc_iff (h₁ : a₁ < b₁) : Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁

Tactic:
convert @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2 <;> exact (@dual_Ico α _ _ _).symm

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Int.lean
theorem ofAdd_zpow (a : ℤ) : (↑(ofAdd a) : ℤₘ₀) = ofAdd (1 : ℤ) ^ a

Proof state:
a : ℤ
⊢ ↑(ofAdd a) = ↑(ofAdd 1) ^ a

Tactic:
rw [← WithZero.coe_zpow, WithZero.coe_inj, ← Int.ofAdd_mul, one_mul]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.le_iff (hl : l.HasBasis p s) : l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t

Proof state:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t

Tactic:
simp only [le_def, hl.mem_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_diff_Ioo_self (h : a < b) : Ioc a b \ Ioo a b = {b}

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}

Tactic:
simp [← coe_inj, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_eq_nil_iff {l : List α} {f : α → List β} : l.flatMap f = [] ↔ ∀ x ∈ l, f x = [] :=
  flatten_eq_nil_iff.trans <| by
    simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ (∀ (l_1 : List β), l_1 ∈ map f l → l_1 = []) ↔ ∀ (x : α), x ∈ l → f x = []

Tactic:
simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_left (e : f ≅ g) : e.inv.left ≫ e.hom.left = 𝟙 _

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ e.inv.left ≫ e.hom.left = 𝟙 g.left

Tactic:
rw [← comp_left, e.inv_hom_id, id_left]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem mono_of_mono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono (f ≫ g)] : Mono f :=
  ⟨fun _ _ w => (cancel_mono (f ≫ g)).1 <| by simp only [← Category.assoc, w]⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono (f ≫ g)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
w : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ ≫ f ≫ g = x✝ ≫ f ≫ g

Tactic:
simp only [← Category.assoc, w]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_eq {x : ℝ} : ‖(x : UnitAddCircle)‖ = |x - round x|

Proof state:
x : ℝ
⊢ ‖↑x‖ = |x - ↑(round x)|

Tactic:
simp [AddCircle.norm_eq]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_sdiff_add_dens_eq_dens (h : s ⊆ t) : dens (t \ s) + dens s = dens t

Proof state:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : s ⊆ t
⊢ (t \ s).dens + s.dens = t.dens

Tactic:
simp [dens, ← card_sdiff_add_card_eq_card h, add_div]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bit_negSucc (b) (n : ℕ) : bit b -[n+1] = -[Nat.bit (not b) n+1]

Proof state:
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]

Tactic:
cases b <;> rfl

Result:
no goals

Proof state:
b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]

Tactic:
rw [bit_val, Nat.bit_val]

Result:
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + (!b).toNat+1]
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_smul_span_singleton {I : Ideal R} {m : M} {x : M} :
    x ∈ I • span R ({m} : Set M) ↔ ∃ y ∈ I, y • m = x :=
  ⟨fun hx =>
    smul_induction_on hx
      (fun r hri _ hnm =>
        let ⟨s, hs⟩ := mem_span_singleton.1 hnm
        ⟨r * s, I.mul_mem_right _ hri, hs ▸ mul_smul r s m⟩)
      fun m1 m2 ⟨y1, hyi1, hy1⟩ ⟨y2, hyi2, hy2⟩ =>
      ⟨y1 + y2, I.add_mem hyi1 hyi2, by rw [add_smul, hy1, hy2]⟩,
    fun ⟨_, hyi, hy⟩ => hy ▸ smul_mem_smul hyi (subset_span <| Set.mem_singleton m)⟩

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
m x : M
hx : x ∈ I • span R {m}
m1 m2 : M
x✝¹ : ∃ y ∈ I, y • m = m1
x✝ : ∃ y ∈ I, y • m = m2
y1 : R
hyi1 : y1 ∈ I
hy1 : y1 • m = m1
y2 : R
hyi2 : y2 ∈ I
hy2 : y2 • m = m2
⊢ (y1 + y2) • m = m1 + m2

Tactic:
rw [add_smul, hy1, hy2]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_add_sin : sin x + sin y = 2 * sin ((x + y) / 2) * cos ((x - y) / 2)

Proof state:
x y : ℂ
⊢ sin x + sin y = 2 * sin ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
simpa using sin_sub_sin x (-y)

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Convex.sum_mem (hs : Convex R s) (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1)
    (hz : ∀ i ∈ t, z i ∈ s) : (∑ i ∈ t, w i • z i) ∈ s

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
t : Finset ι
w : ι → R
z : ι → E
hs : Convex R s
h₀ : ∀ i ∈ t, 0 ≤ w i
h₁ : ∑ i ∈ t, w i = 1
hz : ∀ i ∈ t, z i ∈ s
⊢ ∑ i ∈ t, w i • z i ∈ s

Tactic:
simpa only [h₁, centerMass, inv_one, one_smul] using
  hs.centerMass_mem h₀ (h₁.symm ▸ zero_lt_one) hz

Result:
no goals
-- Mathlib/CategoryTheory/Limits/ColimitLimit.lean
theorem ι_colimitLimitToLimitColimit_π (j) (k) :
    colimit.ι _ k ≫ colimitLimitToLimitColimit F ≫ limit.π _ j =
      limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Proof state:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      limit.lift (curry.obj F ⋙ colim)
          { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              {
                app := fun j =>
                  colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                    { pt := colimit ((curry.obj F).obj j),
                      ι :=
                        {
                          app := fun k =>
                            limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                          naturality := ⋯ } },
                naturality := ⋯ } } ≫
        limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫ colimitLimitToLimitColimit F ≫ limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Tactic:
dsimp [colimitLimitToLimitColimit]

Result:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k ≫
      limit.lift (curry.obj F ⋙ colim)
          { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              {
                app := fun j =>
                  colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                    { pt := colimit ((curry.obj F).obj j),
                      ι :=
                        {
                          app := fun k =>
                            limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                          naturality := ⋯ } },
                naturality := ⋯ } } ≫
        limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem exists_orderOf_eq_prime_pow_iff :
    (∃ k : ℕ, orderOf x = p ^ k) ↔ ∃ m : ℕ, x ^ (p : ℕ) ^ m = 1 :=
  ⟨fun ⟨k, hk⟩ => ⟨k, by rw [← hk, pow_orderOf_eq_one]⟩, fun ⟨_, hm⟩ => by
    obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
    exact ⟨k, hk⟩⟩

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ k, orderOf x = p ^ k
k : ℕ
hk : orderOf x = p ^ k
⊢ x ^ p ^ k = 1

Tactic:
rw [← hk, pow_orderOf_eq_one]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
k : ℕ
left✝ : k ≤ w✝
hk : orderOf x = p ^ k
⊢ ∃ k, orderOf x = p ^ k

Tactic:
exact ⟨k, hk⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
⊢ ∃ k, orderOf x = p ^ k

Tactic:
obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)

Result:
case intro.intro
G : Type u_1
inst✝ : Monoid G
x : G
p : ℕ
hp : Fact (Nat.Prime p)
x✝ : ∃ m, x ^ p ^ m = 1
w✝ : ℕ
hm : x ^ p ^ w✝ = 1
k : ℕ
left✝ : k ≤ w✝
hk : orderOf x = p ^ k
⊢ ∃ k, orderOf x = p ^ k
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_eq_iff_eq_toPMF (μ : Measure α) [IsProbabilityMeasure μ] :
    p.toMeasure = μ ↔ p = μ.toPMF

Proof state:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ p.toMeasure = μ ↔ p = μ.toPMF

Tactic:
rw [← toMeasure_inj, Measure.toPMF_toMeasure]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_eq_zero : Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

Proof state:
α : Type u_1
⊢ Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α

Tactic:
simp [Nat.card, mk_eq_zero_iff, aleph0_le_mk_iff]

Result:
no goals
-- Mathlib/Topology/ExtendFrom.lean
theorem continuous_extendFrom [RegularSpace Y] {f : X → Y} {A : Set X} (hA : Dense A)
    (hf : ∀ x, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)) : Continuous (extendFrom A f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ Continuous (extendFrom A f)

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) univ

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ∀ x ∈ univ, ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)

Tactic:
simpa using hf

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) univ

Tactic:
exact continuousOn_extendFrom (fun x _ ↦ hA x) (by simpa using hf)

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem cospan {i j j' : C} (f : j ⟶ i) (f' : j' ⟶ i) :
    ∃ (k : C) (g : k ⟶ j) (g' : k ⟶ j'), g ≫ f = g' ≫ f' :=
  let ⟨K, G, G', _⟩ := IsCofilteredOrEmpty.cone_objs j j'
  let ⟨k, e, he⟩ := IsCofilteredOrEmpty.cone_maps (G ≫ f) (G' ≫ f')
  ⟨k, e ≫ G, e ≫ G', by simpa only [Category.assoc] using he⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
i j j' : C
f : j ⟶ i
f' : j' ⟶ i
K : C
G : K ⟶ j
G' : K ⟶ j'
h✝ : True
k : C
e : k ⟶ K
he : e ≫ G ≫ f = e ≫ G' ≫ f'
⊢ (e ≫ G) ≫ f = (e ≫ G') ≫ f'

Tactic:
simpa only [Category.assoc] using he

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem neg_birthday_le : -x.birthday.toPGame ≤ x

Proof state:
x : PGame
⊢ -x.birthday.toPGame ≤ x

Tactic:
simpa only [birthday_neg, ← neg_le_iff] using le_birthday (-x)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.clm_comp (hc : HasDerivWithinAt c c' s x)
    (hd : HasDerivWithinAt d d' s x) :
    HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x

Tactic:
have := (hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).hasDerivWithinAt

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
this :
  HasDerivWithinAt (fun y => (c y).comp (d y))
    ((((compL 𝕜 E F G) (c x)).comp (smulRight 1 d') + ((compL 𝕜 E F G).flip (d x)).comp (smulRight 1 c')) 1) s x
⊢ HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
this :
  HasDerivWithinAt (fun y => (c y).comp (d y))
    ((((compL 𝕜 E F G) (c x)).comp (smulRight 1 d') + ((compL 𝕜 E F G).flip (d x)).comp (smulRight 1 c')) 1) s x
⊢ HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x

Tactic:
rwa [add_apply, comp_apply, comp_apply, smulRight_apply, smulRight_apply, one_apply, one_smul,
  one_smul, add_comm] at this

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_eraseMin : ∀ t : Ordnode α, dual (eraseMin t) = eraseMax (dual t)
  | nil => rfl
  | node _ nil _ _ => rfl
  | node _ (node sz l' y r') x r => by
    rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]

Proof state:
α : Type u_1
size✝ sz : ℕ
l' : Ordnode α
y : α
r' : Ordnode α
x : α
r : Ordnode α
⊢ (node size✝ (node sz l' y r') x r).eraseMin.dual = (node size✝ (node sz l' y r') x r).dual.eraseMax

Tactic:
rw [eraseMin, dual_balanceR, dual_eraseMin (node sz l' y r'), dual, dual, dual, eraseMax]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)] lemma oneLePart_div_leOnePart (a : α) : a⁺ᵐ / a⁻ᵐ = a

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ / a⁻ᵐ = a

Tactic:
rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
  sup_comm, oneLePart_def]

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem div2_bit (b n) : div2 (bit b n) = n

Proof state:
case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
case true
n : ℤ
⊢ ofNat (1 / 2) = 0

Tactic:
rw [Nat.div_eq_of_lt] <;> simp

Result:
no goals

Proof state:
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
cases b

Result:
case false
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0

case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Proof state:
case true
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

Tactic:
show ofNat _ = _

Result:
case true
n : ℤ
⊢ ofNat (1 / 2) = 0

Proof state:
case false
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0

Tactic:
decide

Result:
no goals

Proof state:
b : Bool
n : ℤ
⊢ (bit b n).div2 = n

Tactic:
rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]

Result:
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
b : Bool
n : ℤ
⊢ 2 ≠ 0
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_lineMap_lineMap (p₁ p₂ : P) (c₁ c₂ : 𝕜) :
    dist (lineMap p₁ p₂ c₁) (lineMap p₁ p₂ c₂) = dist c₁ c₂ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂

Tactic:
rw [dist_comm p₁ p₂]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c₁ c₂ : 𝕜
⊢ dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁

Tactic:
simp only [lineMap_apply, dist_eq_norm_vsub, vadd_vsub_vadd_cancel_right,
  ← sub_smul, norm_smul, vsub_eq_sub]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem not_isCofinal_iff_bddAbove [NoMaxOrder α] {s : Set α} : ¬ IsCofinal s ↔ BddAbove s

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
z : α
hz : x < z
⊢ ∃ x, ∀ y ∈ s, y < x

Tactic:
exact ⟨z, fun y hy ↦ (h hy).trans_lt hz⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ∃ x, ∀ y ∈ s, y < x

Tactic:
rintro ⟨x, h⟩

Result:
case mpr.intro
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ ∃ x, ∀ y ∈ s, y < x

Proof state:
case mpr.intro
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ ∃ x, ∀ y ∈ s, y < x

Tactic:
obtain ⟨z, hz⟩ := exists_gt x

Result:
case mpr.intro.intro
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
z : α
hz : x < z
⊢ ∃ x, ∀ y ∈ s, y < x

Proof state:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ¬IsCofinal s

Tactic:
rw [not_isCofinal_iff]

Result:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ∃ x, ∀ y ∈ s, y < x

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ ¬IsCofinal s ↔ BddAbove s

Tactic:
use .of_not_isCofinal

Result:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
s : Set α
⊢ BddAbove s → ¬IsCofinal s
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_one (μ : FiniteMeasure Ω) : μ.testAgainstNN 1 = μ.mass

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ (↑μ univ).toNNReal = μ.mass

Tactic:
rfl

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 1 = μ.mass

Tactic:
simp only [testAgainstNN, coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_one]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ (↑μ univ).toNNReal = μ.mass
-- Mathlib/Data/List/Basic.lean
theorem sizeOf_lt_sizeOf_of_mem [SizeOf α] {x : α} {l : List α} (hx : x ∈ l) :
    SizeOf.sizeOf x < SizeOf.sizeOf l

Proof state:
case cons.tail
α : Type u
inst✝ : SizeOf α
x h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ sizeOf x < 1 + sizeOf h + sizeOf t

Tactic:
specialize ih ‹_›

Result:
case cons.tail
α : Type u
inst✝ : SizeOf α
x h : α
t : List α
a✝ : Mem x t
ih : sizeOf x < sizeOf t
⊢ sizeOf x < 1 + sizeOf h + sizeOf t

Proof state:
case cons.tail
α : Type u
inst✝ : SizeOf α
x h : α
t : List α
a✝ : Mem x t
ih : sizeOf x < sizeOf t
⊢ sizeOf x < 1 + sizeOf h + sizeOf t

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
inst✝ : SizeOf α
x : α
l : List α
hx : x ∈ l
⊢ sizeOf x < sizeOf l

Tactic:
induction' l with h t ih <;> cases hx <;> rw [cons.sizeOf_spec]

Result:
case cons.head
α : Type u
inst✝ : SizeOf α
x : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
⊢ sizeOf x < 1 + sizeOf x + sizeOf t

case cons.tail
α : Type u
inst✝ : SizeOf α
x h : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
a✝ : Mem x t
⊢ sizeOf x < 1 + sizeOf h + sizeOf t

Proof state:
case cons.head
α : Type u
inst✝ : SizeOf α
x : α
t : List α
ih : x ∈ t → sizeOf x < sizeOf t
⊢ sizeOf x < 1 + sizeOf x + sizeOf t

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_diff_Ioo_self (h : a ≤ b) : Icc a b \ Ioo a b = {a, b}

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}

Tactic:
simp [← coe_inj, h]

Result:
no goals