harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Adjoin/PowerBasis.lean
theorem repr_mul_isIntegral (hB : IsIntegral R B.gen) [IsDomain S] {x y : A}
    (hx : ∀ i, IsIntegral R (B.basis.repr x i)) (hy : ∀ i, IsIntegral R (B.basis.repr y i))
    (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) :
    ∀ i, IsIntegral R (B.basis.repr (x * y) i)

Proof state:
S : Type u_2
inst✝⁷ : CommRing S
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
inst✝ : IsDomain S
x y : A
hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)
hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)
hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)
i : Fin B.dim
I : Fin B.dim × Fin B.dim
x✝ : I ∈ Finset.univ ×ˢ Finset.univ
⊢ IsIntegral R ((B.basis.repr (B.gen ^ (↑I.1 + ↑I.2))) i)

Tactic:
exact repr_gen_pow_isIntegral hB hmin _ _

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_mapRange {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
    (mapRange f hf g).support ⊆ g.support

Proof state:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β₁ i)
inst✝² : (i : ι) → Zero (β₂ i)
inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ (mapRange f hf g).support ⊆ g.support

Tactic:
simp [mapRange_def]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
/-- The difference from `quasispectrumRestricts_iff_spectrumRestricts_inr` is that the
`Unitization` may be taken with respect to a different scalar field. -/
lemma quasispectrumRestricts_iff_spectrumRestricts_inr'
    {R S' A : Type*} (S : Type*) [Semifield R] [Semifield S'] [Field S] [NonUnitalRing A]
    [Module R A] [Module S' A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A]
    [Algebra R S'] [Algebra S' S] [Algebra R S] [IsScalarTower S' S A] [IsScalarTower R S A]
    {a : A} {f : S' → R} :
    QuasispectrumRestricts a f ↔ SpectrumRestricts (a : Unitization S A) f

Proof state:
R : Type u_3
S' : Type u_4
A : Type u_5
S : Type u_6
inst✝¹³ : Semifield R
inst✝¹² : Semifield S'
inst✝¹¹ : Field S
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : Module R A
inst✝⁸ : Module S' A
inst✝⁷ : Module S A
inst✝⁶ : IsScalarTower S A A
inst✝⁵ : SMulCommClass S A A
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower S' S A
inst✝ : IsScalarTower R S A
a : A
f : S' → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

Tactic:
simp only [quasispectrumRestricts_iff, SpectrumRestricts, Unitization.quasispectrum_inr_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem hasLineDerivAt_zero : HasLineDerivAt 𝕜 f 0 x 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x : E
⊢ HasLineDerivAt 𝕜 f 0 x 0

Tactic:
simp [HasLineDerivAt, hasDerivAt_const]

Result:
no goals
-- Mathlib/Algebra/Order/Pi.lean
@[to_additive (attr := simp)]
lemma mulSingle_le_mulSingle : mulSingle i a ≤ mulSingle i b ↔ a ≤ b

Proof state:
ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
⊢ mulSingle i a ≤ mulSingle i b ↔ a ≤ b

Tactic:
simp [mulSingle, update_le_update_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftUnshift_leftShift (a n' : ℤ) (hn' : n + a = n') :
    (γ.leftShift a n' hn').leftUnshift n hn' = γ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (γ.leftShift a n' hn').leftUnshift n hn' = γ

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ q - n' + n' = q

Tactic:
omega

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq

Tactic:
rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q-n') (by omega),
  γ.leftShift_v a n' hn' (q-n') q (by omega) p hpq, Linear.comp_units_smul,
  Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, one_smul]

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem iterate_le_of_map_le (h : Commute f g) (hf : Monotone f) (hg : Monotone g) {x}
    (hx : f x ≤ g x) (n : ℕ) : f^[n] x ≤ g^[n] x

Proof state:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) ≤ g^[k✝ + 1] x

Tactic:
simp [h.iterate_right _ _, hg.iterate _ hx]

Result:
no goals

Proof state:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x

Tactic:
intros

Result:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) ≤ g^[k✝ + 1] x

Proof state:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Tactic:
rw [iterate_succ_apply']

Result:
no goals

Proof state:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x

Tactic:
rfl

Result:
no goals

Proof state:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

Tactic:
intros

Result:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Proof state:
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x

Tactic:
apply hf.seq_le_seq n

Result:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x

case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem finite_neighborSet_toSubgraph (p : G.Walk u v) : (p.toSubgraph.neighborSet w).Finite

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w).Finite

Tactic:
refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)

Result:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ {u✝, v✝}.Finite

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((cons ha p✝).toSubgraph.neighborSet w).Finite

Tactic:
rw [Walk.toSubgraph, Subgraph.neighborSet_sup]

Result:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w ∪ p✝.toSubgraph.neighborSet w).Finite

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ (nil.toSubgraph.neighborSet w).Finite

Tactic:
rw [Walk.toSubgraph, neighborSet_singletonSubgraph]

Result:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ ∅.Finite

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ ∅.Finite

Tactic:
apply Set.toFinite

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w ∪ p✝.toSubgraph.neighborSet w).Finite

Tactic:
refine Set.Finite.union ?_ ih

Result:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ ((G.subgraphOfAdj ha).neighborSet w).Finite

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
⊢ (p.toSubgraph.neighborSet w).Finite

Tactic:
induction p with
| nil =>
  rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
  apply Set.toFinite
| cons ha _ ih =>
  rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
  refine Set.Finite.union ?_ ih
  refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
  apply Set.toFinite

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
ha : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : (p✝.toSubgraph.neighborSet w).Finite
⊢ {u✝, v✝}.Finite

Tactic:
apply Set.toFinite

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : Eq.rec (motive := fun α _ => α) a h₁ = b) : HEq a b

