harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Basic.lean
lemma erase_sdiff_erase (hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = {b}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a✝ : α
⊢ a✝ ∈ s.erase a \ s.erase b ↔ a✝ ∈ {b}

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
⊢ s.erase a \ s.erase b = {b}

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
hb : b ∈ s
a✝ : α
⊢ a✝ ∈ s.erase a \ s.erase b ↔ a✝ ∈ {b}
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem exp_pow_sum [Algebra ℚ A] (n : ℕ) :
    ((Finset.range n).sum fun k => exp A ^ k) =
      PowerSeries.mk fun p => (Finset.range n).sum
        fun k => (k ^ p : A) * algebraMap ℚ A p.factorial⁻¹

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k ∈ Finset.range n, exp A ^ k = mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹

Tactic:
simp only [exp_pow_eq_rescale_exp, rescale]

Result:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x ∈ Finset.range n,
      { toFun := fun f => mk fun n => ↑x ^ n * (coeff A n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        (exp A) =
    mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹

Proof state:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n n✝ : ℕ
⊢ (coeff A n✝)
      (∑ x ∈ Finset.range n,
        { toFun := fun f => mk fun n => ↑x ^ n * (coeff A n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          (exp A)) =
    (coeff A n✝) (mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹)

Tactic:
simp only [one_div, coeff_mk, cast_pow, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
  coeff_exp, factorial, map_sum]

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ x ∈ Finset.range n,
      { toFun := fun f => mk fun n => ↑x ^ n * (coeff A n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        (exp A) =
    mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹

Tactic:
ext

Result:
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n n✝ : ℕ
⊢ (coeff A n✝)
      (∑ x ∈ Finset.range n,
        { toFun := fun f => mk fun n => ↑x ^ n * (coeff A n) f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          (exp A)) =
    (coeff A n✝) (mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p !)⁻¹)
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurveOn_comp_sub {dt : ℝ} :
    IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ (· - dt)) v (dt +ᵥ s)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
dt : ℝ
⊢ IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun x => x - dt) v (dt +ᵥ s)

Tactic:
simpa using isIntegralCurveOn_comp_add (dt := -dt)

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.neg_pow : Odd n → ∀ a : α, (-a) ^ n = -a ^ n

Proof state:
case intro
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)

Tactic:
simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n

Tactic:
rintro ⟨c, rfl⟩ a

Result:
case intro
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_push_iff {l : Vector α (n + 1)} {b : β} {f : (i : Nat) → α → (h : i < n + 1) → β} {l₂ : Vector β n} :
    l.mapFinIdx f = l₂.push b ↔
      ∃ (l₁ : Vector α n) (a : α), l = l₁.push a ∧
        l₁.mapFinIdx (fun i a h => f i a (by omega)) = l₂ ∧ b = f n a (by omega)

Proof state:
case mk.mk.mpr
α : Type u_1
β : Type u_2
b : β
l : Array α
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
h : l.size = l₂.size + 1
⊢ (∃ l₁ a, l = l₁.push a ∧ (l₁.mapFinIdx fun i a h => f i a ⋯) = l₂ ∧ b = f l₂.size a ⋯) →
    ∃ l₁ a w, (l₁.mapFinIdx fun i a_1 h_1 => f i a_1 ⋯) = l₂ ∧ b = f (l.size - 1) a ⋯

Tactic:
rintro ⟨⟨l₁, h⟩, a, rfl, h₁, rfl⟩

Result:
case mk.mk.mpr.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
l₂ : Array β
f : (i : Nat) → α → i < l₂.size + 1 → β
l₁ : Array α
h✝ : l₁.size = l₂.size
a : α
h : ({ toArray := l₁, size_toArray := h✝ }.push a).size = l₂.size + 1
h₁ : ({ toArray := l₁, size_toArray := h✝ }.mapFinIdx fun i a h => f i a ⋯) = l₂
⊢ ∃ l₁_1 a_1 w,
    (l₁_1.mapFinIdx fun i a_2 h_1 => f i a_2 ⋯) = l₂ ∧
      f l₂.size a ⋯ = f (({ toArray := l₁, size_toArray := h✝ }.push a).size - 1) a_1 ⋯
-- Mathlib/Algebra/Order/Floor.lean
lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉₊ ≤ a) : b * a < ⌊a⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b * (↑⌊a⌋₊ + 1) ≤ ↑⌊a⌋₊

Tactic:
rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
  ← ceil_le]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ 0 < 1 - b

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b * a < ↑⌊a⌋₊

Tactic:
calc
  b * a < b * (⌊a⌋₊ + 1) := by gcongr; exacts [hb₀, lt_floor_add_one _]
  _ ≤ ⌊a⌋₊ := by
    rw [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
      ← ceil_le]
    exact le_floor hba

Result:
no goals

Proof state:
case a0
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ 0 < b

case bc
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ a < ↑⌊a⌋₊ + 1

Tactic:
exacts [hb₀, lt_floor_add_one _]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b * a < b * (↑⌊a⌋₊ + 1)

Tactic:
gcongr

Result:
case a0
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ 0 < b

case bc
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ a < ↑⌊a⌋₊ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ ⌈b / (1 - b)⌉₊ ≤ ⌊a⌋₊

Tactic:
exact le_floor hba

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem coe_mkFinCons {n : ℕ} {N : Submodule R M} (y : M) (b : Basis (Fin n) R N)
    (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0) (hsp : ∀ z : M, ∃ c : R, z + c • y ∈ N) :
    (mkFinCons y b hli hsp : Fin (n + 1) → M) = Fin.cons y ((↑) ∘ b)

Proof state:
R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(let_fun span_b := ⋯;
      Basis.mk ⋯ ⋯) =
    Fin.cons y (Subtype.val ∘ ⇑b)

Tactic:
exact coe_mk (v := Fin.cons y (N.subtype ∘ b)) _ _

Result:
no goals

Proof state:
R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(mkFinCons y b hli hsp) = Fin.cons y (Subtype.val ∘ ⇑b)

Tactic:
unfold mkFinCons

Result:
R : Type u_3
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
N : Submodule R M
y : M
b : Basis (Fin n) R ↥N
hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0
hsp : ∀ (z : M), ∃ c, z + c • y ∈ N
⊢ ⇑(let_fun span_b := ⋯;
      Basis.mk ⋯ ⋯) =
    Fin.cons y (Subtype.val ∘ ⇑b)
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.mul_toMatrix₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) :
    M * LinearMap.toMatrix₂ b₁ b₂ B =
      LinearMap.toMatrix₂ b₁' b₂ (B.comp (toLin b₁' b₁ Mᵀ))

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
n : Type u_11
m : Type u_12
n' : Type u_13
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁'
b₁' : Basis n' R M₁'
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix n' n R
⊢ M * (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁' b₂) (B ∘ₗ (toLin b₁' b₁) Mᵀ)

