harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Basic.lean
theorem injective_foldl_comp {l : List (α → α)} {f : α → α}
    (hl : ∀ f ∈ l, Function.Injective f) (hf : Function.Injective f) :
    Function.Injective (@List.foldl (α → α) (α → α) Function.comp f l)

Proof state:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective lh

Tactic:
apply hl _ (List.mem_cons_self _ _)

Result:
no goals

Proof state:
α : Type u
l : List (α → α)
f : α → α
hl : ∀ (f : α → α), f ∈ l → Injective f
hf : Injective f
⊢ Injective (foldl comp f l)

Tactic:
induction' l with lh lt l_ih generalizing f

Result:
case nil
α : Type u
f : α → α
hl : ∀ (f : α → α), f ∈ [] → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])

case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))

Proof state:
case nil
α : Type u
f : α → α
hl : ∀ (f : α → α), f ∈ [] → Injective f
hf : Injective f
⊢ Injective (foldl comp f [])

Tactic:
exact hf

Result:
no goals

Proof state:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)

Tactic:
apply Function.Injective.comp hf

Result:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective lh

Proof state:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (foldl comp f (lh :: lt))

Tactic:
apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)

Result:
case cons
α : Type u
lh : α → α
lt : List (α → α)
l_ih : ∀ {f : α → α}, (∀ (f : α → α), f ∈ lt → Injective f) → Injective f → Injective (foldl comp f lt)
f : α → α
hl : ∀ (f : α → α), f ∈ lh :: lt → Injective f
hf : Injective f
⊢ Injective (f ∘ lh)
-- Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean
theorem exists_pair_mem_lattice_not_disjoint_vadd [AddCommGroup L] [Countable L] [AddAction L E]
    [MeasurableSpace L] [MeasurableVAdd L E] [VAddInvariantMeasure L E μ]
    (fund : IsAddFundamentalDomain L F μ) (hS : NullMeasurableSet s μ) (h : μ F < μ s) :
    ∃ x y : L, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)

Proof state:
E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddCommGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F μ
hS : NullMeasurableSet s μ
h : ∀ (x y : L), x ≠ y → Disjoint (x +ᵥ s) (y +ᵥ s)
⊢ μ s ≤ μ F

Tactic:
exact ((fund.measure_eq_tsum _).trans (measure_iUnion₀
  (Pairwise.mono h fun i j hij => (hij.mono inf_le_left inf_le_left).aedisjoint)
    fun _ => (hS.vadd _).inter fund.nullMeasurableSet).symm).trans_le
    (measure_mono <| Set.iUnion_subset fun _ => Set.inter_subset_right)

Result:
no goals

Proof state:
E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddCommGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F μ
hS : NullMeasurableSet s μ
h : μ F < μ s
⊢ ∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)

Tactic:
contrapose! h

Result:
E : Type u_1
L : Type u_2
inst✝⁶ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁵ : AddCommGroup L
inst✝⁴ : Countable L
inst✝³ : AddAction L E
inst✝² : MeasurableSpace L
inst✝¹ : MeasurableVAdd L E
inst✝ : VAddInvariantMeasure L E μ
fund : IsAddFundamentalDomain L F μ
hS : NullMeasurableSet s μ
h : ∀ (x y : L), x ≠ y → Disjoint (x +ᵥ s) (y +ᵥ s)
⊢ μ s ≤ μ F
-- Mathlib/Algebra/Group/Opposite.lean
theorem semiconjBy_unop [Mul α] {a x y : αᵐᵒᵖ} :
    SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

Proof state:
α : Type u_1
inst✝ : Mul α
a x y : αᵐᵒᵖ
⊢ SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

Tactic:
conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracket_smul_left
    (hV : MDifferentiableAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) x) :
    mlieBracket I (c • V) W x = c • mlieBracket I V W x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
⊢ mlieBracket I (c • V) W x = c • mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ, ← contMDiffWithinAt_univ] at hV ⊢

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
⊢ mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
⊢ mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_smul_left hV (uniqueMDiffWithinAt_univ _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_ofReal_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) :
    log (r * x) = Real.log r + log x

Proof state:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x

Tactic:
simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le,
  Real.log_mul hr.ne' hx, ofReal_add, add_assoc]

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x

Tactic:
replace hx := norm_ne_zero_iff.mpr hx

Result:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_iSup {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (range f)) :
    lift.{u} (iSup f) = ⨆ i, lift.{u} (f i)

Proof state:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i => lift.{u, w} (f i))

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (iSup f) = ⨆ i, lift.{u, w} (f i)

