harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem choose_exists_companion : Q.exists_companion.choose = polarBilin Q :=
  LinearMap.ext₂ fun x y => by
    rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub,
      add_sub_cancel_left]

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ (⋯.choose x) y = (Q.polarBilin x) y

Tactic:
rw [polarBilin_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub,
  add_sub_cancel_left]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_b₆ : (W.variableChange C).b₆ =
    C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (W.variableChange C).b₆ = ↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)

Tactic:
simp only [b₂, b₄, b₆, variableChange_a₃, variableChange_a₆]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 +
      4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) =
    ↑C.u⁻¹ ^ 6 *
      (W.a₃ ^ 2 + 4 * W.a₆ + 2 * C.r * (2 * W.a₄ + W.a₁ * W.a₃) + C.r ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂) + 4 * C.r ^ 3)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 +
      4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) =
    ↑C.u⁻¹ ^ 6 *
      (W.a₃ ^ 2 + 4 * W.a₆ + 2 * C.r * (2 * W.a₄ + W.a₁ * W.a₃) + C.r ^ 2 * (W.a₁ ^ 2 + 4 * W.a₂) + 4 * C.r ^ 3)

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
lemma cpow_mul_int (x y : ℂ) (n : ℤ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x y : ℂ
n : ℤ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [mul_comm, cpow_int_mul]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_indep_iff' : (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E

Proof state:
α : Type u_1
E I J : Set α
⊢ (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E

Tactic:
rw [uniqueBaseOn, restrict_indep_iff, freeOn_indep_iff, subset_inter_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.map {x y z : P} (h : Wbtw R x y z) (f : P →ᵃ[R] P') : Wbtw R (f x) (f y) (f z)

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ Wbtw R (f x) (f y) (f z)

Tactic:
rw [Wbtw, ← affineSegment_image]

Result:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ f y ∈ ⇑f '' affineSegment R x z

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
h : Wbtw R x y z
f : P →ᵃ[R] P'
⊢ f y ∈ ⇑f '' affineSegment R x z

Tactic:
exact Set.mem_image_of_mem _ h

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem range_cons {α} {n : ℕ} (x : α) (b : Fin n → α) :
    Set.range (Fin.cons x b : Fin n.succ → α) = insert x (Set.range b)

Proof state:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ Set.range (cons x b) = insert x (Set.range b)

Tactic:
rw [range_fin_succ, cons_zero, tail_cons]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerLeft_nil (f : C) {g h : C} (α : g ≅ h) :
    (whiskerLeftIso f α).hom = (whiskerLeftIso f α).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
α : g ≅ h
⊢ (whiskerLeftIso f α).hom = (whiskerLeftIso f α).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem intCast_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) : (a : ZMod b) = 0 ↔ (b : ℤ) ∣ a

Proof state:
a : ℤ
b : ℕ
⊢ ↑a = 0 ↔ ↑b ∣ a

Tactic:
rw [← Int.cast_zero, ZMod.intCast_eq_intCast_iff, Int.modEq_zero_iff_dvd]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
lemma jacobiMatrix_apply (i j : P.rels) :
    P.jacobiMatrix i j = MvPolynomial.pderiv (P.map i) (P.relation j)

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : PreSubmersivePresentation R S
inst✝¹ : Fintype P.rels
inst✝ : DecidableEq P.rels
i j : P.rels
⊢ P.jacobiMatrix i j = (pderiv (P.map i)) (P.relation j)

Tactic:
simp [jacobiMatrix, LinearMap.toMatrix, differential, basis]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_natSucc : {a : ℕ} → {a' c : ℕ} →
    IsNat a a' → Nat.succ a' = c → IsNat (a.succ) c
  | _, _,_, ⟨rfl⟩, rfl => ⟨by simp⟩

Proof state:
n✝ : ℕ
⊢ (↑n✝).succ = ↑n✝.succ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem NormedCommGroup.tendsto_nhds_nhds {f : E → F} {x : E} {y : F} :
    Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x', ‖x' / x‖ < δ → ‖f x' / y‖ < ε

Proof state:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
x : E
y : F
⊢ Tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε

Tactic:
simp_rw [Metric.tendsto_nhds_nhds, dist_eq_norm_div]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuousMul_iInf {ts : ι' → TopologicalSpace M}
    (h' : ∀ i, @ContinuousMul M (ts i) _) : @ContinuousMul M (⨅ i, ts i) _

Proof state:
M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
exact continuousMul_sInf (Set.forall_mem_range.mpr h')

Result:
no goals
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicatorAux_one_of_mem_closure (δ : ℝ) (E : Set α) {x : α}
    (x_mem : x ∈ closure E) : thickenedIndicatorAux δ E x = 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ thickenedIndicatorAux δ E x = 1

Tactic:
rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem star_exp [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (x : 𝔸) :
    star (exp 𝕂 x) = exp 𝕂 (star x)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁷ : Field 𝕂
inst✝⁶ : Ring 𝔸
inst✝⁵ : Algebra 𝕂 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : IsTopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
⊢ star (exp 𝕂 x) = exp 𝕂 (star x)

Tactic:
simp_rw [exp_eq_tsum, ← star_pow, ← star_inv_natCast_smul, ← tsum_star]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_erase_mul [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) :
    (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : a ∈ s
⊢ (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x

Tactic:
rw [mul_comm, mul_prod_erase s f h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
/-- A function has finite integral for the counting measure iff its norm is summable. -/
lemma hasFiniteIntegral_count_iff :
    HasFiniteIntegral f Measure.count ↔ Summable (‖f ·‖)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ HasFiniteIntegral f Measure.count ↔ Summable fun x => ‖f x‖

Tactic:
simp only [hasFiniteIntegral_iff_enorm, enorm, lintegral_count, lt_top_iff_ne_top,
  tsum_coe_ne_top_iff_summable, ← summable_coe, coe_nnnorm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem MemLp.norm {f : α → E} (h : MemLp f p μ) : MemLp (fun x => ‖f x‖) p μ :=
  h.of_le h.aestronglyMeasurable.norm (Eventually.of_forall fun x => by simp)

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
h : MemLp f p μ
x : α
⊢ ‖‖f x‖‖ ≤ ‖f x‖

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma zero_mem_smul_finset_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq β
inst✝³ : Zero β
inst✝² : SMulZeroClass α β
t : Finset β
a : α
inst✝¹ : Zero α
inst✝ : NoZeroSMulDivisors α β
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t

Tactic:
rw [← mem_coe, coe_smul_finset, Set.zero_mem_smul_set_iff ha, mem_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
p : α✝¹ → Option α✝
l : List α✝¹
⊢ findSome? p l = none ↔ ∀ (x : α✝¹), x ∈ l → p x = none

Tactic:
induction l <;> simp [findSome?_cons]

Result:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
p : α✝¹ → Option α✝
head✝ : α✝¹
tail✝ : List α✝¹
tail_ih✝ : findSome? p tail✝ = none ↔ ∀ (x : α✝¹), x ∈ tail✝ → p x = none
⊢ (match p head✝ with
      | some b => some b
      | none => findSome? p tail✝) =
      none ↔
    p head✝ = none ∧ ∀ (a : α✝¹), a ∈ tail✝ → p a = none

Proof state:
case cons
α✝¹ : Type u_1
α✝ : Type u_2
p : α✝¹ → Option α✝
head✝ : α✝¹
tail✝ : List α✝¹
tail_ih✝ : findSome? p tail✝ = none ↔ ∀ (x : α✝¹), x ∈ tail✝ → p x = none
⊢ (match p head✝ with
      | some b => some b
      | none => findSome? p tail✝) =
      none ↔
    p head✝ = none ∧ ∀ (a : α✝¹), a ∈ tail✝ → p a = none

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem stepBound_mono : Monotone stepBound := fun _ _ h =>
  Nat.mul_le_mul h <| Nat.pow_le_pow_of_le_right (by norm_num) h

Proof state:
x✝¹ x✝ : ℕ
h : x✝¹ ≤ x✝
⊢ 4 > 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_right_inj  : ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z

Proof state:
⊢ ∀ {x y z : Bool}, (x != y) = (x != z) ↔ y = z

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.lowerBound?_greatest [@TransCmp α cmp] [IsCut cmp cut] (ht : Ordered cmp t)
    (H : t.lowerBound? cut none = some x) (hy : y ∈ t)
    (xy : cmp x y = .lt) (hx : cut x = .gt) : cut y = .lt :=
  ht.lowerBound?_greatest_lb (by nofun) H hy hx xy

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
H : lowerBound? cut t = some x
hy : y ∈ t
xy : cmp x y = Ordering.lt
hx : cut x = Ordering.gt
⊢ ∀ {x : α}, none = some x → All (fun x_1 => cmpLT cmp x x_1) t

Tactic:
nofun

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem coeff_eval_eq_eval_coeff (s' : Fin n → R) (f : Polynomial (MvPolynomial (Fin n) R))
    (i : ℕ) : Polynomial.coeff (Polynomial.map (eval s') f) i = eval s' (Polynomial.coeff f i)

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
s' : Fin n → R
f : (MvPolynomial (Fin n) R)[X]
i : ℕ
⊢ (Polynomial.map (eval s') f).coeff i = (eval s') (f.coeff i)

Tactic:
simp only [Polynomial.coeff_map]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem foldlm_map (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) :
    foldlm f a (g <$> l) = foldlm (fun x y => f x (g y)) a l

Proof state:
α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : α → γ → m α
a : α
l : t β
⊢ foldlm f a (g <$> l) = foldlm (fun x y => f x (g y)) a l

Tactic:
simp only [foldlm, foldMap_map, Function.comp_def, Function.flip_def]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma antivary_iff_forall_mul_nonpos : Antivary f g ↔ ∀ i j, (f j - f i) * (g j - g i) ≤ 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
⊢ Antivary f g ↔ ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0

Tactic:
simp only [smul_eq_mul, antivary_iff_forall_smul_nonpos]

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem closure_union_closure (x y : α) : l (l x ∪ l y) = l (x ∪ y)

Proof state:
α : Type u_1
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
x y : α
⊢ l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)

Tactic:
rw [closure_union_closure_right, closure_union_closure_left]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
@[reassoc]
lemma tensor_naturality {X Y X' Y' : J} (f : X ⟶ Y) (g : X' ⟶ Y') :
    (F.map f ⊗ G.map g) ≫ (α.app Y ⊗ β.app Y') =
      (α.app X ⊗ β.app X') ≫ (F'.map f ⊗ G'.map g)

Proof state:
J : Type u_1
inst✝² : Category.{u_3, u_1} J
C : Type u_2
inst✝¹ : Category.{u_4, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y X' Y' : J
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (F.map f ⊗ G.map g) ≫ (α.app Y ⊗ β.app Y') = (α.app X ⊗ β.app X') ≫ (F'.map f ⊗ G'.map g)

Tactic:
simp only [← tensor_comp, naturality]

Result:
no goals
-- Mathlib/ModelTheory/Ultraproducts.lean
theorem funMap_cast {n : ℕ} (f : L.Functions n) (x : Fin n → ∀ a, M a) :
    (funMap f fun i => (x i : (u : Filter α).Product M)) =
      (fun a => funMap f fun i => x i a : (u : Filter α).Product M)

Proof state:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝ : (a : α) → L.Structure (M a)
n : ℕ
f : L.Functions n
x : Fin n → (a : α) → M a
⊢ (funMap f fun i => Quotient.mk' (x i)) = Quotient.mk' fun a => funMap f fun i => x i a

Tactic:
apply funMap_quotient_mk'

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem cardQuot_eq_one_iff {P : Submodule R M} : cardQuot P = 1 ↔ P = ⊤ :=
  AddSubgroup.index_eq_one.trans (by simp [SetLike.ext_iff])

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
P : Submodule R M
⊢ P.toAddSubgroup = ⊤ ↔ P = ⊤

Tactic:
simp [SetLike.ext_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₂_of_isCharTwoJEqZeroNF : W.b₂ = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 + 4 * 0 = 0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ W.b₂ = 0

Tactic:
rw [b₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 + 4 * 0 = 0
-- Mathlib/Algebra/Lie/Weights/Killing.lean
@[simp]
lemma coroot_zero [Nontrivial L] : coroot (0 : Weight K H L) = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁸ : LieRing L
inst✝⁷ : Field K
inst✝⁶ : LieAlgebra K L
inst✝⁵ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝⁴ : H.IsCartanSubalgebra
inst✝³ : IsKilling K L
inst✝² : IsTriangularizable K (↥H) L
inst✝¹ : CharZero K
inst✝ : Nontrivial L
⊢ coroot 0 = 0

Tactic:
simp [Weight.isZero_zero]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem mem_split_iff : J ∈ split I i x ↔ ↑J = I.splitLower i x ∨ ↑J = I.splitUpper i x

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ ↑J = I.splitLower i x ∨ ↑J = I.splitUpper i x

Tactic:
simp [split]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertManyIfNewUnit_list_le [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} :
    (insertManyIfNewUnit m l).size ≤ m.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
⊢ (insertManyIfNewUnit m l).size ≤ m.size + l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_list_le

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem NormedCommGroup.tendsto_nhds_one {f : α → E} {l : Filter α} :
    Tendsto f l (𝓝 1) ↔ ∀ ε > 0, ∀ᶠ x in l, ‖f x‖ < ε :=
  Metric.tendsto_nhds.trans <| by simp only [dist_one_right]

Proof state:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, dist (f x) 1 < ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

Tactic:
simp only [dist_one_right]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivAtFilter_const (c : F) (x : E) (L : Filter E) :
    HasFDerivAtFilter (fun _ => c) (0 : E →L[𝕜] F) x L :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun _ => by
    simp only [zero_apply, sub_self, Pi.zero_apply]

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
c : F
x : E
L : Filter E
x✝ : E
⊢ 0 x✝ = c - c - 0 (x✝ - x)

Tactic:
simp only [zero_apply, sub_self, Pi.zero_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_head (x y : α) (xs : List α) (h : Nodup (x :: y :: xs)) :
    formPerm (x :: y :: xs) x = y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
h : (x :: y :: xs).Nodup
⊢ (x :: y :: xs).formPerm x = y

Tactic:
simp [formPerm_apply_of_not_mem h.not_mem]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem quadratic_reciprocity_one_mod_four (hp : p % 4 = 1) (hq : q ≠ 2) :
    legendreSym q p = legendreSym p q

Proof state:
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p % 4 = 1
hq : q ≠ 2
⊢ legendreSym q ↑p = legendreSym p ↑q

Tactic:
rw [quadratic_reciprocity' (Prime.mod_two_eq_one_iff_ne_two.mp (odd_of_mod_four_eq_one hp)) hq,
  pow_mul, neg_one_pow_div_two_of_one_mod_four hp, one_pow, one_mul]

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
theorem add_eq_zero_iff (f g : Π₀ i, α i) : f + g = 0 ↔ f = 0 ∧ g = 0

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
f g : Π₀ (i : ι), α i
⊢ f + g = 0 ↔ f = 0 ∧ g = 0

Tactic:
simp [DFunLike.ext_iff, forall_and]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_inv_of_ne_zero (hq : (q.num : α) ≠ 0) : ↑(q⁻¹) = (q⁻¹ : α)

Proof state:
α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
rw [inv_def', cast_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem iteratedDeriv_cexp_const_mul (n : ℕ) (c : ℂ) :
    (iteratedDeriv n fun s : ℂ => exp (c * s)) = fun s => c ^ n * exp (c * s)

Proof state:
n : ℕ
c : ℂ
⊢ (iteratedDeriv n fun s => cexp (c * s)) = fun s => c ^ n * cexp (c * s)

Tactic:
rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem ofPowerSeries_powerSeriesPart (x : R⸨X⸩) :
    ofPowerSeries ℤ R x.powerSeriesPart = single (-x.order) 1 * x

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart = (single (-order x)) 1 * x

Tactic:
refine Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)

Result:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart =
    (single (-order x)) 1 * ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart)

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ (ofPowerSeries ℤ R) x.powerSeriesPart =
    (single (-order x)) 1 * ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart)

Tactic:
rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp] lemma disjiUnion_empty (t : α → Finset β) : disjiUnion ∅ t (by simp) = ∅ := rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
⊢ (↑∅).PairwiseDisjoint t

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
lemma evaluation_naturality_apply {V : Opens Y} (x : (Opens.map f.base).obj V)
    (a : Y.presheaf.obj (op V)) :
    residueFieldMap f x.val (Y.evaluation ⟨f.base x, x.property⟩ a) =
      X.evaluation x (f.c.app (op V) a)

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (ConcreteCategory.hom (residueFieldMap f ↑x))
      ((ConcreteCategory.hom (Y.evaluation ⟨(ConcreteCategory.hom f.base) ↑x, ⋯⟩)) a) =
    (ConcreteCategory.hom (X.evaluation x)) ((ConcreteCategory.hom (f.c.app (op V))) a)

Tactic:
simpa using congrFun (congrArg (DFunLike.coe ∘ CommRingCat.Hom.hom) <|
  evaluation_naturality f x) a

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropPrefix?_nil [BEq α] {p : List α} : dropPrefix? p [] = some p

Proof state:
α : Type u_1
inst✝ : BEq α
p : List α
⊢ p.dropPrefix? [] = some p

Tactic:
simp [dropPrefix?]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Defs.lean
lemma subtype_injective :
    Function.Injective (SubsemiringClass.subtype s) := fun _ ↦ by
  simp

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : SetLike S R
hSR : SubsemiringClass S R
s : S
x✝ : ↥s
⊢ ∀ ⦃a₂ : ↥s⦄, (subtype s) x✝ = (subtype s) a₂ → x✝ = a₂

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_one_isSolvable : IsSolvable (1 : F[X]).Gal

Proof state:
F : Type u_1
inst✝ : Field F
⊢ IsSolvable (Gal 1)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullbackIsoProdSubtype_inv_snd (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullbackIsoProdSubtype f g).inv ≫ pullback.snd _ _ = pullbackSnd f g

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.snd f g = pullbackSnd f g

Tactic:
simp [pullbackCone, pullbackIsoProdSubtype]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma scalarRTensor_apply_X_tmul_apply (s : σ) (n : N) (d : σ →₀ ℕ) :
    scalarRTensor (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then n else 0

Proof state:
R : Type u
N : Type v
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : DecidableEq σ
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : σ
n : N
d : σ →₀ ℕ
⊢ (scalarRTensor (X s ⊗ₜ[R] n)) d = if Finsupp.single s 1 = d then n else 0

Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma free_μ_freeMk_tmul_freeMk {X Y : Type u} (x : X) (y : Y) :
    μ (free R) _ _ (freeMk x ⊗ₜ freeMk y) = freeMk ⟨x, y⟩

Proof state:
R : Type u
inst✝ : CommRing R
X Y : Type u
x : X
y : Y
⊢ (ConcreteCategory.hom (μ (free R) X Y)) (freeMk x ⊗ₜ[R] freeMk y) = freeMk (x, y)

Tactic:
apply FreeMonoidal.μIso_hom_freeMk_tmul_freeMk

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.one_le_iff (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.856162) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
⊢ 1 ≤ a ↔ ∀ x ∈ spectrum R a, 1 ≤ x

Tactic:
simpa using algebraMap_le_iff_le_spectrum (r := (1 : R)) (a := a)

Result:
no goals
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
lemma totallyDisconnectedSpace_subtype_iff {s : Set α} :
    TotallyDisconnectedSpace s ↔ IsTotallyDisconnected s

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s

Tactic:
rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]

Result:
no goals