harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem take_modify (f : α → α) (n m) (l : List α) :
    (modify f m l).take n = (take n l).modify f m

Proof state:
case succ.cons.succ
α : Type u_1
f : α → α
n : Nat
ih : ∀ (m : Nat) (l : List α), take n (modify f m l) = modify f m (take n l)
hd : α
tl : List α
m : Nat
⊢ take (n + 1) (modify f (m + 1) (hd :: tl)) = modify f (m + 1) (take (n + 1) (hd :: tl))

Tactic:
simp [ih]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n m : Nat
l : List α
⊢ take n (modify f m l) = modify f m (take n l)

Tactic:
induction n generalizing l m with
| zero => simp
| succ n ih =>
  cases l with
  | nil => simp
  | cons hd tl =>
    cases m with
    | zero => simp
    | succ m => simp [ih]

Result:
no goals

Proof state:
case succ.cons.zero
α : Type u_1
f : α → α
n : Nat
ih : ∀ (m : Nat) (l : List α), take n (modify f m l) = modify f m (take n l)
hd : α
tl : List α
⊢ take (n + 1) (modify f 0 (hd :: tl)) = modify f 0 (take (n + 1) (hd :: tl))

Tactic:
simp

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
f : α → α
n : Nat
ih : ∀ (m : Nat) (l : List α), take n (modify f m l) = modify f m (take n l)
m : Nat
hd : α
tl : List α
⊢ take (n + 1) (modify f m (hd :: tl)) = modify f m (take (n + 1) (hd :: tl))

Tactic:
cases m with
| zero => simp
| succ m => simp [ih]

Result:
no goals

Proof state:
case succ.nil
α : Type u_1
f : α → α
n : Nat
ih : ∀ (m : Nat) (l : List α), take n (modify f m l) = modify f m (take n l)
m : Nat
⊢ take (n + 1) (modify f m []) = modify f m (take (n + 1) [])

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
f : α → α
n : Nat
ih : ∀ (m : Nat) (l : List α), take n (modify f m l) = modify f m (take n l)
m : Nat
l : List α
⊢ take (n + 1) (modify f m l) = modify f m (take (n + 1) l)