Tactic:
rw [iSup, iSup, lift_sSup hf, ← range_comp]

Result:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i => lift.{u, w} (f i))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/BEq.lean
theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : List α
⊢ a.beq b = a.isEqv b fun x1 x2 => x1 == x2

Tactic:
induction a generalizing b with
| nil =>
  cases b <;> simp
| cons a as ih =>
  cases b with
  | nil => simp
  | cons b bs =>
    simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
      Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
      Bool.decide_eq_true]
    split <;> simp

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : BEq α
a : α
as : List α
ih : ∀ (b : List α), as.beq b = as.isEqv b fun x1 x2 => x1 == x2
⊢ (a :: as).beq [] = (a :: as).isEqv [] fun x1 x2 => x1 == x2

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a : α
as : List α
ih : ∀ (b : List α), as.beq b = as.isEqv b fun x1 x2 => x1 == x2
b : List α
⊢ (a :: as).beq b = (a :: as).isEqv b fun x1 x2 => x1 == x2

Tactic:
cases b with
| nil => simp
| cons b bs =>
  simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
    Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
    Bool.decide_eq_true]
  split <;> simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : BEq α
a : α
as : List α
ih : ∀ (b : List α), as.beq b = as.isEqv b fun x1 x2 => x1 == x2
b : α
bs : List α
⊢ (a :: as).beq (b :: bs) = (a :: as).isEqv (b :: bs) fun x1 x2 => x1 == x2

Tactic:
simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
  Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
  Bool.decide_eq_true]

Result:
case cons.cons
α : Type u_1
inst✝ : BEq α
a : α
as : List α
ih : ∀ (b : List α), as.beq b = as.isEqv b fun x1 x2 => x1 == x2
b : α
bs : List α
⊢ (a == b &&
      if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length), (as[i] == bs[i]) = true) else false) =
    if h : as.length = bs.length then a == b && decide (∀ (m : Nat) (h_1 : m < as.length), (as[m] == bs[m]) = true)
    else false

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
b : List α
⊢ [].beq b = [].isEqv b fun x1 x2 => x1 == x2

