harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_biSup {ι : Type*} (s : Finset ι) (N : ι → Submodule R M) (h : ∀ i ∈ s, (N i).FG) :
    (⨆ i ∈ s, N i).FG

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Finset ι
N : ι → Submodule R M
h : ∀ i ∈ s, (N i).FG
⊢ (⨆ i ∈ s, N i).FG

Tactic:
simpa only [Finset.sup_eq_iSup] using fg_finset_sup s N h

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean
theorem of_iso {P Q : C} (i : P ≅ Q) (_ : Projective P) : Projective Q where
  factors f e _ :=
    let ⟨f', hf'⟩ := Projective.factors (i.hom ≫ f) e
    ⟨i.inv ≫ f', by simp [hf']⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P Q : C
i : P ≅ Q
x✝¹ : Projective P
E✝ X✝ : C
f : Q ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
f' : P ⟶ E✝
hf' : f' ≫ e = i.hom ≫ f
⊢ (i.inv ≫ f') ≫ e = f

Tactic:
simp [hf']

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma mul_klFun_le_toReal_klDiv (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal) ≤ (klDiv μ ν).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_klFun_rnDeriv_iff hμν]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal

Tactic:
rw [toReal_klDiv_eq_integral_klFun hμν]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal) ≤ (klDiv μ ν).toReal

Tactic:
calc (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal)
_ ≤ ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν := by
  refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν
  rwa [integrable_klFun_rnDeriv_iff hμν]
_ = (klDiv μ ν).toReal := by rw [toReal_klDiv_eq_integral_klFun hμν]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => klFun (μ.rnDeriv ν x).toReal) ν
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesCoimage.iso_inv_π :
    Abelian.coimage.π (F.map f) ≫ (PreservesCoimage.iso F f).inv = F.map (Abelian.coimage.π f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ coimage.π (F.map f) ≫ (iso F f).inv = F.map (coimage.π f)

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_assoc (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R) :
    eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)

Proof state:
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ f a = ((eval₂Hom f g).comp C) a

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = (eval₂Hom f g) (eval₂ C q p)

Tactic:
rw [eval₂_comp_left (eval₂Hom f g)]

Result:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p)

Tactic:
show _ = eval₂Hom f g (eval₂ C q p)

Result:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = (eval₂Hom f g) (eval₂ C q p)

Proof state:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
⊢ eval₂ f (fun t => eval₂ f g (q t)) p = eval₂ ((eval₂Hom f g).comp C) (⇑(eval₂Hom f g) ∘ q) p

Tactic:
congr with a