Tactic:
cases l with
| nil => simp
| cons hd tl =>
  cases m with
  | zero => simp
  | succ m => simp [ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
f : α → α
m : Nat
l : List α
⊢ take 0 (modify f m l) = modify f m (take 0 l)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_pow (f : ι → α) (n : ℕ) : (∑ a, f a) ^ n = ∑ p : Fin n → ι, ∏ i, f (p i)

Proof state:
ι : Type u_7
α : Type u_9
inst✝¹ : Fintype ι
inst✝ : CommSemiring α
f : ι → α
n : ℕ
⊢ (∑ a : ι, f a) ^ n = ∑ p : Fin n → ι, ∏ i : Fin n, f (p i)

Tactic:
simp [sum_pow']

Result:
no goals
-- Mathlib/Order/Defs/Unbundled.lean
theorem rel_congr [IsSymm α r] [IsTrans α r] {a b c d : α} (h₁ : r a b) (h₂ : r c d) :
    r a c ↔ r b d

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
⊢ r a c ↔ r b d

Tactic:
rw [rel_congr_left h₁, rel_congr_right h₂]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem mul_self_inj_of_nonneg (a0 : 0 ≤ a) (b0 : 0 ≤ b) : a * a = b * b ↔ a = b :=
  mul_self_eq_mul_self_iff.trans <|
    or_iff_left_of_imp fun h => by
      subst a
      have : b = 0 := le_antisymm (neg_nonneg.1 a0) b0
      rw [this, neg_zero]

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
b : α
b0 : 0 ≤ b
a0 : 0 ≤ -b
this : b = 0
⊢ -b = b

Tactic:
rw [this, neg_zero]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
h : a = -b
⊢ a = b

Tactic:
subst a

Result:
α : Type u_2
inst✝ : LinearOrderedField α
b : α
b0 : 0 ≤ b
a0 : 0 ≤ -b
⊢ -b = b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
b : α
b0 : 0 ≤ b
a0 : 0 ≤ -b
⊢ -b = b

Tactic:
have : b = 0 := le_antisymm (neg_nonneg.1 a0) b0

Result:
α : Type u_2
inst✝ : LinearOrderedField α
b : α
b0 : 0 ≤ b
a0 : 0 ≤ -b
this : b = 0
⊢ -b = b
-- Mathlib/Algebra/Module/Defs.lean
theorem Module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
zero_eq_one : 0 = 1
⊢ x = 0

Tactic:
rw [← one_smul R x, ← zero_eq_one, zero_smul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_one (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 1 = a

Tactic:
simp only [rpow_def, NNReal.coe_one, NNReal.rpow_eq_pow, NNReal.rpow_one, cfc_id' ℝ≥0 a]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_conj (z : ℂ) : normSq (conj z) = normSq z

Proof state:
z : ℂ
⊢ normSq ((starRingEnd ℂ) z) = normSq z

Tactic:
simp [normSq]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem col_smul [SMul R α] (x : R) (v : m → α) : col ι (x • v) = x • col ι v

Proof state:
case a
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : m
j✝ : ι
⊢ col ι (x • v) i✝ j✝ = (x • col ι v) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
⊢ col ι (x • v) = x • col ι v

Tactic:
ext

Result:
case a
m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : m
j✝ : ι
⊢ col ι (x • v) i✝ j✝ = (x • col ι v) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
    k' ∈ Const.alter m k f ↔ if k == k' then (f (Const.get? m k)).isSome = true else k' ∈ m

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
⊢ k' ∈ alter m k f ↔ if (k == k') = true then (f (get? m k)).isSome = true else k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter, Bool.ite_eq_true_distrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_updateBucket_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} :
    Perm (toListModel (updateBucket m.1.buckets m.2 a (AssocList.alter a f)))
      (alterKey a f (toListModel m.1.buckets))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel (updateBucket m.val.buckets ⋯ a (AssocList.alter a f)) ~ alterKey a f (toListModel m.val.buckets)

Tactic:
exact toListModel_updateBucket h AssocList.toList_alter List.alterKey_of_perm
  List.alterKey_append_of_containsKey_right_eq_false

Result:
no goals
-- Mathlib/Data/Bundle.lean
theorem TotalSpace.mk_inj {b : B} {y y' : E b} : mk' F b y = mk' F b y' ↔ y = y'

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
y y' : E b
⊢ mk' F b y = mk' F b y' ↔ y = y'

Tactic:
simp [TotalSpace.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).size ≤ m.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insertIfNew k v).size ≤ m.size + 1

Tactic:
simp_to_raw using Raw₀.size_insertIfNew_le

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem add_tsub_cancel_of_le (h : a ≤ b) : a + (b - a) = b

Proof state:
case intro
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : a ≤ a + c
⊢ a + (a + c - a) ≤ a + c

Tactic:
exact add_le_add_left add_tsub_le_left a

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) ≤ b

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le h

Result:
case intro
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c : α
h : a ≤ a + c
⊢ a + (a + c - a) ≤ a + c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
refine le_antisymm ?_ le_add_tsub

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a + (b - a) ≤ b
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem hasGenEigenvalue_iff_hasEigenvalue {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) :
    f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ :=
  hasUnifEigenvalue_iff_hasUnifEigenvalue_one <| by simpa using hk

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ 0 < ↑k

Tactic:
simpa using hk

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem coeToSubmodule_eq_bot {I : FractionalIdeal S P} : (I : Submodule R P) = ⊥ ↔ I = 0 :=
  ⟨fun h => coeToSubmodule_injective (by simp [h]), fun h => by simp [h]⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
h : ↑I = ⊥
⊢ (fun I => ↑I) I = (fun I => ↑I) 0

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
h : I = 0
⊢ ↑I = ⊥

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma injective_ringHomComp {f : R' →+* R''} (hf : Function.Injective f) :
    Function.Injective (ringHomComp (R := R) · f)

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
f : R' →+* R''
hf : Function.Injective ⇑f
⊢ Function.Injective fun x => x.ringHomComp f

Tactic:
simpa
  only [Function.Injective, MulChar.ext_iff, ringHomComp, coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
  using fun χ χ' h a ↦ hf (h a)

Result:
no goals
-- Mathlib/Algebra/Module/Projective.lean
theorem Projective.of_equiv [Module.Projective R M]
    (e : M ≃ₗ[R] P) : Module.Projective R P :=
  Projective.of_split e.symm e.toLinearMap (by ext; simp)

Proof state:
case h
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
e : M ≃ₗ[R] P
x✝ : P
⊢ (↑e ∘ₗ ↑e.symm) x✝ = LinearMap.id x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
e : M ≃ₗ[R] P
⊢ ↑e ∘ₗ ↑e.symm = LinearMap.id

Tactic:
ext

Result:
case h
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
e : M ≃ₗ[R] P
x✝ : P
⊢ (↑e ∘ₗ ↑e.symm) x✝ = LinearMap.id x✝
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotient_map_comp_mkₐ (f : A →ₐ[R₁] B) (H : I ≤ J.comap f) :
    (quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I) = (Quotient.mkₐ R₁ J).comp f :=
  AlgHom.ext fun x => by simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]

Proof state:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R₁
inst✝⁵ : Ring A
inst✝⁴ : Algebra R₁ A
inst✝³ : Ring B
inst✝² : Algebra R₁ B
I : Ideal A
J : Ideal B
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : A →ₐ[R₁] B
H : I ≤ comap f J
x : A
⊢ ((quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I)) x = ((Quotient.mkₐ R₁ J).comp f) x

Tactic:
simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropAt_iff {P : (H → H') → Set H → H → Prop} {f : M → M'} {x : M} :
    LiftPropAt P f x ↔
      ContinuousAt f x ∧ P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) univ (chartAt H x x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
f : M → M'
x : M
⊢ LiftPropAt P f x ↔ ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x)

Tactic:
rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]

Result:
no goals
-- Mathlib/Probability/Distributions/Pareto.lean
/-- The Lebesgue integral of the Pareto pdf over reals `≤ t` equals `0`. -/
lemma lintegral_paretoPDF_of_le (hx : x ≤ t) :
    ∫⁻ y in Iio x, paretoPDF t r y = 0

Proof state:
case h
t r x : ℝ
hx : x ≤ t
a : ℝ
x✝ : a < x
⊢ (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0

Tactic:
rw [if_neg (by linarith)]

Result:
no goals

Proof state:
t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

Tactic:
rw [lintegral_zero, ← ENNReal.ofReal_zero]

Result:
no goals

Proof state:
t r x : ℝ
hx : x ≤ t
a : ℝ
x✝ : a < x
⊢ ¬t ≤ a

Tactic:
linarith

Result:
no goals

Proof state:
t r x : ℝ
hx : x ≤ t
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → paretoPDF t r x_1 = 0

Tactic:
simp only [paretoPDF_eq, ge_iff_le, ENNReal.ofReal_eq_zero]

Result:
t r x : ℝ
hx : x ≤ t
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → (if t ≤ x_1 then r * t ^ r * x_1 ^ (-(r + 1)) else 0) ≤ 0

Proof state:
t r x : ℝ
hx : x ≤ t
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → (if t ≤ x_1 then r * t ^ r * x_1 ^ (-(r + 1)) else 0) ≤ 0

Tactic:
filter_upwards with a (_ : a < _)

Result:
case h
t r x : ℝ
hx : x ≤ t
a : ℝ
x✝ : a < x
⊢ (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0

Proof state:
t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (y : ℝ) in Iio x, paretoPDF t r y = 0

Tactic:
rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]

Result:
t r x : ℝ
hx : x ≤ t
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

t r x : ℝ
hx : x ≤ t
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iio x → paretoPDF t r x_1 = 0
-- Mathlib/Data/Finset/Option.lean
theorem mem_eraseNone {s : Finset (Option α)} {x : α} : x ∈ eraseNone s ↔ some x ∈ s

Proof state:
α : Type u_1
s : Finset (Option α)
x : α
⊢ x ∈ eraseNone s ↔ some x ∈ s

Tactic:
simp [eraseNone]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem _root_.Prod.fst_zmod_cast (a : ZMod n) : (cast a : R × S).fst = cast a

Proof state:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast

Tactic:
rfl

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast

Tactic:
simp [ZMod.cast]

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.1 = a.cast

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.1 = a.cast

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.1 = a.cast
-- Mathlib/Analysis/LocallyConvex/Basic.lean
theorem balanced_iff_neg_mem (hs : Convex ℝ s) : Balanced ℝ s ↔ ∀ ⦃x⦄, x ∈ s → -x ∈ s

Proof state:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s

Tactic:
refine ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => ?_⟩

Result:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s

Proof state:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a = -((1 - a) / 2) + (a - -1) / 2

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s

Tactic:
rw [Real.norm_eq_abs, abs_le] at ha

Result:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s

Proof state:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (1 - a) / 2 + (a - -1) / 2 = 1

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s

Tactic:
rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]

Result:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s

Proof state:
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s

Tactic:
exact hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two)
  (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two) (by ring)

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
lemma apply_congr_of_mem_measurableAtom (κ : Kernel α β) {y' y : α} (hy' : y' ∈ measurableAtom y) :
    κ y' = κ y

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
s : Set β
hs : MeasurableSet s
⊢ (κ y') s = (κ y) s

Tactic:
exact mem_of_mem_measurableAtom hy' (κ.measurable_coe hs (measurableSet_singleton (κ y s))) rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
⊢ κ y' = κ y

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
y' y : α
hy' : y' ∈ measurableAtom y
s : Set β
hs : MeasurableSet s
⊢ (κ y') s = (κ y) s
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsPerfectMatching.isAlternating_symmDiff_right
    {M' : Subgraph G'} (hM : M.IsPerfectMatching) (hM' : M'.IsPerfectMatching) :
    (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M'.spanningCoe

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M'.spanningCoe

Tactic:
simpa [symmDiff_comm] using isAlternating_symmDiff_left hM' hM

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
@[reassoc (attr := simp)]
lemma affineTargetImageFactorization_comp :
    affineTargetImageFactorization f ≫ affineTargetImageInclusion f = f

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ affineTargetImageFactorization f ≫ affineTargetImageInclusion f = f

Tactic:
simp [affineTargetImageFactorization, affineTargetImageInclusion]

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem transpose_neg [Neg α] (M : Matrix m n α) : (-M)ᵀ = -Mᵀ

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Neg α
M : Matrix m n α
i✝ : n
j✝ : m
⊢ (-M)ᵀ i✝ j✝ = (-Mᵀ) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Neg α
M : Matrix m n α
⊢ (-M)ᵀ = -Mᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Neg α
M : Matrix m n α
i✝ : n
j✝ : m
⊢ (-M)ᵀ i✝ j✝ = (-Mᵀ) i✝ j✝
-- Mathlib/Control/Fold.lean
theorem foldr_toList (f : α → β → β) (xs : t α) (x : β) :
    foldr f x xs = List.foldr f x (toList xs)

Proof state:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = (Foldr.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x

Tactic:
rw [toList_spec, foldr, Foldr.get, FreeMonoid.ofList_toList, foldMap_hom_free,
  foldr.ofFreeMonoid_comp_of]

Result:
no goals

Proof state:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = List.foldr f x (toList xs)

Tactic:
change _ = Foldr.ofFreeMonoid _ (FreeMonoid.ofList <| toList xs) _

Result:
α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β → β
xs : t α
x : β
⊢ foldr f x xs = (Foldr.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x
-- Mathlib/Data/Finset/Interval.lean
theorem card_Ico_finset (h : s ⊆ t) : (Ico s t).card = 2 ^ (t.card - s.card) - 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ico s t) = 2 ^ (#t - #s) - 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc_finset h]

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
theorem eventually_smallSets_eventually {p : α → Prop} :
    (∀ᶠ s in l.smallSets, ∀ᶠ x in l', x ∈ s → p x) ↔ ∀ᶠ x in l ⊓ l', p x :=
  calc
    _ ↔ ∃ s ∈ l, ∀ᶠ x in l', x ∈ s → p x :=
      eventually_smallSets' fun _ _ hst ht => ht.mono fun _ hx hs => hx (hst hs)
    _ ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x, x ∈ t → x ∈ s → p x

Proof state:
α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x

Tactic:
simp only [eventually_iff_exists_mem]

Result:
no goals

Proof state:
α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x

Tactic:
simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem mapAlgHom_eq_eval₂AlgHom'_CAlgHom (f : A →ₐ[R] B) : mapAlgHom f = eval₂AlgHom'
    (CAlgHom.comp f) X (fun a => (commute_X (C (f a))).symm)

Proof state:
case H
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (x : A[X]), (mapAlgHom f) x = (eval₂AlgHom' (CAlgHom.comp f) X ⋯) x

Tactic:
intro x

Result:
case H
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A[X]
⊢ (mapAlgHom f) x = (eval₂AlgHom' (CAlgHom.comp f) X ⋯) x

Proof state:
case H
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
x : A[X]
⊢ (mapAlgHom f) x = (eval₂AlgHom' (CAlgHom.comp f) X ⋯) x

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ mapAlgHom f = eval₂AlgHom' (CAlgHom.comp f) X ⋯

Tactic:
apply AlgHom.ext

Result:
case H
R : Type u
A : Type z
B : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ ∀ (x : A[X]), (mapAlgHom f) x = (eval₂AlgHom' (CAlgHom.comp f) X ⋯) x
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem findP?_some [@TransCmp α cmp] [IsStrictCut cmp cut] {t : RBSet α cmp} :
    t.findP? cut = some y ↔ y ∈ toList t ∧ cut y = .eq :=
  t.2.out.1.find?_some.trans <| by simp [mem_toList]

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
t : RBSet α cmp
⊢ y ∈ t.val ∧ cut y = Ordering.eq ↔ y ∈ t.toList ∧ cut y = Ordering.eq

Tactic:
simp [mem_toList]

Result:
no goals