Tactic:
rw [LinearMap.toMatrix₂_comp b₁, toMatrix_toLin, transpose_transpose]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.map_eq_map' {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z]
    (f : W ⟶ Y) (g : X ⟶ Z) : biprod.map f g = biprod.map' f g

Proof state:
case h₀.h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.left } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.right } ≫
        (mapPair f g).app { as := WalkingPair.right } =
    f ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.left } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.right }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
lemma cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
    (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s)

Proof state:
case a
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => ‖cexp (a * ↑x ^ 2 + b * ↑x)‖) =o[atTop] fun x => x ^ s

Tactic:
convert rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s with x

Result:
case h.e'_7.h
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ‖cexp (a * ↑x ^ 2 + b * ↑x)‖ = rexp (a.re * x ^ 2 + b.re * x)

Proof state:
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x => x ^ s

Tactic:
apply Asymptotics.IsLittleO.of_norm_left

Result:
case a
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x => ‖cexp (a * ↑x ^ 2 + b * ↑x)‖) =o[atTop] fun x => x ^ s

Proof state:
case h.e'_7.h
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
⊢ ‖cexp (a * ↑x ^ 2 + b * ↑x)‖ = rexp (a.re * x ^ 2 + b.re * x)

Tactic:
simp_rw [Complex.norm_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
    re_ofReal_mul, mul_comm _ (re _)]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
    ((Ico n m).filter fun x => l ≤ x) = Ico n m :=
  filter_eq_self.2 fun k hk => by
    rw [decide_eq_true_eq]
    exact le_trans hln (mem.1 hk).1

Proof state:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k

Tactic:
exact le_trans hln (mem.1 hk).1

Result:
no goals

Proof state:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ decide (l ≤ k) = true

Tactic:
rw [decide_eq_true_eq]