Proof state:
case h
α : Sort u
a b : α
h₂ : Eq.rec a ⋯ = b
⊢ a = b

Tactic:
exact h₂

Result:
no goals

Proof state:
α β : Sort u
a : α
b : β
h₁ : α = β
h₂ : Eq.rec a h₁ = b
⊢ HEq a b

Tactic:
subst h₁

Result:
α : Sort u
a b : α
h₂ : Eq.rec a ⋯ = b
⊢ HEq a b

Proof state:
α : Sort u
a b : α
h₂ : Eq.rec a ⋯ = b
⊢ HEq a b

Tactic:
apply heq_of_eq

Result:
case h
α : Sort u
a b : α
h₂ : Eq.rec a ⋯ = b
⊢ a = b
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDeriv_comp_add_right (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a x : E
⊢ iteratedFDeriv 𝕜 n (fun z => f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a)

Tactic:
simp [iteratedFDeriv_comp_add_right']

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorAdd_hom_app_f (K : CochainComplex C ℤ) (a b n : ℤ) :
    ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [add_comm a, add_assoc])).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)

Tactic:
rw [shiftFunctorAdd_inv_app_f]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ IsIso (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
this : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)
⊢ 𝟙 (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) (a + b)).obj K).X n) = (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom

Tactic:
simp only [XIsoOfEq, eqToIso.hom, eqToHom_trans, eqToHom_refl]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
this : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)
⊢ ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
rw [← cancel_mono (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n),
  ← comp_f, Iso.hom_inv_id_app, id_f, shiftFunctorAdd_inv_app_f]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
this : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)
⊢ 𝟙 (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) (a + b)).obj K).X n) = (XIsoOfEq K ⋯).hom ≫ (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ IsIso (XIsoOfEq K ⋯).hom

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + { as := a + b }.as = n + { as := b }.as + { as := a }.as

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + (a + b) = n + b + a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
have : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n) := by
  rw [shiftFunctorAdd_inv_app_f]
  infer_instance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
this : IsIso (((shiftFunctorAdd (CochainComplex C ℤ) a b).inv.app K).f n)
⊢ ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b n : ℤ
⊢ n + (a + b) = n + b + a

