harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Flat/Basic.lean
lemma _root_.LinearMap.rTensor_injective_iff_subtype {f : N →ₗ[R] P} (hf : Function.Injective f)
    (e : P ≃ₗ[R] Q) : Function.Injective (f.rTensor M) ↔
      Function.Injective ((range <| e.toLinearMap ∘ₗ f).subtype.rTensor M)

Proof state:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Function.Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Function.Injective ⇑(rTensor M (↑e ∘ₗ f)) ↔
    Function.Injective ⇑(rTensor M ((range (↑e ∘ₗ f)).subtype ∘ₗ ↑(LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯)))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Function.Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Function.Injective ⇑(rTensor M f) ↔ Function.Injective ⇑(rTensor M (range (↑e ∘ₗ f)).subtype)

Tactic:
simp_rw [← EquivLike.injective_comp <| (LinearEquiv.ofInjective (e.toLinearMap ∘ₗ f)
  (e.injective.comp hf)).rTensor M, ← EquivLike.comp_injective _ (e.rTensor M),
  ← LinearEquiv.coe_coe, ← coe_comp, LinearEquiv.coe_rTensor,  ← rTensor_comp]

Result:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Function.Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Function.Injective ⇑(rTensor M (↑e ∘ₗ f)) ↔
    Function.Injective ⇑(rTensor M ((range (↑e ∘ₗ f)).subtype ∘ₗ ↑(LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯)))
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_bot_left : relrank ⊥ A = Module.rank F A

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ ⊥.relrank A = Module.rank F ↥A

Tactic:
rw [← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le), IntermediateField.rank_bot, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma image_top : (⊤ : Subpresheaf F).image f = range f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ⊤.image f = range f

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.toListModel_insertMany_list {β : Type v} [BEq α] [Hashable α] [EquivBEq α]
    [LawfulHashable α] {m : Raw₀ α (fun _ => β)} {l : List (α × β)} (h : Raw.WFImp m.1) :
    Perm (toListModel (Const.insertMany m l).1.1.buckets)
      (insertListConst (toListModel m.1.buckets) l)

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
l : List (α × β)
h : Raw.WFImp m.val
⊢ toListModel (insertListₘ m l).val.buckets ~ insertListConst (toListModel m.val.buckets) l

Tactic:
apply toListModel_insertListₘ h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
l : List (α × β)
h : Raw.WFImp m.val
⊢ toListModel (insertMany m l).val.val.buckets ~ insertListConst (toListModel m.val.buckets) l

Tactic:
rw [Const.insertMany_eq_insertListₘ]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
l : List (α × β)
h : Raw.WFImp m.val
⊢ toListModel (insertListₘ m l).val.buckets ~ insertListConst (toListModel m.val.buckets) l
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_inf {π₁ π₂ : Prepartition I} :
    J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, (J : WithBot (Box ι)) = ↑J₁ ⊓ ↑J₂

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
⊢ J ∈ π₁ ⊓ π₂ ↔ ∃ J₁ ∈ π₁, ∃ J₂ ∈ π₂, ↑J = ↑J₁ ⊓ ↑J₂

Tactic:
simp only [inf_def, mem_biUnion, mem_restrict]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem eval₂Hom_comp_C (f : R →+* S) (g : σ → S) : (eval₂Hom f g).comp C = f

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp C = f

Tactic:
ext1 r

Result:
case a
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
r : R
⊢ ((eval₂Hom f g).comp C) r = f r

Proof state:
case a
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
r : R
⊢ ((eval₂Hom f g).comp C) r = f r

Tactic:
exact eval₂_C f g r

Result:
no goals
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem Real.mem_closure_iff {s : Set ℝ} {x : ℝ} :
    x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε

Proof state:
s : Set ℝ
x : ℝ
⊢ x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε

Tactic:
simp [mem_closure_iff_nhds_basis nhds_basis_ball, Real.dist_eq]

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem lt_sup_principal_of_not_mem (hx : x ∉ I) : I < I ⊔ principal x :=
  le_sup_left.lt_of_ne fun h ↦ hx <| by simpa only [left_eq_sup, principal_le_iff] using h

Proof state:
P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I

Tactic:
simpa only [left_eq_sup, principal_le_iff] using h

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_re_lt (a : ℝ) : frontier { z : ℂ | z.re < a } = { z | z.re = a }

Proof state:
a : ℝ
⊢ frontier {z | z.re < a} = {z | z.re = a}

