harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Cofinite.lean
theorem coprod_cofinite : (cofinite : Filter α).coprod (cofinite : Filter β) = cofinite :=
  Filter.coext fun s => by
    simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

Proof state:
α : Type u_2
β : Type u_3
s : Set (α × β)
⊢ sᶜ ∈ cofinite.coprod cofinite ↔ sᶜ ∈ cofinite

Tactic:
simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem card_commutatorSet_closureCommutatorRepresentatives :
    Nat.card (commutatorSet (closureCommutatorRepresentatives G)) = Nat.card (commutatorSet G)

Proof state:
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) =
    Nat.card ↑(⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G))

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ (subtype_injective _))

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) = Nat.card ↑(commutatorSet G)

Tactic:
rw [← image_commutatorSet_closureCommutatorRepresentatives G]

Result:
G : Type u
inst✝ : Group G
⊢ Nat.card ↑(commutatorSet ↥(closureCommutatorRepresentatives G)) =
    Nat.card ↑(⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G))
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_nat_mul_two_pi_sub_pi (n : ℕ) : cos (n * (2 * π) - π) = -1

Proof state:
n : ℕ
⊢ cos (↑n * (2 * ↑π) - ↑π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).sub_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdrop_nil : rdrop ([] : List α) n = []

Proof state:
α : Type u_1
n : ℕ
⊢ [].rdrop n = []

Tactic:
simp [rdrop]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma le_expect (hs : s.Nonempty) (h : ∀ x ∈ s, a ≤ f x) : a ≤ 𝔼 i ∈ s, f i :=
  (le_inv_smul_iff_of_pos <| mod_cast hs.card_pos).2 <| by
    rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ ↑(#s) • a ≤ ∑ i ∈ s, (fun i => f i) i

Tactic:
rw [Nat.cast_smul_eq_nsmul]

Result:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun i => f i) i

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun i => f i) i

Tactic:
exact card_nsmul_le_sum _ _ _ h

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
theorem isBigO_symm_asympBound : asympBound g a b =O[atTop] T

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ asympBound g a b =O[atTop] T

Tactic:
calc asympBound g a b = (fun n => 1 * asympBound g a b n) := by simp
               _ ~[atTop] (fun n => (1 + ε n) * asympBound g a b n) := by
                          refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl
                          rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero,
                            ← Function.comp_def (fun n => 1 + ε n) Nat.cast]
                          exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
                            tendsto_natCast_atTop_atTop
               _ =O[atTop] T := R.smoothingFn_mul_asympBound_isBigO_T

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n => 1 + ε ↑n) ~[atTop] fun n => 1

Tactic:
rw [Function.const_def, isEquivalent_const_iff_tendsto one_ne_zero,
  ← Function.comp_def (fun n => 1 + ε n) Nat.cast]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n => 1 + ε n) ∘ Nat.cast) atTop (𝓝 1)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ asympBound g a b = fun n => 1 * asympBound g a b n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n => 1 * asympBound g a b n) ~[atTop] fun n => (1 + ε ↑n) * asympBound g a b n

Tactic:
refine IsEquivalent.mul (IsEquivalent.symm ?_) IsEquivalent.refl

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ (fun n => 1 + ε ↑n) ~[atTop] fun n => 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Tendsto ((fun n => 1 + ε n) ∘ Nat.cast) atTop (𝓝 1)

Tactic:
exact Tendsto.comp isEquivalent_one_add_smoothingFn_one.tendsto_const
  tendsto_natCast_atTop_atTop

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
theorem toNat_add {m n : ℕ∞} (hm : m ≠ ⊤) (hn : n ≠ ⊤) : toNat (m + n) = toNat m + toNat n

Proof state:
case intro
n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ (↑m + n).toNat = (↑m).toNat + n.toNat

Tactic:
lift n to ℕ using hn

Result:
case intro.intro
m n : ℕ
⊢ (↑m + ↑n).toNat = (↑m).toNat + (↑n).toNat

Proof state:
case intro.intro
m n : ℕ
⊢ (↑m + ↑n).toNat = (↑m).toNat + (↑n).toNat

Tactic:
rfl

Result:
no goals

Proof state:
m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ (m + n).toNat = m.toNat + n.toNat

Tactic:
lift m to ℕ using hm

Result:
case intro
n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ (↑m + n).toNat = (↑m).toNat + n.toNat
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem mem_fixedPoints_iff {α : Type*} {f : α → α} {x : α} : x ∈ fixedPoints f ↔ f x = x

Proof state:
α : Type u_1
f : α → α
x : α
⊢ x ∈ fixedPoints f ↔ f x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma IsInvertible.inverse_apply_eq {f : M →L[R] M₂} {x : M} {y : M₂} (hf : f.IsInvertible) :
    f.inverse y = x ↔ y = f x

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
x : M
y : M₂
hf : f.IsInvertible
⊢ f.inverse y = x ↔ y = f x

Tactic:
rcases hf with ⟨M, rfl⟩

Result:
case intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M✝
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M✝
inst✝² : Module R M✝
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ (↑M).inverse y = x ↔ y = ↑M x