Tactic:
rw [add_comm a, add_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/HaarToSphere.lean
theorem toSphere_apply_aux (s : Set (sphere (0 : E) 1)) (r : Ioi (0 : ℝ)) :
    μ ((↑) '' (homeomorphUnitSphereProd E ⁻¹' s ×ˢ Iio r)) = μ (Ioo (0 : ℝ) r • ((↑) '' s))

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ ((fun x => ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) = μ ((fun x => SMul.smul ↑x.2 ↑x.1) '' s ×ˢ Iio r)

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ (Subtype.val '' (⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r)) = μ (Ioo 0 ↑r • Subtype.val '' s)

Tactic:
rw [← image2_smul, image2_image_right, ← Homeomorph.image_symm, image_image,
  ← image_subtype_val_Ioi_Iio, image2_image_left, image2_swap, ← image_prod]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ ((fun x => ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) = μ ((fun x => SMul.smul ↑x.2 ↑x.1) '' s ×ˢ Iio r)
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_inj {z w : ℝ} : (z : ℂ) = w ↔ z = w :=
  ⟨congrArg re, by apply congrArg⟩

Proof state:
z w : ℝ
⊢ z = w → ↑z = ↑w

Tactic:
apply congrArg

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem le_span_singleton_mul_iff {x : R} {I J : Ideal R} :
    I ≤ span {x} * J ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI :=
  show (∀ {zI} (_ : zI ∈ I), zI ∈ span {x} * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI by
    simp only [mem_span_singleton_mul]

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ (∀ {zI : R}, zI ∈ I → zI ∈ span {x} * J) ↔ ∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI

Tactic:
simp only [mem_span_singleton_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
    rev i = ⟨a, Nat.lt_succ_of_le (h ▸ Nat.le_add_right ..)⟩

Proof state:
case h
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ a + ↑i + 1 - (↑i + 1) = a

Tactic:
rw [Nat.add_assoc, Nat.add_sub_cancel]

Result:
no goals

Proof state:
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ i.rev = ⟨a, ⋯⟩

Tactic:
ext

Result:
case h
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑i.rev = ↑⟨a, ⋯⟩

Proof state:
case h
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ ↑i.rev = ↑⟨a, ⋯⟩

Tactic:
dsimp

Result:
case h
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ n + 1 - (↑i + 1) = a

Proof state:
case h
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ n + 1 - (↑i + 1) = a

Tactic:
conv => lhs; congr; rw [h]

Result:
case h
n a : Nat
i : Fin (n + 1)
h : n = a + ↑i
⊢ a + ↑i + 1 - (↑i + 1) = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tail else l.tail ++ l'

Proof state:
α : Type u_1
l l' : List α
⊢ (l ++ l').tail = if l.isEmpty = true then l'.tail else l.tail ++ l'

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insertMany_list_of_mem [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h'} :
    (m.insertMany l).get k' h' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : k' ∈ m.insertMany l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : k' ∈ m.insertMany l
⊢ (m.insertMany l).get k' h' = cast ⋯ v

Tactic:
simp_to_raw using Raw₀.get_insertMany_list_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : k' ∈ m.insertMany l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h' : k' ∈ m.insertMany l
⊢ k = k'
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.Nonempty.ciSup_eq_max'_image {s : Finset ι} (h : s.Nonempty)
    (h' : (s.image f).Nonempty := h.image f) :
    ⨆ i ∈ s, f i = (s.image f).max' h' :=
  s.ciSup_eq_max'_image _ (h.imp (by simp)) _

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
s : Finset ι
h : s.Nonempty
h' : optParam (image f s).Nonempty ⋯
⊢ ∀ a ∈ s, a ∈ s ∧ sSup ∅ ≤ f a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_eq_zero (hi : i ∈ s) (h : f i = 0) : ∏ j ∈ s, f j = 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ ∏ j ∈ s, f j = 0

Tactic:
rw [← prod_erase_mul _ _ hi, h, mul_zero]

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
i : ι
hi : i ∈ s
h : f i = 0
⊢ ∏ j ∈ s, f j = 0

Tactic:
classical rw [← prod_erase_mul _ _ hi, h, mul_zero]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- Embedding `Fin n` into `Fin (n + 1)` with a hole around `last n` embeds by `castSucc`. -/
@[simp] lemma succAbove_last : succAbove (last n) = castSucc

Proof state:
case h.h
n : ℕ
x✝ : Fin n
⊢ ↑((last n).succAbove x✝) = ↑x✝.castSucc

Tactic:
simp only [succAbove_of_castSucc_lt, castSucc_lt_last]

Result:
no goals

Proof state:
n : ℕ
⊢ (last n).succAbove = castSucc

Tactic:
ext

Result:
case h.h
n : ℕ
x✝ : Fin n
⊢ ↑((last n).succAbove x✝) = ↑x✝.castSucc
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_multiset_of_infinite (α : Type u) [Infinite α] : #(Multiset α) = #α

Proof state:
α : Type u
inst✝ : Infinite α
⊢ #(Multiset α) = #α

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem le_def {x y : PGame} :
    x ≤ y ↔
      (∀ i, (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧
        ∀ j, (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j

Proof state:
x y : PGame
⊢ ((∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j) ↔
    (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧
      ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j

Tactic:
conv =>
  lhs
  simp only [lf_iff_exists_le]

Result:
no goals

Proof state:
x y : PGame
⊢ x ≤ y ↔
    (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧
      ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j

Tactic:
rw [le_iff_forall_lf]

Result:
x y : PGame
⊢ ((∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j) ↔
    (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧
      ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sub : cos (x - y) = cos x * cos y + sin x * sin y

Proof state:
x y : ℝ
⊢ cos (x - y) = cos x * cos y + sin x * sin y

Tactic:
simp [sub_eq_add_neg, cos_add, sin_neg, cos_neg]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem monotoneOn_deriv (hfc : ConvexOn ℝ S f) (hfd : ∀ x ∈ S, DifferentiableAt ℝ f x) :
    MonotoneOn (deriv f) S

Proof state:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ deriv f x ≤ deriv f x

Tactic:
rfl

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
⊢ MonotoneOn (deriv f) S

Tactic:
intro x hx y hy hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ deriv f x ≤ deriv f y

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
⊢ deriv f x ≤ deriv f y

Tactic:
rcases eq_or_lt_of_le hxy with rfl | hxy'

Result:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ deriv f x ≤ deriv f x

case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ deriv f x ≤ deriv f y

Proof state:
case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ deriv f x ≤ deriv f y

Tactic:
exact (hfc.deriv_le_slope hx hy hxy' (hfd x hx)).trans (hfc.slope_le_deriv hx hy hxy' (hfd y hy))

Result:
no goals