Tactic:
cases b <;> simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : BEq α
a : α
as : List α
ih : ∀ (b : List α), as.beq b = as.isEqv b fun x1 x2 => x1 == x2
b : α
bs : List α
⊢ (a == b &&
      if h : as.length = bs.length then decide (∀ (i : Nat) (h' : i < as.length), (as[i] == bs[i]) = true) else false) =
    if h : as.length = bs.length then a == b && decide (∀ (m : Nat) (h_1 : m < as.length), (as[m] == bs[m]) = true)
    else false

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
/-- `IsCoprime` is not a useful definition for `PNat`; consider using `Nat.Coprime` instead. -/
lemma PNat.isCoprime_iff {m n : ℕ+} : IsCoprime (m : ℕ) n ↔ m = 1 ∨ n = 1

Proof state:
m n : ℕ+
⊢ IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem prod_eq_inf {A : C} {f₁ f₂ : Subobject A} [HasBinaryProduct f₁ f₂] :
    (f₁ ⨯ f₂) = f₁ ⊓ f₂

Proof state:
case a.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂

Tactic:
exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂

Tactic:
apply le_antisymm

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)

Tactic:
apply leOfHom

Result:
case a.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂

Tactic:
refine le_inf _ _ _ (Limits.prod.fst.le) (Limits.prod.snd.le)

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem zero_mul [Fintype m] (M : Matrix m n α) : (0 : Matrix l m α) * M = 0

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
i✝ : l
j✝ : n
⊢ (0 * M) i✝ j✝ = 0 i✝ j✝

Tactic:
apply zero_dotProduct

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
⊢ 0 * M = 0

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
i✝ : l
j✝ : n
⊢ (0 * M) i✝ j✝ = 0 i✝ j✝
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem coeFn_negPart_eq_max (f : Lp ℝ p μ) : ∀ᵐ a ∂μ, negPart f a = max (-f a) 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(posPart (-f)) a = -↑↑f a ⊔ 0

Tactic:
filter_upwards [coeFn_posPart (-f), coeFn_neg f] with _ h₁ h₂

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = ↑↑(-f) a✝ ⊔ 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ ↑↑(posPart (-f)) a✝ = -↑↑f a✝ ⊔ 0

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = ↑↑(-f) a✝ ⊔ 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ ↑↑(posPart (-f)) a✝ = -↑↑f a✝ ⊔ 0

Tactic:
rw [h₁, h₂, Pi.neg_apply]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(negPart f) a = -↑↑f a ⊔ 0

Tactic:
rw [negPart]

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp ℝ p μ)
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(posPart (-f)) a = -↑↑f a ⊔ 0
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem isOpen_cPolynomialAt : IsOpen { x | CPolynomialAt 𝕜 f x }

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ {x | CPolynomialAt 𝕜 f x} ∈ 𝓝 x

Tactic:
exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.cPolynomialAt_of_mem hy

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ IsOpen {x | CPolynomialAt 𝕜 f x}

Tactic:
rw [isOpen_iff_mem_nhds]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ∀ x ∈ {x | CPolynomialAt 𝕜 f x}, {x | CPolynomialAt 𝕜 f x} ∈ 𝓝 x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ∀ x ∈ {x | CPolynomialAt 𝕜 f x}, {x | CPolynomialAt 𝕜 f x} ∈ 𝓝 x

Tactic:
rintro x ⟨p, n, r, hr⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ {x | CPolynomialAt 𝕜 f x} ∈ 𝓝 x
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.node4L {l x m y r} (hl : @Sized α l) (hm : Sized m) (hr : Sized r) :
    Sized (node4L l x m y r)

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hl : l.Sized
hm : m.Sized
hr : r.Sized
⊢ (l.node4L x m y r).Sized

Tactic:
cases m <;> [exact (hl.node' hm).node' hr; exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)]

Result:
no goals
-- Mathlib/Analysis/Convex/GaugeRescale.lean
theorem gauge_gaugeRescale_le (s t : Set E) (x : E) :
    gauge t (gaugeRescale s t x) ≤ gauge s x

Proof state:
case pos
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
simp [gaugeRescale, hx, gauge_nonneg]

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : ¬gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
exact (gauge_gaugeRescale' s hx).le

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

Tactic:
by_cases hx : gauge t x = 0

Result:
case pos
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x

case neg
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
x : E
hx : ¬gauge t x = 0
⊢ gauge t (gaugeRescale s t x) ≤ gauge s x
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem sheafifyMap_comp {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R) :
    J.sheafifyMap (η ≫ γ) = J.sheafifyMap η ≫ J.sheafifyMap γ

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ J.plusMap (J.plusMap (η ≫ γ)) = J.plusMap (J.plusMap η) ≫ J.plusMap (J.plusMap γ)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ J.sheafifyMap (η ≫ γ) = J.sheafifyMap η ≫ J.sheafifyMap γ

Tactic:
dsimp [sheafifyMap, sheafify]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ J.plusMap (J.plusMap (η ≫ γ)) = J.plusMap (J.plusMap η) ≫ J.plusMap (J.plusMap γ)
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_add_tsub_comm (hb : AddLECancellable b) (hd : AddLECancellable d)
    (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d)

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)

Tactic:
rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem any_beq [BEq α] {xs : Array α} {a : α} : (xs.any fun x => a == x) = xs.contains a

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.any fun x => a == x) = { toList := toList✝ }.contains a

Tactic:
simp [List.any_beq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
xs : Array α
a : α
⊢ (xs.any fun x => a == x) = xs.contains a

Tactic:
cases xs

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
toList✝ : List α
⊢ ({ toList := toList✝ }.any fun x => a == x) = { toList := toList✝ }.contains a
-- Mathlib/Topology/LocallyConstant/Basic.lean
@[simp]
lemma piecewise'_apply_right {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
    (h₂ : IsClosed C₂) (f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)
    [DecidablePred (· ∈ C₁)] (hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩)
    (x : C₀) (hx : x.val ∈ C₂) :
    piecewise' h₀ h₁ h₂ f₁ f₂ hf x = f₂ ⟨x.val, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩

Tactic:
rw [piecewise', piecewise_apply_right (f := (f₁.comap
  ⟨(restrictPreimage C₁ ((↑) : C₀ → X)), continuous_subtype_val.restrictPreimage⟩))
  (hx := hx)]

Result:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, hx⟩ = f₂ ⟨↑x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩

Tactic:
letI : ∀ j : C₀, Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) Iff.rfl

Result:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed C₁
h₂ : IsClosed C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x => x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
x : ↑C₀
hx : ↑x ∈ C₂
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j => decidable_of_iff (↑j ∈ C₁) ⋯
⊢ (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, hx⟩ = f₂ ⟨↑x, hx⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma Differentiable.add_iff_right (hg : Differentiable 𝕜 f) :
    Differentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 g

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
hg : Differentiable 𝕜 f
⊢ (Differentiable 𝕜 fun y => f y + g y) ↔ Differentiable 𝕜 g

Tactic:
simp only [add_comm (f _), hg.add_iff_left]

Result:
no goals