Proof state:
case intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M✝
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M✝
inst✝² : Module R M✝
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ M.symm y = x ↔ y = M x

Tactic:
exact ContinuousLinearEquiv.symm_apply_eq M

Result:
no goals

Proof state:
case intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M✝
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M✝
inst✝² : Module R M✝
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ (↑M).inverse y = x ↔ y = ↑M x

Tactic:
simp only [inverse_equiv, ContinuousLinearEquiv.coe_coe]

Result:
case intro
R : Type u_3
M✝ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M✝
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M✝
inst✝² : Module R M✝
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ M.symm y = x ↔ y = M x
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_dblZ (P : Fin 3 → R) : (W'.map f).toProjective.dblZ (f ∘ P) = f (W'.dblZ P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toProjective.dblZ (⇑f ∘ P) = f (W'.dblZ P)

Tactic:
simp only [dblZ, negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z *
      ((⇑f ∘ P) y - (-(⇑f ∘ P) y - (map W' f).toProjective.a₁ * (⇑f ∘ P) x - (map W' f).toProjective.a₃ * (⇑f ∘ P) z)) ^
        3 =
    f (P z * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) ^ 3)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z *
      ((⇑f ∘ P) y - (-(⇑f ∘ P) y - (map W' f).toProjective.a₁ * (⇑f ∘ P) x - (map W' f).toProjective.a₃ * (⇑f ∘ P) z)) ^
        3 =
    f (P z * (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) ^ 3)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_ceil_left_pure (n : ℤ) : Tendsto (ceil : α → ℤ) (𝓝[≤] n) (pure n)

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ Tendsto ceil (𝓝[≤] ↑n) (pure n)

Tactic:
simpa only [ceil_intCast] using tendsto_ceil_left_pure_ceil (n : α)

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem prevD_eq (f : ∀ i j, C.X i ⟶ D.X j) {j j' : ι} (w : c.Rel j' j) :
    prevD j f = f j j' ≫ D.d j' j

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
j : ι
w : c.Rel (c.prev j) j
⊢ (prevD j) f = f j (c.prev j) ≫ D.d (c.prev j) j

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
j j' : ι
w : c.Rel j' j
⊢ (prevD j) f = f j j' ≫ D.d j' j

Tactic:
obtain rfl := c.prev_eq' w

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : (i j : ι) → C.X i ⟶ D.X j
j : ι
w : c.Rel (c.prev j) j
⊢ (prevD j) f = f j (c.prev j) ≫ D.d (c.prev j) j
-- Mathlib/Order/Interval/Set/Pi.lean
theorem pi_univ_Ioc_update_right {x y : ∀ i, α i} {i₀ : ι} {m : α i₀} (hm : m ≤ y i₀) :
    (pi univ fun i ↦ Ioc (x i) (update y i₀ m i)) =
      { z | z i₀ ≤ m } ∩ pi univ fun i ↦ Ioc (x i) (y i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i => Ioc (x i) (y i)

Tactic:
simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({i₀} : Set ι),
  singleton_pi', ← inter_assoc, this]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)

Tactic:
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
  inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ (univ.pi fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i => Ioc (x i) (y i)

Tactic:
have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm,
    inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i => Ioc (x i) (y i)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j => Ioc (x j) (y j)

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem isLimit_opow_left {a b : Ordinal} (l : IsLimit a) (hb : b ≠ 0) : IsLimit (a ^ b)

Proof state:
case inr.inl.intro
a : Ordinal.{u_1}
l : a.IsLimit
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ (a ^ succ b).IsLimit

Tactic:
rw [opow_succ]

Result:
case inr.inl.intro
a : Ordinal.{u_1}
l : a.IsLimit
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ (a ^ b * a).IsLimit

Proof state:
case inr.inl.intro
a : Ordinal.{u_1}
l : a.IsLimit
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ (a ^ b * a).IsLimit

Tactic:
exact isLimit_mul (opow_pos _ l.pos) l

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
l : a.IsLimit
hb : b ≠ 0
⊢ (a ^ b).IsLimit

Tactic:
rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l')

Result:
case inl
a b : Ordinal.{u_1}
l : a.IsLimit
hb : b ≠ 0
e : b = 0
⊢ (a ^ b).IsLimit

case inr.inl.intro
a : Ordinal.{u_1}
l : a.IsLimit
b : Ordinal.{u_1}
hb : succ b ≠ 0
⊢ (a ^ succ b).IsLimit

case inr.inr
a b : Ordinal.{u_1}
l : a.IsLimit
hb : b ≠ 0
l' : b.IsLimit
⊢ (a ^ b).IsLimit

Proof state:
case inr.inr
a b : Ordinal.{u_1}
l : a.IsLimit
hb : b ≠ 0
l' : b.IsLimit
⊢ (a ^ b).IsLimit

Tactic:
exact isLimit_opow l.one_lt l'

Result:
no goals

Proof state:
case inl
a b : Ordinal.{u_1}
l : a.IsLimit
hb : b ≠ 0
e : b = 0
⊢ (a ^ b).IsLimit

Tactic:
exact absurd e hb

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem nat_le_card {o} {n : ℕ} : (n : Cardinal) ≤ card o ↔ (n : Ordinal) ≤ o

Proof state:
o : Ordinal.{u_1}
n : ℕ
⊢ ↑n ≤ o.card ↔ ↑n ≤ o

Tactic:
rw [← Cardinal.ord_le, Cardinal.ord_nat]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem map_sup [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
    f (x ⊔ y) = f x ⊓ f y

Proof state:
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f (x ⊔ y) = f x ⊓ f y

Tactic:
cases le_total x y <;> have := hf ?_ ?_ ‹_› <;>
  first
  | assumption
  | simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Result:
no goals

Proof state:
case inr.refine_2
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
⊢ x ∈ s

Tactic:
assumption

Result:
no goals

Proof state:
case inr.refine_3
α : Type u
β : Type v
f : α → β
s : Set α
x y : α
inst✝¹ : LinearOrder α
inst✝ : SemilatticeInf β
hf : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
h✝ : y ≤ x
this : f x ≤ f y
⊢ f (x ⊔ y) = f x ⊓ f y

Tactic:
simp only [*, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapRightHomologyIso_inv_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
    F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
      (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
    (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapRightHomologyIso F).hom, ← mapRightHomologyIso_hom_naturality_assoc,
  Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
lemma pairwiseDisjoint_range_iff {α β : Type*} {f : α → (Set β)} :
    (range f).PairwiseDisjoint id ↔ ∀ x y, f x ≠ f y → Disjoint (f x) (f y)

Proof state:
α : Type u_6
β : Type u_7
f : α → Set β
⊢ (range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x ≠ f y → Disjoint (f x) (f y)

Tactic:
aesop (add simp [PairwiseDisjoint, Set.Pairwise])

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracket_add_left (hV : DifferentiableAt 𝕜 V x) (hV₁ : DifferentiableAt 𝕜 V₁ x) :
    lieBracket 𝕜 (V + V₁) W  x =
      lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ lieBracket 𝕜 (V + V₁) W x = lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x

Tactic:
simp only [lieBracket, Pi.add_apply, map_add]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 (V + V₁) x) (W x) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 V₁ x) (W x))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W x) (V₁ x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V₁ x) (W x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 V₁ x) (W x))

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 (V + V₁) x) (W x) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 V₁ x) (W x))

