harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk (p : R[X]) :
    (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
        (Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X]))
        (p.map (Ideal.Quotient.mk I))) =
      Ideal.Quotient.mk (I.map (of f)) (mk f p)

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
f p : R[X]
⊢ (quotAdjoinRootEquivQuotPolynomialQuot I f).symm
      ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) p)) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) p)

Tactic:
rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply,
  RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply, RingEquiv.symm_symm,
  Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk, ←
  RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
  quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk,
  quotMapOfEquivQuotMapCMapSpanMk_symm_mk]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
lemma natCast_cpow_natCast_mul (n m : ℕ) (z : ℂ) : (n : ℂ) ^ (m * z) = ((n : ℂ) ^ m) ^ z

Proof state:
n m : ℕ
z : ℂ
⊢ ↑n ^ (↑m * z) = (↑n ^ m) ^ z

Tactic:
refine cpow_nat_mul' (x := n) (n := m) ?_ ?_ z

Result:
case refine_1
n m : ℕ
z : ℂ
⊢ -π < ↑m * (↑n).arg

case refine_2
n m : ℕ
z : ℂ
⊢ ↑m * (↑n).arg ≤ π

Proof state:
case refine_1
n m : ℕ
z : ℂ
⊢ -π < ↑m * (↑n).arg

Tactic:
simp only [natCast_arg, mul_zero, Left.neg_neg_iff, pi_pos]

Result:
no goals

Proof state:
case refine_2
n m : ℕ
z : ℂ
⊢ ↑m * (↑n).arg ≤ π

Tactic:
simp only [natCast_arg, mul_zero, pi_pos.le]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_pos_left (h : SameRay R x y) (hx : x ≠ 0) (hy : y ≠ 0) :
    ∃ r : R, 0 < r ∧ r • x = y :=
  let ⟨r₁, r₂, hr₁, hr₂, h⟩ := h.exists_pos hx hy
  ⟨r₂⁻¹ * r₁, mul_pos (inv_pos.2 hr₂) hr₁, by rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']⟩

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h✝ : SameRay R x y
hx : x ≠ 0
hy : y ≠ 0
r₁ r₂ : R
hr₁ : 0 < r₁
hr₂ : 0 < r₂
h : r₁ • x = r₂ • y
⊢ (r₂⁻¹ * r₁) • x = y