Tactic:
simpa only [frontier_Iio] using frontier_preimage_re (Iio a)

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem _root_.Semigroup.mem_center_iff {z : M} :
    z ∈ Set.center M ↔ ∀ g, g * z = z * g := ⟨fun a g ↦ by rw [IsMulCentral.comm a g],
  fun h ↦ ⟨fun _ ↦ (Commute.eq (h _)).symm, fun _ _ ↦ (mul_assoc z _ _).symm,
  fun _ _ ↦ mul_assoc _ z _, fun _ _ ↦ mul_assoc _ _ z⟩ ⟩

Proof state:
M : Type u_1
inst✝ : Semigroup M
z : M
a : z ∈ center M
g : M
⊢ g * z = z * g

Tactic:
rw [IsMulCentral.comm a g]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanSingleton_le_iff_mem {x : P} {I : FractionalIdeal S P} :
    spanSingleton S x ≤ I ↔ x ∈ I

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I : FractionalIdeal S P
⊢ spanSingleton S x ≤ I ↔ x ∈ I

Tactic:
rw [← coe_le_coe, coe_spanSingleton, Submodule.span_singleton_le_iff_mem, mem_coe]

Result:
no goals
-- Mathlib/Order/BoundedOrder/Basic.lean
theorem coe_eq_bot_iff [OrderBot α] [OrderBot (Subtype p)] (hbot : p ⊥) {x : { x // p x }} :
    (x : α) = ⊥ ↔ x = ⊥

Proof state:
α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : OrderBot (Subtype p)
hbot : p ⊥
x : { x // p x }
⊢ ↑x = ⊥ ↔ x = ⊥

Tactic:
rw [← coe_bot hbot, Subtype.ext_iff]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.succ_ne (h : IsSuccPrelimit a) (b : α) : succ b ≠ a

Proof state:
α : Type u_1
a : α
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
h : IsSuccPrelimit a
b : α
⊢ succ b ≠ a

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ b)
⊢ False

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
b : α
h : IsSuccPrelimit (succ b)
⊢ False

Tactic:
exact not_isMax _ h.isMax

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
/-- Dirac delta measures at two different points are different, assuming the measurable space
separates points. -/
lemma dirac_ne_dirac [SeparatesPoints α] {x y : α} (x_ne_y : x ≠ y) :
    Measure.dirac x ≠ Measure.dirac y

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
y_notin_A : y ∉ A
⊢ dirac x ≠ dirac y

Tactic:
exact dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
⊢ dirac x ≠ dirac y

Tactic:
obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace.SeparatesPoints α
x y : α
x_ne_y : x ≠ y
A : Set α
A_mble : MeasurableSet A
x_in_A : x ∈ A
y_notin_A : y ∉ A
⊢ dirac x ≠ dirac y
-- Mathlib/Topology/UnitInterval.lean
theorem lt_symm_comm {i j : I} : i < σ j ↔ j < σ i

Proof state:
i j : ↑I
⊢ i < σ j ↔ j < σ i

Tactic:
rw [← symm_lt_symm, symm_symm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_rootD_l : Equiv self (self.rootD a) b ↔ Equiv self a b

Proof state:
self : UnionFind
a b : Nat
⊢ self.Equiv (self.rootD a) b ↔ self.Equiv a b

Tactic:
simp [Equiv, rootD_rootD]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.smod_umod (x y : BitVec w) :
    x.smod y =
      bif x.getLsbD (w - 1) then
        bif y.getLsbD (w - 1) then
          - ((- x) % (- y))
        else
          (bif (- x) % y == 0#w then (- x) % y else y - (- x) % y)
      else
        bif y.getLsbD (w - 1) then
          (bif x % (- y) == 0#w then x % (- y) else x % (- y) + y)
        else
          x.umod y

Proof state:
w : Nat
x y : BitVec w
⊢ x.smod y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else bif -x % y == 0#w then -x % y else y - -x % y
    else bif y.getLsbD (w - 1) then bif x % -y == 0#w then x % -y else x % -y + y else x.umod y

Tactic:
rw [BitVec.smod_eq, ← BitVec.msb_eq_getLsbD_last, ← BitVec.msb_eq_getLsbD_last]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      let u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)) =
    bif x.msb then bif y.msb then -(-x % -y) else bif -x % y == 0#w then -x % y else y - -x % y
    else bif y.msb then bif x % -y == 0#w then x % -y else x % -y + y else x.umod y

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      let u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)) =
    bif x.msb then bif y.msb then -(-x % -y) else bif -x % y == 0#w then -x % y else y - -x % y
    else bif y.msb then bif x % -y == 0#w then x % -y else x % -y + y else x.umod y

Tactic:
cases x.msb <;> cases y.msb <;> simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_add_left (x y : V) : (o.oangle (x + y) y).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle (x + y) y).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_add_smul_left x y 1, one_smul]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_mul_abs (x : α) : (sign x * |x| : α) = x

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
x : α
⊢ ↑(sign x) * |x| = x

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Result:
no goals
-- Mathlib/Analysis/Complex/Asymptotics.lean
theorem isTheta_ofReal (f : α → ℝ) (l : Filter α) : (f · : α → ℂ) =Θ[l] f :=
  .of_norm_left <| by simpa using (Asymptotics.isTheta_rfl (f := f)).norm_left