Tactic:
rw [fderiv_add' hV hV₁, ContinuousLinearMap.add_apply]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ : E → E
x : E
hV : DifferentiableAt 𝕜 V x
hV₁ : DifferentiableAt 𝕜 V₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W x) (V₁ x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V₁ x) (W x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W x) (V₁ x) - (fderiv 𝕜 V₁ x) (W x))
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Icc_succ_pred_eq_Ioo (a b : α) : Icc (succ a) (pred b) = Ioo a b

Proof state:
case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
by_cases hb : IsMin b

Result:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

case neg
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Proof state:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b

Tactic:
exact fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]

Result:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : PredOrder α
inst✝ : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b
-- Mathlib/Analysis/Analytic/Composition.lean
theorem comp_partialSum (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F)
    (M N : ℕ) (z : E) :
    q.partialSum M (∑ i ∈ Finset.Ico 1 N, p i fun _j => z) =
      ∑ i ∈ compPartialSumTarget 0 M N, q.compAlongComposition p i.2 fun _j => z

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ (∑ n ∈ Finset.range M, ∑ r ∈ Fintype.piFinset fun i => Finset.Ico 1 N, (q n) fun i => (p (r i)) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z

Tactic:
rw [Finset.range_eq_Ico, Finset.sum_sigma']

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
⊢ (∑ x ∈ (Finset.Ico 0 M).sigma fun n => Fintype.piFinset fun i => Finset.Ico 1 N,
      (q x.fst) fun i => (p (x.snd i)) fun _j => z) =
    ∑ i ∈ compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z

Proof state:
case h.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
M N : ℕ
z : E
k : ℕ
blocks_fun : Fin k → ℕ
H : ⟨k, blocks_fun⟩ ∈ compPartialSumSource 0 M N
i✝ : ℕ
him✝ : i✝ < ⟨k, blocks_fun⟩.fst
hin✝ : i✝ < (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd.length
⊢ ((p (⟨k, blocks_fun⟩.snd ⟨i✝, him✝⟩)) fun _j => z) =
    p.applyComposition (compChangeOfVariables 0 M N ⟨k, blocks_fun⟩ H).snd (fun _j => z) ⟨i✝, hin✝⟩

Tactic:
rw [← compChangeOfVariables_blocksFun 0 M N H, applyComposition, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_cons (p : α → Bool) (a : α) (l : List α) :
    (a :: l).takeWhile p = if p a then a :: l.takeWhile p else []

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (match p a with
    | true => a :: takeWhile p l
    | false => []) =
    if p a = true then a :: takeWhile p l else []

Tactic:
by_cases h: p a <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ takeWhile p (a :: l) = if p a = true then a :: takeWhile p l else []

Tactic:
simp only [takeWhile]

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (match p a with
    | true => a :: takeWhile p l
    | false => []) =
    if p a = true then a :: takeWhile p l else []