Result:
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
lemma cast_addConst_mul_card (A B : Finset G') : (σ[A, B] * #A : 𝕜) = #(A + B)

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑σ[A, B] * ↑(#A) = ↑(#(A + B))

Tactic:
norm_cast

Result:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ σ[A, B] * ↑(#A) = ↑(#(A + B))

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ σ[A, B] * ↑(#A) = ↑(#(A + B))

Tactic:
exact addConst_mul_card _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem rank_lt_rank_dual' {V : Type u} [AddCommGroup V] [Module K V] (h : ℵ₀ ≤ Module.rank K V) :
    Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Proof state:
case h.e'_3
K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)

Tactic:
rw [lift_id]

Result:
no goals

Proof state:
K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
convert lift_rank_lt_rank_dual' h

Result:
case h.e'_3
K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_const_iff {c : F''} : (f'' =O[l] fun _x => c) ↔
    (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (· ≤ ·) l fun x => ‖f'' x‖

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ (f'' =O[l] fun _x => c) ↔ (c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖

Tactic:
refine ⟨fun h => ⟨fun hc => isBigO_zero_right_iff.1 (by rwa [← hc]), h.isBoundedUnder_le⟩, ?_⟩

Result:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ ((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖) → f'' =O[l] fun _x => c

Proof state:
case intro.inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
hc : c = 0
⊢ f'' =O[l] fun _x => c

case intro.inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
hc : c ≠ 0
⊢ f'' =O[l] fun _x => c

Tactic:
exacts [(hcf hc).trans_isBigO (isBigO_zero _ _), hf.isBigO_const hc]

Result:
no goals

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
h : f'' =O[l] fun _x => c
hc : c = 0
⊢ f'' =O[l] fun _x => 0

Tactic:
rwa [← hc]

Result:
no goals

Proof state:
case intro
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
⊢ f'' =O[l] fun _x => c

Tactic:
rcases eq_or_ne c 0 with (hc | hc)

Result:
case intro.inl
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
hc : c = 0
⊢ f'' =O[l] fun _x => c

case intro.inr
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
hc : c ≠ 0
⊢ f'' =O[l] fun _x => c

Proof state:
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
⊢ ((c = 0 → f'' =ᶠ[l] 0) ∧ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖) → f'' =O[l] fun _x => c

Tactic:
rintro ⟨hcf, hf⟩

Result:
case intro
α : Type u_1
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f'' : α → E''
l : Filter α
c : F''
hcf : c = 0 → f'' =ᶠ[l] 0
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f'' x‖
⊢ f'' =O[l] fun _x => c
-- Mathlib/RingTheory/Binomial.lean
theorem choose_zero_right' (r : R) : choose r 0 = (r + 1) ^ 0

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ Nat.factorial 0 • multichoose (r - ↑0 + 1) 0 = Nat.factorial 0 • (r + 1) ^ 0

Tactic:
simp [factorial_nsmul_multichoose_eq_ascPochhammer]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose (r - ↑0 + 1) 0 = (r + 1) ^ 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 0)]

Result:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ Nat.factorial 0 • multichoose (r - ↑0 + 1) 0 = Nat.factorial 0 • (r + 1) ^ 0

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ choose r 0 = (r + 1) ^ 0

Tactic:
dsimp only [choose]

Result:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose (r - ↑0 + 1) 0 = (r + 1) ^ 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Pairwise.lean
theorem forall_mem_pwFilter [DecidableRel (α := α) R]
    (neg_trans : ∀ {x y z}, R x z → R x y ∨ R y z) (a : α) (l : List α) :
    (∀ b ∈ pwFilter R l, R a b) ↔ ∀ b ∈ l, R a b

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
this : (decide ¬R x k) = true
⊢ ¬R x k

Tactic:
rw [decide_eq_true_iff] at this

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
neg_trans : ∀ {x y z : α}, R x z → R x y ∨ R y z
a x : α
l : List α
IH : (∀ (b : α), b ∈ pwFilter R l → R a b) → ∀ (b : α), b ∈ l → R a b
h : ¬∀ (y : α), y ∈ pwFilter R l → R x y
H : ∀ (b : α), b ∈ pwFilter R l → R a b
k : α
e : find? (fun y => decide ¬R x y) (pwFilter R l) = some k
this : ¬R x k
⊢ ¬R x k
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_μ_fst (X Y : C) : (μ (prod' F G) X Y).1 = μ F X Y

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 : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = μ F X Y

Tactic:
rfl

Result:
no goals

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 : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 ≫ F.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).1) = μ F X Y

Tactic:
rw [Functor.map_id, Category.comp_id]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = μ F X Y

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 : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod' G) X Y).1 = μ F X Y

Tactic:
change _ ≫ F.map (𝟙 _) = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X Y : C
⊢ (μ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 ≫ F.map (𝟙 ((diag C).obj X ⊗ (diag C).obj Y).1) = μ F X Y
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
    ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f'.extend I) x ∈ ↑(f'.extend I) '' (f'.source ∩ f.source)

Tactic:
exact mem_image_of_mem _ ⟨hxf', hxf⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ContDiffWithinAt 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) (range ↑I) (↑(f'.extend I) x)

Tactic:
refine contDiffWithinAt_extend_coord_change hf hf' ?_

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f'.extend I) x ∈ ((f'.extend I).symm ≫ f.extend I).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f'.extend I) x ∈ ((f'.extend I).symm ≫ f.extend I).source

Tactic:
rw [← extend_image_source_inter]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
x : M
hxf : x ∈ f.source
hxf' : x ∈ f'.source
⊢ ↑(f'.extend I) x ∈ ↑(f'.extend I) '' (f'.source ∩ f.source)
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_def [DecidableEq σ] (i : σ) : pderiv i = mkDerivation R (Pi.single i 1)

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ pderiv i = mkDerivation R (Pi.single i 1)

Tactic:
unfold pderiv

Result:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ mkDerivation R (Pi.single i 1) = mkDerivation R (Pi.single i 1)

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
⊢ mkDerivation R (Pi.single i 1) = mkDerivation R (Pi.single i 1)

Tactic:
congr!

Result:
no goals