harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean
theorem dist_normed_convolution_le {x₀ : G} {ε : ℝ} (hmg : AEStronglyMeasurable g μ)
    (hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε) :
    dist ((φ.normed μ ⋆[lsmul ℝ ℝ, μ] g : G → E') x₀) (g x₀) ≤ ε :=
  dist_convolution_le (by simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self φ.rOut_pos)])
    φ.support_normed_eq.subset φ.nonneg_normed φ.integral_normed hmg hg

Proof state:
G : Type uG
E' : Type uE'
inst✝¹¹ : NormedAddCommGroup E'
g : G → E'
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedSpace ℝ E'
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : HasContDiffBump G
inst✝⁵ : CompleteSpace E'
φ : ContDiffBump 0
inst✝⁴ : BorelSpace G
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : FiniteDimensional ℝ G
inst✝ : μ.IsAddLeftInvariant
x₀ : G
ε : ℝ
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε
⊢ 0 ≤ ε

Tactic:
simp_rw [← dist_self (g x₀), hg x₀ (mem_ball_self φ.rOut_pos)]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma lt_mul_self_iff : ∀ {n : ℕ}, n < n * n ↔ 1 < n
  | 0 => by simp
  | n + 1 => Nat.lt_mul_iff_one_lt_left n.succ_pos

Proof state:
⊢ 0 < 0 * 0 ↔ 1 < 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem All_def {t : RBNode α} : t.All p ↔ ∀ x ∈ t, p x

Proof state:
α : Type u_1
p : α → Prop
t : RBNode α
⊢ All p t ↔ ∀ (x : α), x ∈ t → p x

Tactic:
induction t <;> simp [or_imp, forall_and, *]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_apply_singleton (a : α) (h : MeasurableSet ({a} : Set α)) :
    p.toMeasure {a} = p a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
a : α
h : MeasurableSet {a}
⊢ p.toMeasure {a} = p a

Tactic:
simp [toMeasure_apply_eq_toOuterMeasure_apply _ _ h, toOuterMeasure_apply_singleton]

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem comp_noncommPiCoprod {P : Type*} [Monoid P] {f : M →* P}
    (hcomm' : Pairwise fun i j => ∀ x y, Commute (f.comp (ϕ i) x) (f.comp (ϕ j) y) :=
      Pairwise.mono hcomm (fun i j ↦ forall_imp (fun x h y ↦ by
        simp only [MonoidHom.coe_comp, Function.comp_apply, Commute.map  (h y) f]))) :
    f.comp (MonoidHom.noncommPiCoprod ϕ hcomm) =
      MonoidHom.noncommPiCoprod (fun i ↦ f.comp (ϕ i)) hcomm' :=
  MonoidHom.ext fun _ ↦ by
    simp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk,
      Function.comp_apply, Finset.map_noncommProd]

Proof state:
M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
P : Type u_4
inst✝ : Monoid P
f : M →* P
hcomm' : optParam (Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y)) ⋯
x✝ : (i : ι) → N i
⊢ (f.comp (noncommPiCoprod ϕ hcomm)) x✝ = (noncommPiCoprod (fun i => f.comp (ϕ i)) hcomm') x✝

Tactic:
simp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk,
  Function.comp_apply, Finset.map_noncommProd]

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : Monoid M
ι : Type u_2
inst✝² : Fintype ι
N : ι → Type u_3
inst✝¹ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
P : Type u_4
inst✝ : Monoid P
f : M →* P
i j : ι
x : N i
h : ∀ (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
y : N j
⊢ Commute ((f.comp (ϕ i)) x) ((f.comp (ϕ j)) y)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, Commute.map  (h y) f]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToL1S_le (T : Set α → E →L[ℝ] F) {C : ℝ}
    (hT_norm : ∀ s, MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * (μ s).toReal) (f : α →₁ₛ[μ] E) :
    ‖setToL1S T f‖ ≤ C * ‖f‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal
f : ↥(simpleFunc E 1 μ)
⊢ ‖setToL1S T f‖ ≤ C * ‖f‖

Tactic:
rw [setToL1S, norm_eq_sum_mul f]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal
f : ↥(simpleFunc E 1 μ)
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal
f : ↥(simpleFunc E 1 μ)
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤
    C * ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
