harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_eq_discr (b : Basis ι ℤ A) (b' : Basis ι ℤ A) :
    Algebra.discr ℤ b = Algebra.discr ℤ b'

Proof state:
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b = discr ℤ ⇑b'

Tactic:
convert Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)

Result:
case h.e'_2.h.e'_9
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ ⇑b = ⇑b' ᵥ* (b'.toMatrix ⇑b).map ⇑(algebraMap ℤ A)

case h.e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Proof state:
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : (b'.toMatrix ⇑b).det ^ 2 = 1
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
rw [this, one_mul]

Result:
no goals

Proof state:
case h.e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit ((LinearMap.toMatrix b b') LinearMap.id).det

Tactic:
exact LinearEquiv.isUnit_det (LinearEquiv.refl ℤ A) b b'

Result:
no goals

Proof state:
case h.e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
suffices IsUnit (b'.toMatrix b).det by
  rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
  rw [this, one_mul]

Result:
case h.e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (b'.toMatrix ⇑b).det

Proof state:
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : IsUnit (b'.toMatrix ⇑b).det
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Tactic:
rw [Int.isUnit_iff, ← sq_eq_one_iff] at this

Result:
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
this : (b'.toMatrix ⇑b).det ^ 2 = 1
⊢ discr ℤ ⇑b' = (b'.toMatrix ⇑b).det ^ 2 * discr ℤ ⇑b'

Proof state:
case h.e'_2.h.e'_9
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ ⇑b = ⇑b' ᵥ* (b'.toMatrix ⇑b).map ⇑(algebraMap ℤ A)

Tactic:
rw [Basis.toMatrix_map_vecMul]

Result:
no goals

Proof state:
case h.e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (b'.toMatrix ⇑b).det

Tactic:
rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']

Result:
case h.e'_3
A : Type u
ι : Type w
inst✝² : DecidableEq ι
inst✝¹ : CommRing A
inst✝ : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit ((LinearMap.toMatrix b b') LinearMap.id).det
-- Mathlib/Algebra/Order/Ring/Canonical.lean
theorem mul_self_tsub_mul_self (a b : α) :
    a * a - b * b = (a + b) * (a - b)

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : AddLeftReflectLE α
a b : α
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
rw [mul_tsub, add_mul, add_mul, tsub_add_eq_tsub_tsub, mul_comm b a, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
lemma measurable_restrict_cylinderEvents (Δ : Set ι) :
    Measurable[cylinderEvents (π := π) Δ] (restrict Δ)

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
⊢ Measurable Δ.restrict

Tactic:
rw [@measurable_pi_iff]

Result:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
⊢ ∀ (a : ↑Δ), Measurable fun x => Δ.restrict x a

Proof state:
ι : Type u_2
π : ι → Type u_3
m : (i : ι) → MeasurableSpace (π i)
Δ : Set ι
⊢ ∀ (a : ↑Δ), Measurable fun x => Δ.restrict x a

Tactic:
exact fun i ↦ measurable_cylinderEvent_apply i.2

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/NormPow.lean
theorem hasDerivAt_norm_rpow (x : ℝ) {p : ℝ} (hp : 1 < p) :
    HasDerivAt (fun x : ℝ ↦ ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x

Proof state:
x p : ℝ
hp : 1 < p
⊢ HasDerivAt (fun x => ‖x‖ ^ p) (p * ‖x‖ ^ (p - 2) * x) x

Tactic:
convert hasFDerivAt_norm_rpow x hp |>.hasDerivAt using 1

Result:
case h.e'_9
x p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2) * x = ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) 1

Proof state:
case h.e'_9
x p : ℝ
hp : 1 < p
⊢ p * ‖x‖ ^ (p - 2) * x = ((p * ‖x‖ ^ (p - 2)) • (innerSL ℝ) x) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem map_normalClosure (s : Set G) (f : G →* N) (hf : Surjective f) :
    (normalClosure s).map f = normalClosure (f '' s)

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)

Tactic:
have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)

Tactic:
exact normalClosure_le_normal (Set.image_subset f subset_normalClosure)

Result:
no goals

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

Tactic:
simp [map_le_iff_le_comap, normalClosure_le_normal, coe_comap,
  ← Set.image_subset_iff, subset_normalClosure]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) = normalClosure (⇑f '' s)

Tactic:
apply le_antisymm

Result:
case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) ≤ normalClosure (⇑f '' s)

case a
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
hf : Surjective ⇑f
this : (map f (normalClosure s)).Normal
⊢ normalClosure (⇑f '' s) ≤ map f (normalClosure s)
-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
@[simp]
lemma ofSection_image {F' : Cᵒᵖ ⥤ Type w} (f : F ⟶ F') :
    (ofSection x).image f = ofSection (f.app _ x)

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ofSection (f.app X x) ≤ (ofSection x).image f

Tactic:
simp only [ofSection_le_iff, image_obj, Set.mem_image]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ∃ x_1 ∈ (ofSection x).obj X, f.app X x_1 = f.app X x

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ∃ x_1 ∈ (ofSection x).obj X, f.app X x_1 = f.app X x

Tactic:
exact ⟨x, mem_ofSection_obj x, rfl⟩

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ofSection x).image f ≤ ofSection (f.app X x)

Tactic:
rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ f.app X x ∈ (ofSection (f.app X x)).obj X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ofSection x).image f = ofSection (f.app X x)

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ofSection x).image f ≤ ofSection (f.app X x)

case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ofSection (f.app X x) ≤ (ofSection x).image f

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ f.app X x ∈ (ofSection (f.app X x)).obj X

Tactic:
exact ⟨𝟙 X, by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ F'.map (𝟙 X) (f.app X x) = f.app X x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2] (f1 : σ1)
    (f2 : σ2) (h : Liff α f1 f2) :
    Unsatisfiable α f1 ↔ Unsatisfiable α f2

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Liff α f1 f2
⊢ Unsatisfiable α f1 ↔ Unsatisfiable α f2

Tactic:
simp only [Liff] at h

Result:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : ∀ (a : α → Bool), a ⊨ f1 ↔ a ⊨ f2
⊢ Unsatisfiable α f1 ↔ Unsatisfiable α f2

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : ∀ (a : α → Bool), a ⊨ f1 ↔ a ⊨ f2
⊢ Unsatisfiable α f1 ↔ Unsatisfiable α f2

Tactic:
simp [Unsatisfiable, h]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
theorem mulShift_spec' (ψ : AddChar R M) (n : ℕ) (x : R) : mulShift ψ n x = ψ x ^ n

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
n : ℕ
x : R
⊢ (ψ.mulShift ↑n) x = ψ x ^ n

Tactic:
rw [mulShift_apply, ← nsmul_eq_mul, map_nsmul_eq_pow]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem le_of_pred_lt {a b : α} : pred a < b → a ≤ b := fun h ↦ by
  by_contra! nh
  exact le_pred_of_lt nh |>.trans_lt h |>.false

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a < b
nh : b < a
⊢ False

Tactic:
exact le_pred_of_lt nh |>.trans_lt h |>.false

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a < b
⊢ a ≤ b

Tactic:
by_contra! nh

Result:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a < b
nh : b < a
⊢ False
-- Mathlib/Data/Fin/Rev.lean
theorem lt_rev_iff {i j : Fin n} : i < rev j ↔ j < rev i

Proof state:
n : ℕ
i j : Fin n
⊢ i < j.rev ↔ j < i.rev

Tactic:
rw [← rev_lt_rev, rev_rev]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem natDegree_pos_of_eraseLead_ne_zero (h : f.eraseLead ≠ 0) : 0 < f.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
⊢ 0 < f.natDegree

Tactic:
by_contra h₂

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Tactic:
rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (C (f.coeff 0)).eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (C (f.coeff 0)).eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem one_mem_center : (1 : M) ∈ Set.center M where
  comm _

Proof state:
M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ x✝¹ * 1 * x✝ = x✝¹ * (1 * x✝)

Tactic:
rw [mul_one, one_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
x✝ : M
⊢ 1 * x✝ = x✝ * 1

Tactic:
rw [one_mul, mul_one]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * 1 = x✝¹ * (x✝ * 1)

Tactic:
rw [mul_one, mul_one]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
x✝¹ x✝ : M
⊢ 1 * (x✝¹ * x✝) = 1 * x✝¹ * x✝

Tactic:
rw [one_mul, one_mul]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem IsPositive.add {T S : E →L[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) :
    (T + S).IsPositive

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T S : E →L[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ (T + S).reApplyInnerSelf x

Tactic:
rw [reApplyInnerSelf, add_apply, inner_add_left, map_add]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T S : E →L[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ re ⟪T x, x⟫_𝕜 + re ⟪S x, x⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T S : E →L[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
⊢ (T + S).IsPositive

Tactic:
refine ⟨hT.isSelfAdjoint.add hS.isSelfAdjoint, fun x => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T S : E →L[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ (T + S).reApplyInnerSelf x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T S : E →L[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ re ⟪T x, x⟫_𝕜 + re ⟪S x, x⟫_𝕜

Tactic:
exact add_nonneg (hT.inner_nonneg_left x) (hS.inner_nonneg_left x)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem le_edist_of_le_infsep {d x} (hx : x ∈ s) {y} (hy : y ∈ s) (hxy : x ≠ y)
    (hd : d ≤ s.infsep) : d ≤ dist x y

Proof state:
case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : s.Subsingleton
⊢ d ≤ dist x y

Tactic:
rw [hs.infsep_zero] at hd

Result:
case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ 0
hs : s.Subsingleton
⊢ d ≤ dist x y

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
⊢ d ≤ dist x y

Tactic:
by_cases hs : s.Nontrivial

Result:
case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : s.Nontrivial
⊢ d ≤ dist x y

case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : ¬s.Nontrivial
⊢ d ≤ dist x y

Proof state:
case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ 0
hs : s.Subsingleton
⊢ d ≤ dist x y

Tactic:
exact le_trans hd dist_nonneg

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : ¬s.Nontrivial
⊢ d ≤ dist x y

Tactic:
rw [not_nontrivial_iff] at hs

Result:
case neg
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : s.Subsingleton
⊢ d ≤ dist x y

Proof state:
case pos
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
hs : s.Nontrivial
⊢ d ≤ dist x y

Tactic:
exact hs.le_infsep_iff.1 hd x hx y hy hxy

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem coe_toIocMod (θ ψ : ℝ) : ↑(toIocMod two_pi_pos ψ θ) = (θ : Angle)

Proof state:
θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Tactic:
refine ⟨-toIocDiv two_pi_pos ψ θ, ?_⟩

Result:
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)

Proof state:
θ ψ : ℝ
⊢ ↑(toIocMod two_pi_pos ψ θ) = ↑θ

Tactic:
rw [angle_eq_iff_two_pi_dvd_sub]

Result:
θ ψ : ℝ
⊢ ∃ k, toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑k

Proof state:
θ ψ : ℝ
⊢ toIocMod two_pi_pos ψ θ - θ = 2 * π * ↑(-toIocDiv two_pi_pos ψ θ)

Tactic:
rw [toIocMod_sub_self, zsmul_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk_cancel (s : S) (m : M) : mk (s • m) s = mk m 1 :=
  mk_eq.mpr ⟨1, by simp⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ 1 • 1 • s • m = 1 • s • m

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
theorem comp_distTriang_mor_zero₁₂ (T) (H : T ∈ (distTriang C)) : T.mor₁ ≫ T.mor₂ = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
obtain ⟨c, hc⟩ :=
  complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁)
    T.mor₁ rfl

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_whiskerRight_comp_evaluation {X Y : C} [HasLeftDual X] [HasLeftDual Y]
    (f : X ⟶ Y) : (tensorLeftHomEquiv _ _ _ _) (f ▷ _ ≫ ε_ _ _) = (ᘁf) ≫ (ρ_ _).inv

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (ᘁY) (ᘁX) X (𝟙_ C)) (f ▷ ᘁY ≫ ε_ (ᘁY) Y) = (ᘁf) ≫ (ρ_ ᘁX).inv

Tactic:
dsimp [tensorLeftHomEquiv, leftAdjointMate]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (α_ (ᘁX) X ᘁY).hom ≫ ᘁX ◁ (f ▷ ᘁY ≫ ε_ (ᘁY) Y) =
    ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ≫ (ρ_ ᘁX).inv

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (α_ (ᘁX) X ᘁY).hom ≫ ᘁX ◁ (f ▷ ᘁY ≫ ε_ (ᘁY) Y) =
    ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom) ≫ (ρ_ ᘁX).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
theorem liftNormedAddGroupHom_normNoninc {N : Type*} [SeminormedAddCommGroup N]
    (f : NormedAddGroupHom M N) (hf : ∀ s, ‖s‖ = 0 → f s = 0) (fb : f.NormNoninc) :
    (liftNormedAddGroupHom f hf).NormNoninc := fun x => by
  have fb' : ‖f‖ ≤ 1 := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb
  exact le_trans (norm_liftNormedAddGroupHom_apply_le f hf x)
    (mul_le_of_le_one_left (norm_nonneg x) fb')

Proof state:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → f s = 0
fb : f.NormNoninc
x : SeparationQuotient M
⊢ ‖(liftNormedAddGroupHom f hf) x‖ ≤ ‖x‖

Tactic:
have fb' : ‖f‖ ≤ 1 := NormedAddGroupHom.NormNoninc.normNoninc_iff_norm_le_one.mp fb

Result:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → f s = 0
fb : f.NormNoninc
x : SeparationQuotient M
fb' : ‖f‖ ≤ 1
⊢ ‖(liftNormedAddGroupHom f hf) x‖ ≤ ‖x‖

Proof state:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (s : M), ‖s‖ = 0 → f s = 0
fb : f.NormNoninc
x : SeparationQuotient M
fb' : ‖f‖ ≤ 1
⊢ ‖(liftNormedAddGroupHom f hf) x‖ ≤ ‖x‖

Tactic:
exact le_trans (norm_liftNormedAddGroupHom_apply_le f hf x)
  (mul_le_of_le_one_left (norm_nonneg x) fb')

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem IsIntegral.inv_mem_adjoin (int : IsIntegral R x) : x⁻¹ ∈ adjoin R {x}

Proof state:
case inr
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional R ↥(adjoin R {x})
⊢ x⁻¹ ∈ adjoin R {x}

Tactic:
obtain ⟨⟨y, hy⟩, h1⟩ := FiniteDimensional.exists_mul_eq_one R
  (K := adjoin R {x}) (x := ⟨x, subset_adjoin rfl⟩) (mt Subtype.ext_iff.mp h0)

Result:
case inr.intro.mk
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional R ↥(adjoin R {x})
y : S
hy : y ∈ adjoin R {x}
h1 : ⟨x, ⋯⟩ * ⟨y, hy⟩ = 1
⊢ x⁻¹ ∈ adjoin R {x}

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
⊢ x⁻¹ ∈ adjoin R {x}

Tactic:
obtain rfl | h0 := eq_or_ne x 0

Result:
case inl
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
int : IsIntegral R 0
⊢ 0⁻¹ ∈ adjoin R {0}

case inr
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
⊢ x⁻¹ ∈ adjoin R {x}

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
int : IsIntegral R 0
⊢ 0⁻¹ ∈ adjoin R {0}

Tactic:
rw [inv_zero]

Result:
case inl
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
int : IsIntegral R 0
⊢ 0 ∈ adjoin R {0}

Proof state:
case inr.intro.mk
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional R ↥(adjoin R {x})
y : S
hy : y ∈ adjoin R {x}
h1 : ⟨x, ⋯⟩ * ⟨y, hy⟩ = 1
⊢ x⁻¹ ∈ adjoin R {x}

Tactic:
rwa [← mul_left_cancel₀ h0 ((Subtype.ext_iff.mp h1).trans (mul_inv_cancel₀ h0).symm)]

Result:
no goals

Proof state:
case inr
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
⊢ x⁻¹ ∈ adjoin R {x}

Tactic:
have : FiniteDimensional R (adjoin R {x}) := ⟨(Submodule.fg_top _).mpr int.fg_adjoin_singleton⟩

Result:
case inr
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional R ↥(adjoin R {x})
⊢ x⁻¹ ∈ adjoin R {x}

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
int : IsIntegral R 0
⊢ 0 ∈ adjoin R {0}

Tactic:
exact Subalgebra.zero_mem _

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma norm (hf : GrowsPolynomially f) : GrowsPolynomially (fun x => ‖f x‖)

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x => ‖f x‖

Tactic:
simp only [norm_eq_abs]

Result:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x => |f x|

Proof state:
f : ℝ → ℝ
hf : GrowsPolynomially f
⊢ GrowsPolynomially fun x => |f x|

Tactic:
exact hf.abs

Result:
no goals