Proof state:
α : Type u_1
f : α → ℝ
l : Filter α
⊢ (fun x => ‖↑(f x)‖) =Θ[l] f

Tactic:
simpa using (Asymptotics.isTheta_rfl (f := f)).norm_left

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem not_coprime_zero_zero : ¬Coprime 0 0

Proof state:
⊢ ¬Coprime 0 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma floorRoot_eq_zero : floorRoot n a = 0 ↔ n = 0 ∨ a = 0 :=
  floorRoot_ne_zero.not_right.trans <| by simp only [not_and_or, ne_eq, not_not]

Proof state:
a n : ℕ
⊢ ¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0

Tactic:
simp only [not_and_or, ne_eq, not_not]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/AffineMap.lean
theorem hasStrictDerivAt_lineMap : HasStrictDerivAt (lineMap a b) (b - a) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : E
x : 𝕜
⊢ HasStrictDerivAt (⇑(lineMap a b)) (b - a) x

Tactic:
simpa using (lineMap a b : 𝕜 →ᵃ[𝕜] E).hasStrictDerivAt

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp) posPart_pos] lemma one_lt_oneLePart (ha : 1 < a) : 1 < a⁺ᵐ

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
ha : 1 < a
⊢ 1 < a⁺ᵐ

Tactic:
rwa [oneLePart_eq_self.2 ha.le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z)

Proof state:
n : Nat
x y z : BitVec n
⊢ x + y + z = x + (y + z)

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
x y z : BitVec n
⊢ (x + y + z).toNat = (x + (y + z)).toNat

Proof state:
case a
n : Nat
x y z : BitVec n
⊢ (x + y + z).toNat = (x + (y + z)).toNat

Tactic:
simp [Nat.add_assoc]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/AddCircle.lean
theorem ergodic_nsmul {n : ℕ} (hn : 1 < n) : Ergodic fun y : AddCircle T => n • y :=
  ergodic_zsmul (by simp [hn] : 1 < |(n : ℤ)|)

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℕ
hn : 1 < n
⊢ 1 < |↑n|

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_smul_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = u ^ 4 • W'.add P Q