exact
  SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm_of_integrable T hT_norm _
    (SimpleFunc.integrable f)

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem hasTerminal_of_isSeparating [LocallySmall.{w} Cᵒᵖ] [WellPowered.{w} Cᵒᵖ]
    [HasColimitsOfSize.{w, w} C] {𝒢 : Set C} [Small.{w} 𝒢]
    (h𝒢 : IsSeparating 𝒢) : HasTerminal C

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst✝² : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst✝¹ : HasColimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
this : Small.{w, u₁} ↑𝒢.op
⊢ HasTerminal C

Tactic:
haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating ((isCoseparating_op_iff _).2 h𝒢)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst✝² : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst✝¹ : HasColimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
this✝ : Small.{w, u₁} ↑𝒢.op
this : HasInitial Cᵒᵖ
⊢ HasTerminal C

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst✝² : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst✝¹ : HasColimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
⊢ HasTerminal C

Tactic:
haveI : Small.{w} 𝒢.op := small_of_injective (Set.opEquiv_self 𝒢).injective

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst✝² : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst✝¹ : HasColimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
this : Small.{w, u₁} ↑𝒢.op
⊢ HasTerminal C

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst✝² : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst✝¹ : HasColimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
this✝ : Small.{w, u₁} ↑𝒢.op
this : HasInitial Cᵒᵖ
⊢ HasTerminal C

Tactic:
exact hasTerminal_of_hasInitial_op

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coconePointUniqueUpToIso_inv_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
    (coconePointUniqueUpToIso P Q).inv ≫ P.desc r = Q.desc r :=
  Q.uniq _ _ (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r s t : Cocone F
P : IsColimit s
Q : IsColimit t
⊢ ∀ (j : J), t.ι.app j ≫ (P.coconePointUniqueUpToIso Q).inv ≫ P.desc r = r.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/SMulWithZero.lean
protected lemma MulActionWithZero.subsingleton
    [MulActionWithZero R M] [Subsingleton R] : Subsingleton M :=
  ⟨fun x y => by
    rw [← one_smul R x, ← one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]⟩

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : MonoidWithZero R
inst✝² : Zero M
inst✝¹ : MulActionWithZero R M
inst✝ : Subsingleton R
x y : M
⊢ x = y

Tactic:
rw [← one_smul R x, ← one_smul R y, Subsingleton.elim (1 : R) 0, zero_smul, zero_smul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').support = p.support ++ p'.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').support = p.support ++ p'.support.tail

Tactic:
induction p <;> cases p' <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_mul_prod_one_sub_of_lt_order {R ι : Type*} [CommRing R] (d : σ →₀ ℕ) (s : Finset ι)
    (f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R) :
    (∀ i ∈ s, degree d < order (g i)) → coeff R d (f * ∏ i ∈ s, (1 - g i)) = coeff R d f

Proof state:
σ : Type u_1
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, ↑((weight fun x => 1) d) < (g i).order) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f

Tactic:
exact coeff_mul_prod_one_sub_of_lt_weightedOrder _ d s f g

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, ↑d.degree < (g i).order) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_4
ι : Type u_5
inst✝ : CommRing R
d : σ →₀ ℕ
s : Finset ι
f : MvPowerSeries σ R
g : ι → MvPowerSeries σ R
⊢ (∀ i ∈ s, ↑((weight fun x => 1) d) < (g i).order) → (coeff R d) (f * ∏ i ∈ s, (1 - g i)) = (coeff R d) f
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem comp_eq_of_monotoneOn {β : Type*} [LinearOrder β] (f : α → E) {t : Set β}
    (φ : β → α) (hφ : MonotoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) :
    variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
rcases le_total x y with (h | h)

Result:
case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Proof state:
case inl
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
rw [variationOnFromTo.eq_of_le _ _ h, variationOnFromTo.eq_of_le _ _ (hφ hx hy h),
  eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hx hy]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
rw [variationOnFromTo.eq_of_ge _ _ h, variationOnFromTo.eq_of_ge _ _ (hφ hy hx h),
  eVariationOn.comp_inter_Icc_eq_of_monotoneOn f φ hφ hy hx]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
theorem of_comm {A ι : Type*} [CommRing A] (B : ι → AddSubgroup A)
    (inter : ∀ i j, ∃ k, B k ≤ B i ⊓ B j) (mul : ∀ i, ∃ j, (B j : Set A) * B j ⊆ B i)
    (leftMul : ∀ x : A, ∀ i, ∃ j, (B j : Set A) ⊆ (fun y : A => x * y) ⁻¹' B i) :
    RingSubgroupsBasis B :=
  { inter
    mul
    leftMul
    rightMul := fun x i ↦ (leftMul x i).imp fun j hj ↦ by simpa only [mul_comm] using hj }

Proof state:
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i j : ι
hj : ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)

Tactic:
simpa only [mul_comm] using hj

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem exists_hasEigenvalue_of_iSup_genEigenspace_eq_top [Nontrivial M] {f : End R M}
    (hf : ⨆ μ, ⨆ k : ℕ, f.genEigenspace μ k = ⊤) :
    ∃ μ, f.HasEigenvalue μ

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
⊢ ∃ μ, f.HasEigenvalue μ

Tactic:
apply exists_hasEigenvalue_of_genEigenspace_eq_top _ hf

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) ↑k = ⊤
⊢ ∃ μ, f.HasEigenvalue μ

Tactic:
simp_rw [iSup_genEigenspace_eq] at hf

Result:
R : Type u_3
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
f : End R M
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
⊢ ∃ μ, f.HasEigenvalue μ
-- Mathlib/Algebra/Ring/Commute.lean
theorem mul_self_eq_one_iff [NonAssocRing R] [NoZeroDivisors R] {a : R} :
    a * a = 1 ↔ a = 1 ∨ a = -1

Proof state:
R : Type u
inst✝¹ : NonAssocRing R
inst✝ : NoZeroDivisors R
a : R
⊢ a * a = 1 ↔ a = 1 ∨ a = -1

Tactic:
rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_reverse : ∀ l : List α, formPerm l.reverse = (formPerm l)⁻¹
  | [] => rfl
  | [_] => rfl
  | a::b::l => by
    simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b::l)]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (a :: b :: l).reverse.formPerm = (a :: b :: l).formPerm⁻¹

Tactic:
simp [formPerm_append_pair, swap_comm, ← formPerm_reverse (b::l)]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_lt [LinearOrderedSemiring α] {m n : PosNum} : (m : α) < n ↔ m < n

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemiring α
m n : PosNum
⊢ ↑m < ↑n ↔ m < n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem bot_eq_top_of_finrank_adjoin_le_one [FiniteDimensional F E]
    (h : ∀ x : E, finrank F F⟮x⟯ ≤ 1) : (⊥ : IntermediateField F E) = ⊤

Proof state:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
⊢ ∀ (x : E), finrank F ↥F⟮x⟯ = 1

Tactic:
exact fun x => by linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
⊢ ⊥ = ⊤

Tactic:
apply bot_eq_top_of_finrank_adjoin_eq_one

Result:
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
⊢ ∀ (x : E), finrank F ↥F⟮x⟯ = 1

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : ∀ (x : E), finrank F ↥F⟮x⟯ ≤ 1
x : E
⊢ finrank F ↥F⟮x⟯ = 1

Tactic:
linarith [h x, show 0 < finrank F F⟮x⟯ from finrank_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_push (a : α) (l : Vector α n) : countP p (l.push a) = countP p l + if p a then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
l : Vector α n
⊢ countP p (l.push a) = countP p l + if p a = true then 1 else 0

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
l : Array α
⊢ countP p ({ toArray := l, size_toArray := ⋯ }.push a) =
    countP p { toArray := l, size_toArray := ⋯ } + if p a = true then 1 else 0

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
l : Array α
⊢ countP p ({ toArray := l, size_toArray := ⋯ }.push a) =
    countP p { toArray := l, size_toArray := ⋯ } + if p a = true then 1 else 0

Tactic:
simp [Array.countP_push]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma forall_congr_right : (∀ a, q (e a)) ↔ ∀ b, q b :=
  ⟨fun h a ↦ by simpa using h (e.symm a), fun h _ ↦ h _⟩

Proof state:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
h : ∀ (a : α), q (e a)
a : β
⊢ q a

Tactic:
simpa using h (e.symm a)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_intCast (n : ℤ) : natDegree (n : R[X]) = 0

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natDegree = 0

Tactic:
rw [← C_eq_intCast, natDegree_C]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_neg : s • -t = -(s • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Set α
t : Set β
⊢ s • -t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

Result:
α : Type u_2
β : Type u_3
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Set α
t : Set β
⊢ s • (fun x => -x) '' t = (fun x => -x) '' (s • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Set α
t : Set β
⊢ s • (fun x => -x) '' t = (fun x => -x) '' (s • t)

Tactic:
exact image_image2_right_comm smul_neg

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem modOf_add_divOf (x : k[G]) (g : G) : x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x

Tactic:
rw [add_comm, divOf_add_modOf]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_le_iff_ne_zero {c : Cardinal} : 1 ≤ c ↔ c ≠ 0

Proof state:
c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ c ≠ 0

Tactic:
rw [one_le_iff_pos, pos_iff_ne_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineEquiv.affineIndependent_set_of_eq_iff {s : Set P} (e : P ≃ᵃ[k] P₂) :
    AffineIndependent k ((↑) : e '' s → P₂) ↔ AffineIndependent k ((↑) : s → P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
⊢ AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val

Tactic:
have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
this : ⇑e ∘ Subtype.val = Subtype.val ∘ ⇑((↑e).image s)
⊢ AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
this : ⇑e ∘ Subtype.val = Subtype.val ∘ ⇑((↑e).image s)
⊢ AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val

Tactic:
erw [← e.affineIndependent_iff, this, affineIndependent_equiv]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma neg_smul (P : Fin 3 → R) (u : R) : W'.neg (u • P) = u • W'.neg P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
simpa only [neg, negY_smul] using (smul_fin3 (W'.neg P) u).symm

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mrange_inr : mrange (inr M N) = prod ⊥ ⊤

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mrange (inr M N) = ⊥.prod ⊤

Tactic:
simpa only [mrange_eq_map] using map_inr ⊤

Result:
no goals
-- Mathlib/Order/Basic.lean
protected lemma lt_of_lt_of_le (h₁ : x.1 < y.1) (h₂ : x.2 ≤ y.2) : x < y

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
simp [lt_iff, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem_modifyHead_succ {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
    (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h)

Proof state:
α : Type u_1
l : List α
f : α → α
n : Nat
h : n + 1 < (modifyHead f l).length
⊢ (modifyHead f l)[n + 1] = l[n + 1]

Tactic:
simp [getElem_modifyHead]

Result:
no goals

Proof state:
α : Type ?u.3318
l : List α
f : α → α
n : Nat
h : n + 1 < (modifyHead f l).length
⊢ n + 1 < l.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem chineseRemainder'_lt_lcm (h : a ≡ b [MOD gcd n m]) (hn : n ≠ 0) (hm : m ≠ 0) :
    ↑(chineseRemainder' h) < lcm n m

Proof state:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : 0 < ↑(n.lcm m)
⊢ ((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat <
    (↑(n.lcm m)).toNat

Tactic:
exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)

Result:
no goals

Proof state:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then ⟨a, ⋯⟩
      else
        if hm : m = 0 then ⟨b, ⋯⟩
        else ⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩) <
    n.lcm m

Tactic:
rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]

Result:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat <
    (↑(n.lcm m)).toNat

Proof state:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat <
    (↑(n.lcm m)).toNat

Tactic:
have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))

Result:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
lcm_pos : 0 < ↑(n.lcm m)
⊢ ((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat <
    (↑(n.lcm m)).toNat

Proof state:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(chineseRemainder' h) < n.lcm m

Tactic:
dsimp only [chineseRemainder']

Result:
m n a b : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n ≠ 0
hm : m ≠ 0
⊢ ↑(if hn : n = 0 then ⟨a, ⋯⟩
      else
        if hm : m = 0 then ⟨b, ⋯⟩
        else ⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩) <
    n.lcm m
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem ι_mul_ι_mul_ι (a b : M) :
    ι Q a * ι Q b * ι Q a = ι Q (QuadraticMap.polar Q a b • a - Q a • b)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a b : M
⊢ (ι Q) a * (ι Q) b * (ι Q) a = (ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

Tactic:
rw [ι_mul_ι_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ←
  Algebra.smul_def, ← map_smul, ← map_smul, ← map_sub]

Result:
no goals