Tactic:
rw [mul_smul, h, inv_smul_smul₀ hr₂.ne']

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_ball' : y ∈ ball x ε ↔ edist x y < ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ ball x ε ↔ edist x y < ε

Tactic:
rw [edist_comm, mem_ball]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The product of the prime factors of `n` that are in `s` is an `s`-factored number. -/
lemma prod_mem_factoredNumbers (s : Finset ℕ) (n : ℕ) :
    (n.primeFactorsList.filter (· ∈ s)).prod ∈ factoredNumbers s

Proof state:
case intro
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
H₁ : Prime p
H₂ : p ∣ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod
⊢ p ∈ s

Tactic:
simpa only [decide_eq_true_eq] using List.of_mem_filter <| mem_list_primes_of_dvd_prod H₁.prime
  (fun _ hq ↦ (prime_of_mem_primeFactorsList (List.mem_of_mem_filter hq)).prime) H₂

Result:
no goals

Proof state:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
⊢ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ∈ factoredNumbers s

Tactic:
refine ⟨h₀, fun p hp ↦ ?_⟩

Result:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
⊢ p ∈ s

Proof state:
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
⊢ p ∈ s

Tactic:
obtain ⟨H₁, H₂⟩ := (mem_primeFactorsList h₀).mp hp

Result:
case intro
s : Finset ℕ
n : ℕ
h₀ : (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod ≠ 0
p : ℕ
hp : p ∈ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod.primeFactorsList
H₁ : Prime p
H₂ : p ∣ (List.filter (fun x => decide (x ∈ s)) n.primeFactorsList).prod
⊢ p ∈ s
-- Mathlib/Topology/Instances/Rat.lean
theorem Nat.isClosedEmbedding_coe_rat : IsClosedEmbedding ((↑) : ℕ → ℚ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist

Proof state:
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y

Tactic:
simpa using Nat.pairwise_one_le_dist

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_one : logMap (1 : mixedSpace K) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ logMap 1 = 0

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 1 x✝ = 0 x✝

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 1 x✝ = 0 x✝

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean
theorem _root_.Finset.sum_single_ite [Fintype n] (a : R) (i : n) :
    (∑ x : n, Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a

Proof state:
R : Type u_1
n : Type u_3
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : Fintype n
a : R
i : n
⊢ ∑ x : n, Finsupp.single x (if i = x then a else 0) = Finsupp.single i a

Tactic:
simp only [apply_ite (Finsupp.single _), Finsupp.single_zero, Finset.sum_ite_eq,
  if_pos (Finset.mem_univ _)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_one_add_measure (f : α → F) (μ ν : Measure α) :
    eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
μ ν : Measure α
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
rw [lintegral_add_measure _ μ ν]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
μ ν : Measure α
⊢ eLpNorm f 1 (μ + ν) = eLpNorm f 1 μ + eLpNorm f 1 ν

Tactic:
simp_rw [eLpNorm_one_eq_lintegral_enorm]

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
f : α → F
μ ν : Measure α
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂(μ + ν) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ + ∫⁻ (x : α), ‖f x‖ₑ ∂ν
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_lt_rpow_iff_of_pos (hx : 0 < x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0

Proof state:
x y : ℝ
hx : 0 < x
⊢ 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0

Tactic:
rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx.le, log_neg_iff hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_ro (u w v k : Nat) : u ≤ w → w ≤ v + k → u ≤ v + k

Proof state:
u w v k : Nat
⊢ u ≤ w → w ≤ v + k → u ≤ v + k

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem contDiff {n : ℕ∞} : ContDiff ℝ n expNegInvGlue

Proof state:
n : ℕ∞
⊢ ContDiff ℝ (↑n) expNegInvGlue

Tactic:
simpa using contDiff_polynomial_eval_inv_mul 1

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem mem_falling : s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Proof state:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ i ∈ 𝒜, s ⊆ i ∧ #s = k) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

Tactic:
simp_rw [falling, mem_sup, mem_powersetCard]

Result:
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
⊢ (∃ i ∈ 𝒜, s ⊆ i ∧ #s = k) ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ioc_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_pow (b x : ℕ) (hb : 1 < b) : clog b (b ^ x) = x :=
  eq_of_forall_ge_iff fun z ↦ by rw [← le_pow_iff_clog_le hb, Nat.pow_le_pow_iff_right hb]

Proof state:
b x : ℕ
hb : 1 < b
z : ℕ
⊢ clog b (b ^ x) ≤ z ↔ x ≤ z

Tactic:
rw [← le_pow_iff_clog_le hb, Nat.pow_le_pow_iff_right hb]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix'_id : LinearMap.toMatrix' (LinearMap.id : (n → R) →ₗ[R] n → R) = 1

Proof state:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = 1 i✝ j✝

Tactic:
rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ toMatrix' id = 1

Tactic:
ext

Result:
case a
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = 1 i✝ j✝
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_union_Ioc (h : min c d < b) : Iic b ∪ Ioc c d = Iic (max b d)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (d ⊔ b)

Tactic:
simp [*, max_eq_right_of_lt h]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c < b
⊢ Iic b ∪ Ioc c d = Iic (b ⊔ d)

Tactic:
exact Iic_union_Ioc' h

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (b ⊔ d)

Tactic:
rw [max_comm]

Result:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (d ⊔ b)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : c ⊓ d < b
⊢ Iic b ∪ Ioc c d = Iic (b ⊔ d)

Tactic:
rcases le_total c d with hcd | hcd <;> simp [hcd] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c < b
⊢ Iic b ∪ Ioc c d = Iic (b ⊔ d)

case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d ≤ c
h : d < b
⊢ Iic b ∪ Ioc c d = Iic (b ⊔ d)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_eq_right_iff_dvd : m ∣ n ↔ gcd n m = m

Proof state:
m n : Nat
⊢ m ∣ n ↔ m.gcd n = m

Tactic:
exact gcd_eq_left_iff_dvd

Result:
no goals

Proof state:
m n : Nat
⊢ m ∣ n ↔ n.gcd m = m

Tactic:
rw [gcd_comm]

Result:
m n : Nat
⊢ m ∣ n ↔ m.gcd n = m
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma associative_ε₂_ε₁ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
    ε₂ c₁ c₂₃ c (i₁, π c₂ c₃ c₂₃ (i₂, i₃)) * ε₁ c₂ c₃ c₂₃ (i₂, i₃) =
      ε₁ c₁₂ c₃ c (π c₁ c₂ c₁₂ (i₁, i₂), i₃) * ε₂ c₁ c₂ c₁₂ (i₁, i₂)

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
    c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
apply Associative.ε₂_ε₁

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem inv_left_hom_right [IsIso sq] : inv sq.left ≫ f.hom ≫ sq.right = g.hom

Proof state:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ inv sq.left ≫ f.hom ≫ sq.right = g.hom

Tactic:
simp only [w, IsIso.inv_comp_eq]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem eval_maximal {σ} {f : σ → Option σ} {a b} (h : b ∈ eval f a) {c} : Reaches f b c ↔ c = b :=
  let ⟨_, b0⟩ := mem_eval.1 h
  reflTransGen_iff_eq fun b' h' ↦ by cases b0.symm.trans h'

Proof state:
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
c : σ
left✝ : Reaches f a b
b0 : f b = none
b' : σ
h' : b' ∈ f b
⊢ False

Tactic:
cases b0.symm.trans h'

Result:
no goals
-- Mathlib/Topology/Sets/OpenCover.lean
lemma iSup_set_eq_univ (hu : IsOpenCover u) : ⋃ i, (u i : Set X) = univ

Proof state:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
⊢ ⋃ i, ↑(u i) = univ

Tactic:
simpa [← SetLike.coe_set_eq] using hu.iSup_eq_top

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem restrictScalars_adjoin_eq_sup (K : IntermediateField F E) (S : Set E) :
    restrictScalars F (adjoin K S) = K ⊔ adjoin F S

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = K ⊔ adjoin F S

Tactic:
rw [restrictScalars_adjoin, adjoin_union, adjoin_self]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem exists_iff_ne_zero {p : G₀ → Prop} : (∃ u : G₀ˣ, p u) ↔ ∃ x ≠ 0, p x

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
p : G₀ → Prop
⊢ (∃ u, p ↑u) ↔ ∃ x, x ≠ 0 ∧ p x

Tactic:
simp [exists0]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem orderTop_neg {x : HahnSeries Γ R} : (-x).orderTop = x.orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : HahnSeries Γ R
⊢ (-x).orderTop = x.orderTop

Tactic:
simp only [orderTop, support_neg, neg_eq_zero]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : HahnSeries Γ R
⊢ (-x).orderTop = x.orderTop

Tactic:
classical simp only [orderTop, support_neg, neg_eq_zero]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_bitm1 (n : ZNum) : -n.bitm1 = (-n).bit1

Proof state:
n : ZNum
⊢ -n.bitm1 = (-n).bit1

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem coe_dvd : ↑u ∣ a :=
  ⟨↑u⁻¹ * a, by simp⟩

Proof state:
α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ a = ↑u * (↑u⁻¹ * a)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Basic.lean
theorem map_dite (F : C ⥤ D) {X Y : C} {P : Prop} [Decidable P]
    (f : P → (X ⟶ Y)) (g : ¬P → (X ⟶ Y)) :
    F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
P : Prop
inst✝ : Decidable P
f : P → (X ⟶ Y)
g : ¬P → (X ⟶ Y)
⊢ F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem Metric.inseparable_iff_nndist {x y : α} : Inseparable x y ↔ nndist x y = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ nndist x y = 0

Tactic:
rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_of_im_nonneg_of_ne_zero {z : ℂ} (h₁ : 0 ≤ z.im) (h₂ : z ≠ 0) :
    arg z = Real.arccos (z.re / ‖z‖)

Proof state:
z : ℂ
h₁ : 0 ≤ z.im
h₂ : z ≠ 0
⊢ z.arg = Real.arccos (z.re / ‖z‖)

Tactic:
rw [← cos_arg h₂, Real.arccos_cos (arg_nonneg_iff.2 h₁) (arg_le_pi _)]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma functorEnriched_id_comp [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₁ F₁] :
    (λ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedId V F₁ ▷ functorEnrichedHom V F₁ F₂ ≫
        functorEnrichedComp V F₁ F₁ F₂ = 𝟙 (functorEnrichedHom V F₁ F₂)

Proof state:
V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasFunctorEnrichedHom V F₁ F₂
inst✝ : HasFunctorEnrichedHom V F₁ F₁
⊢ (λ_ (functorEnrichedHom V F₁ F₂)).inv ≫
      functorEnrichedId V F₁ ▷ functorEnrichedHom V F₁ F₂ ≫ functorEnrichedComp V F₁ F₁ F₂ =
    𝟙 (functorEnrichedHom V F₁ F₂)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Analysis/Fourier/ZMod.lean
/--
The discrete Fourier transform agrees with the general one (assuming the target space is a complete
normed space).
-/
lemma dft_eq_fourier {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
    (Φ : ZMod N → E) (k : ZMod N) :
    𝓕 Φ k = Fourier.fourierIntegral toCircle Measure.count Φ k

Proof state:
N : ℕ
inst✝³ : NeZero N
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
Φ : ZMod N → E
k : ZMod N
⊢ 𝓕 Φ k = Fourier.fourierIntegral toCircle Measure.count Φ k

Tactic:
simp only [dft_apply, stdAddChar_apply, Fourier.fourierIntegral_def, Circle.smul_def,
  integral_countable' <| .of_finite .., Measure.count_singleton, ENNReal.one_toReal, one_smul,
  tsum_fintype]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_eq_zero : toNNRat q = 0 ↔ q ≤ 0

Proof state:
q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0

Tactic:
simpa [-toNNRat_pos] using (@toNNRat_pos q).not

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem Matrix.toLinearMap₂'_apply (M : Matrix n m N₂) (x : n → S₁) (y : m → S₂) :
    -- porting note: we don't seem to have `∑ i j` as valid notation yet
    Matrix.toLinearMap₂' R M x y = ∑ i, ∑ j, x i • y j • M i j :=
  Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by
    rw [RingHom.id_apply, RingHom.id_apply, smul_comm]

Proof state:
R : Type u_1
S₁ : Type u_3
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid N₂
inst✝¹¹ : Module R N₂
inst✝¹⁰ : Semiring S₁
inst✝⁹ : Semiring S₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
M : Matrix n m N₂
x : n → S₁
y : m → S₂
x✝³ : n
x✝² : x✝³ ∈ univ
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ (RingHom.id S₂) (y x✝¹) •> (RingHom.id S₁) (x x✝³) •> M x✝³ x✝¹ = x x✝³ •> y x✝¹ •> M x✝³ x✝¹

Tactic:
rw [RingHom.id_apply, RingHom.id_apply, smul_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem measure_closedBall_le_integral : (μ (closedBall c f.rIn)).toReal ≤ ∫ x, f x ∂μ

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ (μ (closedBall c f.rIn)).toReal = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
⊢ (μ (closedBall c f.rIn)).toReal ≤ ∫ (x : E), ↑f x ∂μ

Tactic:
calc
(μ (closedBall c f.rIn)).toReal = ∫ x in closedBall c f.rIn, 1 ∂μ := by simp
_ = ∫ x in closedBall c f.rIn, f x ∂μ := setIntegral_congr_fun measurableSet_closedBall
(fun x hx ↦ (one_of_mem_closedBall f hx).symm)
_ ≤ ∫ x, f x ∂μ := setIntegral_le_integral f.integrable (Eventually.of_forall (fun x ↦ f.nonneg))

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_self_mul_right (a b : E) : dist a (a * b) = ‖b‖

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (a * b) = ‖b‖

Tactic:
rw [← dist_one_left, ← dist_mul_left a 1 b, mul_one]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nonempty (a b : Ordinal.{u}) :
    {c : Ordinal.{u} | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}.Nonempty

Proof state:
case intro
a b c : Ordinal.{u}
hc : c ∈ upperBounds ((fun x => x.1 ⨳ b ♯ a ⨳ x.2) '' Iio a ×ˢ Iio b)
⊢ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}.Nonempty

Tactic:
exact ⟨_, fun x hx y hy ↦
  (lt_succ_of_le <| hc <| Set.mem_image_of_mem _ <| Set.mk_mem_prod hx hy).trans_le le_self_nadd⟩

Result:
no goals

Proof state:
a b : Ordinal.{u}
⊢ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}.Nonempty

Tactic:
obtain ⟨c, hc⟩ : BddAbove ((fun x ↦ x.1 ⨳ b ♯ a ⨳ x.2) '' Set.Iio a ×ˢ Set.Iio b) :=
  bddAbove_of_small _

Result:
case intro
a b c : Ordinal.{u}
hc : c ∈ upperBounds ((fun x => x.1 ⨳ b ♯ a ⨳ x.2) '' Iio a ×ˢ Iio b)
⊢ {c | ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'}.Nonempty
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sub_left {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x z - o.oangle x y = o.oangle y z

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x z - o.oangle x y = o.oangle y z

Tactic:
rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz]

Result:
no goals
-- Mathlib/Algebra/Lie/OfAssociative.lean
/-- Given an equivalence `e` of Lie algebras from `L` to `L'`, and an element `x : L`, the conjugate
of the endomorphism `ad(x)` of `L` by `e` is the endomorphism `ad(e x)` of `L'`. -/
@[simp]
lemma conj_ad_apply (e : L ≃ₗ⁅R⁆ L') (x : L) : LinearEquiv.conj e (ad R L x) = ad R L' (e x)

Proof state:
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
⊢ e.toLinearEquiv.conj ((ad R L) x) = (ad R L') (e x)

Tactic:
ext y'

Result:
case h
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ (e.toLinearEquiv.conj ((ad R L) x)) y' = ((ad R L') (e x)) y'

Proof state:
case h
R : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ (e.toLinearEquiv.conj ((ad R L) x)) y' = ((ad R L') (e x)) y'

Tactic:
rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
  ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
theorem ne_bot_iff_nonempty (U : Opens α) : U ≠ ⊥ ↔ Set.Nonempty (U : Set α)

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ U ≠ ⊥ ↔ (↑U).Nonempty

Tactic:
rw [Ne, ← not_nonempty_iff_eq_bot, not_not]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_mul_self_apply_self [NonAssocSemiring α] (i : V) :
    (G.adjMatrix α * G.adjMatrix α) i i = degree G i

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
i : V
⊢ (adjMatrix α G * adjMatrix α G) i i = ↑(G.degree i)

Tactic:
simp [filter_true_of_mem]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q)
    (hPz : P z ≠ 0) (hQz : Q z = 0) : W'.add P Q = -(Q y ^ 2 * P z) • P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
⊢ W'.add P Q = -(Q y ^ 2 * P z) • P

Tactic:
rw [add, if_neg <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]

Result:
no goals