Result:
case e_f.a
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
q : S₂ → MvPolynomial σ R
p : MvPolynomial S₂ R
a : R
⊢ f a = ((eval₂Hom f g).comp C) a
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitUnopIsoUnopColimit_hom_comp_ι (F : Jᵒᵖ ⥤ Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) :
    (limitUnopIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.unop j.unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ Cᵒᵖ
inst✝ : HasColimit F
j : Jᵒᵖ
⊢ (limitUnopIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.unop (unop j)

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem length_of_sublistsLen :
    ∀ {n} {l l' : List α}, l' ∈ sublistsLen n l → length l' = n
  | 0, l, l', h => by simp_all
  | n + 1, a :: l, l', h => by
    rw [sublistsLen_succ_cons, mem_append, mem_map] at h
    rcases h with (h | ⟨l', h, rfl⟩)
    · exact length_of_sublistsLen h
    · exact congr_arg (· + 1) (length_of_sublistsLen h)

Proof state:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1 ∈ sublistsLen n l, a :: a_1 = l'
⊢ l'.length = n + 1

Tactic:
rcases h with (h | ⟨l', h, rfl⟩)

Result:
case inl
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

case inr.intro.intro
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1

Proof state:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ l'.length = n + 1

Tactic:
rw [sublistsLen_succ_cons, mem_append, mem_map] at h

Result:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ a_1 ∈ sublistsLen n l, a :: a_1 = l'
⊢ l'.length = n + 1

Proof state:
α : Type u
l l' : List α
h : l' ∈ sublistsLen 0 l
⊢ l'.length = 0

Tactic:
simp_all

Result:
no goals

Proof state:
case inl
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

Tactic:
exact length_of_sublistsLen h

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Away.lean
theorem Away.mk_eq_monoidOf_mk' : mk = (Away.monoidOf x).mk'

Proof state:
M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ mk = Submonoid.LocalizationMap.mk' (monoidOf x)

Tactic:
simp [Localization.mk_eq_monoidOf_mk']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_polynomialZ : (W'.map f).toJacobian.polynomialZ = MvPolynomial.map f W'.polynomialZ

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
⊢ (map W' f).toJacobian.polynomialZ = (MvPolynomial.map f) W'.polynomialZ

Tactic:
simp only [polynomialZ, map_polynomial, pderiv_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem intCast [StarOrderedRing R] [DecidableEq n] (d : ℤ) (hd : 0 ≤ d) :
    PosSemidef (d : Matrix n n R) :=
  ⟨isHermitian_intCast _, fun x => by
    simp only [intCast_mulVec, dotProduct_smul]
    rw [Int.cast_smul_eq_zsmul]
    exact zsmul_nonneg (dotProduct_star_self_nonneg _) hd⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n → R
⊢ 0 ≤ ↑d • (star x ⬝ᵥ x)

Tactic:
rw [Int.cast_smul_eq_zsmul]

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n → R
⊢ 0 ≤ d • (star x ⬝ᵥ x)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n → R
⊢ 0 ≤ d • (star x ⬝ᵥ x)

Tactic:
exact zsmul_nonneg (dotProduct_star_self_nonneg _) hd

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n → R
⊢ 0 ≤ star x ⬝ᵥ ↑d *ᵥ x

Tactic:
simp only [intCast_mulVec, dotProduct_smul]

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : ℤ
hd : 0 ≤ d
x : n → R
⊢ 0 ≤ ↑d • (star x ⬝ᵥ x)
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
h : (s ∩ t).Nonempty
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
rcases h with ⟨x, ⟨xs, xt⟩⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
simpa using diam_union xs xt

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem map_linearMap_addHaar_pi_eq_smul_addHaar {ι : Type*} [Finite ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ}
    (hf : LinearMap.det f ≠ 0) (μ : Measure (ι → ℝ)) [IsAddHaarMeasure μ] :
    Measure.map f μ = ENNReal.ofReal (abs (LinearMap.det f)⁻¹) • μ

Proof state:
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul,
  Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]

Result:
no goals

Proof state:
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
have := addHaarMeasure_unique μ (piIcc01 ι)

Result:
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
this : μ = μ ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Proof state:
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
inst✝¹ : Finite ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
μ : Measure (ι → ℝ)
inst✝ : μ.IsAddHaarMeasure
val✝ : Fintype ι
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD []

Proof state:
α : Type u_1
l : List α
⊢ l.tail = l.tail?.getD []

Tactic:
simp [tail_eq_tailD]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.pow [NormOneClass R] {f : α → R} {g : α → 𝕜} (h : IsBigOWith c l f g) :
    ∀ n : ℕ, IsBigOWith (c ^ n) l (fun x => f x ^ n) fun x => g x ^ n
  | 0 => by simpa using h.pow' 0
  | n + 1 => h.pow' (n + 1)

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝² : SeminormedRing R
inst✝¹ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
inst✝ : NormOneClass R
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
⊢ IsBigOWith (c ^ 0) l (fun x => f x ^ 0) fun x => g x ^ 0

Tactic:
simpa using h.pow' 0

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma mk_XYIdeal'_mul_mk_XYIdeal' {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁)
    (h₂ : W.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
    ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) =
      ClassGroup.mk (XYIdeal' <| nonsingular_add h₁ h₂ hxy)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ClassGroup.mk (XYIdeal' h₁ * XYIdeal' h₂) = ClassGroup.mk (XYIdeal' ⋯)

Tactic:
exact (ClassGroup.mk_eq_mk_of_coe_ideal (by exact (FractionalIdeal.coeIdeal_mul ..).symm) <|
    XYIdeal'_eq _).mpr
  ⟨_, _, XClass_ne_zero W _, YClass_ne_zero W _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ↑(XYIdeal' h₁ * XYIdeal' h₂) = ↑(XYIdeal W x₁ (C y₁) * XYIdeal W x₂ (C y₂))

Tactic:
exact (FractionalIdeal.coeIdeal_mul ..).symm

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) = ClassGroup.mk (XYIdeal' ⋯)

Tactic:
rw [← _root_.map_mul]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ClassGroup.mk (XYIdeal' h₁ * XYIdeal' h₂) = ClassGroup.mk (XYIdeal' ⋯)
-- Mathlib/Analysis/RCLike/Basic.lean
theorem one_re : re (1 : K) = 1

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ re 1 = 1

Tactic:
rw [← ofReal_one, ofReal_re]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq (hl : HasStrictFDerivAt l l' y)
    (hf : HasStrictDerivAt f f' x) (hy : y = f x) :
    HasStrictDerivAt (l ∘ f) (l' f') x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' (f x)
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt (l ∘ f) (l' f') x

Tactic:
exact hl.comp_hasStrictDerivAt x hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' y
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt (l ∘ f) (l' f') x

Tactic:
rw [hy] at hl

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasStrictFDerivAt l l' (f x)
hf : HasStrictDerivAt f f' x
hy : y = f x
⊢ HasStrictDerivAt (l ∘ f) (l' f') x
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
@[simp] lemma nextCoeffUp_zero : nextCoeffUp (0 : R[X]) = 0

Proof state:
R : Type u
inst✝ : Semiring R
⊢ nextCoeffUp 0 = 0

Tactic:
simp [nextCoeffUp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_add_one (h : m.1.WF) {k : α} {f : Option β → Option β}
    (h₁ : m.contains k = false) (h₂ : (f (Const.get? m k)).isSome) :
    (Const.alter m k f).1.size = m.1.size + 1

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
h₁ : m.contains k = false
h₂ : (f (get? m k)).isSome = true
⊢ (alter m k f).val.size = m.val.size + 1

Tactic:
simp [size_alter, h, h₁, h₂]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mod_.lean
theorem id_hom' (M : Mod_ A) : (𝟙 M : M ⟶ M).hom = 𝟙 M.X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A : Mon_ C
M : Mod_ A
⊢ (𝟙 M).hom = 𝟙 M.X

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem mem_zipIdx {x : α} {i : Nat} {xs : Vector α n} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
    k ≤ i ∧ i < k + n ∧
      x = xs[i - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
  ⟨le_snd_of_mem_zipIdx h, snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩

Proof state:
α : Type ?u.28578
n : Nat
x : α
i : Nat
xs : Vector α n
k : Nat
h : (x, i) ∈ xs.zipIdx k
⊢ i - k < n

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.28578
n : Nat
x : α
i : Nat
xs : Vector α n
k : Nat
h : (x, i) ∈ xs.zipIdx k
this : k ≤ (x, i).snd
⊢ i - k < n

Proof state:
α : Type ?u.28578
n : Nat
x : α
i : Nat
xs : Vector α n
k : Nat
h : (x, i) ∈ xs.zipIdx k
this✝ : k ≤ (x, i).snd
this : (x, i).snd < k + n
⊢ i - k < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.28578
n : Nat
x : α
i : Nat
xs : Vector α n
k : Nat
h : (x, i) ∈ xs.zipIdx k
this : k ≤ (x, i).snd
⊢ i - k < n

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.28578
n : Nat
x : α
i : Nat
xs : Vector α n
k : Nat
h : (x, i) ∈ xs.zipIdx k
this✝ : k ≤ (x, i).snd
this : (x, i).snd < k + n
⊢ i - k < n
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_inv_tensor_right (X Y Z : C) :
    (β_ X (Y ⊗ Z)).inv  =
      (α_ Y Z X).hom ≫ Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫
        (β_ X Y).inv ▷ Z ≫ (α_ X Y Z).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ inv (β_ X (Y ⊗ Z)).inv = inv ((α_ Y Z X).hom ≫ Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫ (β_ X Y).inv ▷ Z ≫ (α_ X Y Z).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Sl2.lean
@[nolint unusedArguments]
lemma lie_f_pow_toEnd_f (P : HasPrimitiveVectorWith t m μ) (n : ℕ) :
    ⁅f, ψ n⁆ = ψ (n + 1)

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
h e f : L
m : M
μ : R
t : IsSl2Triple h e f
P : t.HasPrimitiveVectorWith m μ
n : ℕ
⊢ ⁅f, ((toEnd R L M) f ^ n) m⁆ = ((toEnd R L M) f ^ (n + 1)) m

Tactic:
simp [pow_succ']

Result:
no goals
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem mapClusterPt_inv_atTop_pow {x y : G} :
    MapClusterPt x⁻¹ atTop (y ^ · : ℕ → G) ↔ MapClusterPt x atTop (y ^ · : ℕ → G)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
⊢ (MapClusterPt x⁻¹ atTop fun x => y ^ x) ↔ MapClusterPt x atTop fun x => y ^ x

Tactic:
simp only [mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, inv_mem_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
lemma LinearMap.toMatrixOrthonormal_reindex (e : n ≃ m) (f : E →ₗ[𝕜] E) :
    toMatrixOrthonormal (v₁.reindex e) f = (toMatrixOrthonormal v₁ f).reindex e e :=
  Matrix.ext fun i j =>
    calc toMatrixOrthonormal (v₁.reindex e) f i j
      _ = (v₁.reindex e).repr (f (v₁.reindex e j)) i := f.toMatrix_apply ..
      _ = v₁.repr (f (v₁ (e.symm j))) (e.symm i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
m : Type u_5
n : Type u_6
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : FiniteDimensional 𝕜 E
v₁ : OrthonormalBasis n 𝕜 E
e : n ≃ m
f : E →ₗ[𝕜] E
i j : m
⊢ (v₁.reindex e).repr (f ((v₁.reindex e) j)) i = v₁.repr (f (v₁ (e.symm j))) (e.symm i)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_inv_iff_mul_le_one_left : a ≤ b⁻¹ ↔ b * a ≤ 1 :=
  (mul_le_mul_iff_left b).symm.trans <| by rw [mul_inv_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ b * a ≤ b * b⁻¹ ↔ b * a ≤ 1

Tactic:
rw [mul_inv_cancel]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_eq_finsetCard (s : Finset α) : Nat.card s = s.card

Proof state:
α : Type u_1
s : Finset α
⊢ Nat.card { x // x ∈ s } = s.card

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Basic.lean
theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l

Proof state:
α : Type u
l : Array α
i : Nat
h : i < l.size
⊢ getElem l i h ∈ l

Tactic:
rw [Array.mem_def, ← getElem_toList]

Result:
α : Type u
l : Array α
i : Nat
h : i < l.size
⊢ getElem l.toList i h ∈ l.toList

Proof state:
α : Type u
l : Array α
i : Nat
h : i < l.size
⊢ getElem l.toList i h ∈ l.toList

Tactic:
apply List.getElem_mem

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem measurable_div_const' {G : Type*} [DivInvMonoid G] [MeasurableSpace G] [MeasurableMul G]
    (g : G) : Measurable fun h => h / g

Proof state:
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableMul G
g : G
⊢ Measurable fun h => h / g

Tactic:
simp_rw [div_eq_mul_inv, measurable_mul_const]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_ball_iff_norm'' : b ∈ ball a r ↔ ‖b / a‖ < r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖b / a‖ < r

Tactic:
rw [mem_ball, dist_eq_norm_div]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
protected lemma min_le_iff : min (a : WithZero α) b ≤ c ↔ min a b ≤ c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ↑a ⊓ ↑b ≤ ↑c ↔ a ⊓ b ≤ c

Tactic:
simp only [WithZero.coe_le_coe, min_le_iff]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem IsPWO.isWF (h : s.IsPWO) : s.IsWF

Proof state:
α : Type u_2
inst✝ : Preorder α
s : Set α
h : s.IsPWO
⊢ s.IsWF

Tactic:
simpa only [← lt_iff_le_not_le] using h.wellFoundedOn

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem cyclicPermutations_injective : Function.Injective (@cyclicPermutations α) := fun l l' h ↦ by
  simpa using congr_arg head? h

Proof state:
α : Type u
l l' : List α
h : l.cyclicPermutations = l'.cyclicPermutations
⊢ l = l'

Tactic:
simpa using congr_arg head? h

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.eq_generate (h : l.HasBasis p s) : l = generate { U | ∃ i, p i ∧ s i = U }

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ l = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
rw [← h.isBasis.filter_eq_generate, h.filter_eq]

Result:
no goals