Tactic:
rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_sub (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
    ∫ x in a..b, f x - g x ∂μ = (∫ x in a..b, f x ∂μ) - ∫ x in a..b, g x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ ∫ (x : ℝ) in a..b, f x - g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simpa only [sub_eq_add_neg] using (integral_add hf hg.neg).trans (congr_arg _ integral_neg)

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem sub_mem_Ico_zero_iff_right : b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Tactic:
simp only [sub_mem_Ico_iff_right, sub_self, sub_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_alter [Inhabited α] {k k' : α} (h : m.1.WF) {f : Option β → Option β} :
    (Const.alter m k f).getKey! k' =
      if k == k' then
        if (f (Const.get? m k)).isSome then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
inst✝ : Inhabited α
k k' : α
h : m.val.WF
f : Option β → Option β
⊢ (alter m k f).getKey! k' =
    if (k == k') = true then if (f (get? m k)).isSome = true then k else default else m.getKey! k'

Tactic:
simp_to_model [Const.alter] using List.Const.getKey!_alterKey

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem _root_.Matrix.posDef_intCast_iff [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
    [Nonempty n] [Nontrivial R] {d : ℤ} :
    PosDef (d : Matrix n n R) ↔ 0 < d :=
  posDef_diagonal_iff.trans <| by simp

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
inst✝² : NoZeroDivisors R
inst✝¹ : Nonempty n
inst✝ : Nontrivial R
d : ℤ
⊢ n → 0 < ↑d ↔ 0 < d

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_replaceEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (replaceEntry k v l).length = l.length

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (replaceEntry k v l).length = l.length

Tactic:
induction l using assoc_induction <;> simp_all [replaceEntry_cons, Bool.apply_cond List.length]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_modify_self (h : m.1.WF) {k : α} {f : β → β} :
    (Const.modify m k f).getKey? k = if m.contains k then some k else none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : β → β
⊢ (modify m k f).getKey? k = if m.contains k = true then some k else none

Tactic:
simp_to_model [Const.modify] using List.Const.getKey?_modifyKey_self

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : 𝕜
⊢ ofScalars E (x • c) = x • ofScalars E c

Tactic:
unfold ofScalars

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : 𝕜
⊢ (fun n => (x • c) n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    x • fun n => c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
x : 𝕜
⊢ (fun n => (x • c) n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) =
    x • fun n => c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E

Tactic:
simp [Pi.smul_def x _, smul_smul]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_comp_add_left (a : E) :
    fderiv 𝕜 (fun x ↦ f (a + x)) x = fderiv 𝕜 f (a + x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x a : E
⊢ fderiv 𝕜 (fun x => f (a + x)) x = fderiv 𝕜 f (a + x)

Tactic:
simpa [add_comm a] using fderiv_comp_add_right a

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem continuousAt_of_locally_uniform_approx_of_continuousAt
    (L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
    ContinuousAt f x

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace β
f : α → β
x : α
inst✝ : TopologicalSpace α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x

Tactic:
apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace β
f : α → β
x : α
inst✝ : TopologicalSpace α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ F, ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace β
f : α → β
x : α
inst✝ : TopologicalSpace α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousAt f x

Tactic:
rw [← continuousWithinAt_univ]

Result:
α : Type u
β : Type v
inst✝¹ : UniformSpace β
f : α → β
x : α
inst✝ : TopologicalSpace α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace β
f : α → β
x : α
inst✝ : TopologicalSpace α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ F, ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_two : T R 2 = 2 * X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ T R 2 = 2 * X ^ 2 - 1

Tactic:
simpa [pow_two, mul_assoc] using T_add_two R 0

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_succ_left (n : ℕ) :
    ascPochhammer S (n + 1) = X * (ascPochhammer S n).comp (X + 1)

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ ascPochhammer S (n + 1) = X * (ascPochhammer S n).comp (X + 1)

Tactic:
rw [ascPochhammer]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_append (L₁ L₂ : List (List α)) : flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂

Proof state:
α : Type u_1
L₁ L₂ : List (List α)
⊢ (L₁ ++ L₂).flatten = L₁.flatten ++ L₂.flatten

Tactic:
induction L₁ <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem _root_.LinearMapClass.ker_eq_bot : ker f = ⊥ ↔ Injective f

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
⊢ ker f = ⊥ ↔ Injective ⇑f

Tactic:
simpa [disjoint_iff_inf_le] using disjoint_ker' (f := f) (p := ⊤)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma map_ofHom (f : X ⟶ Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) [W.ContainsIdentities] :
    (ofHom W f).map L hL = L.map f

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
f : X ⟶ Y
L : C ⥤ D
hL : W.IsInvertedBy L
inst✝ : W.ContainsIdentities
⊢ (ofHom W f).map L hL = L.map f

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Topology/Compactness/LocallyCompact.lean
theorem compact_basis_nhds [LocallyCompactSpace X] (x : X) :
    (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsCompact s) fun s => s :=
  hasBasis_self.2 <| by simpa only [and_comm] using LocallyCompactSpace.local_compact_nhds x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, IsCompact r ∧ r ⊆ t

Tactic:
simpa only [and_comm] using LocallyCompactSpace.local_compact_nhds x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_self_assoc {m n : Nat} : min m (min m n) = min m n

Proof state:
m n : Nat
⊢ min m (min m n) = min m n

Tactic:
rw [← Nat.min_assoc, Nat.min_self]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem equivRealProd_apply_le (z : ℂ) : ‖equivRealProd z‖ ≤ ‖z‖

Proof state:
z : ℂ
⊢ ‖equivRealProd z‖ ≤ ‖z‖

Tactic:
simp [Prod.norm_def, abs_re_le_norm, abs_im_le_norm]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem image_setOf_minimal : f '' {x | Minimal (· ∈ s) x} = {x | Minimal (· ∈ f '' s) x} :=
  _root_.image_monotone_setOf_minimal (by simp [f.le_iff_le])

Proof state:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α ↪o β
⊢ ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals