harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_ideal_over_prime_of_isIntegral_of_isDomain [Algebra.IsIntegral R S] (P : Ideal R)
    [IsPrime P] (hP : RingHom.ker (algebraMap R S) ≤ P) :
    ∃ Q : Ideal S, IsPrime Q ∧ Q.comap (algebraMap R S) = P

Proof state:
case h.e'_2
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
Sₚ : Type u_2 := Localization (Algebra.algebraMapSubmonoid S P.primeCompl)
this✝ : IsDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) :=
  IsLocalization.isDomain_localization (le_nonZeroDivisors_of_noZeroDivisors hP0)
Qₚ : Ideal Sₚ
Qₚ_maximal : Qₚ.IsMaximal
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this : Algebra.IsIntegral Rₚ Sₚ
Qₚ_max : (comap (algebraMap Rₚ Sₚ) Qₚ).IsMaximal
⊢ comap ((IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)) Qₚ =
    comap (algebraMap R (Localization.AtPrime P)) (comap (algebraMap Rₚ Sₚ) Qₚ)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P

Tactic:
let Rₚ := Localization P.primeCompl

Result:
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : Algebra.IsIntegral R S
P : Ideal R
inst✝ : P.IsPrime
hP : RingHom.ker (algebraMap R S) ≤ P
hP0 : 0 ∉ Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization P.primeCompl
⊢ ∃ Q, Q.IsPrime ∧ comap (algebraMap R S) Q = P
-- Mathlib/NumberTheory/Divisors.lean
theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
    x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j

Proof state:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1, (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
simp only [exists_prop, and_assoc]

Result:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j

Proof state:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1 ≤ k, x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j < k, x = p ^ j

Tactic:
apply exists_congr

Result:
case h
p : ℕ
pp : Prime p
k x : ℕ
⊢ ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a

Proof state:
case h.mpr.intro
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ a < k

Tactic:
simp [h_left, le_of_lt]

Result:
no goals

Proof state:
case h.mp
p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k
⊢ a < k ∧ x = p ^ a

Tactic:
rcases h with ⟨_h_left, rfl, h_right⟩

Result:
case h.mp.intro.intro
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : p ^ a < p ^ k
⊢ a < k ∧ p ^ a = p ^ a

Proof state:
case h.mp.intro.intro
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : p ^ a < p ^ k
⊢ a < k ∧ p ^ a = p ^ a

Tactic:
rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right

Result:
case h.mp.intro.intro
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ a < k ∧ p ^ a = p ^ a

Proof state:
case h.mpr.intro
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k

Tactic:
rw [Nat.pow_lt_pow_iff_right pp.one_lt]

Result:
case h.mpr.intro
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ a < k

Proof state:
case h.mpr
p : ℕ
pp : Prime p
k x a : ℕ
h : a < k ∧ x = p ^ a
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k

Tactic:
rcases h with ⟨h_left, rfl⟩

Result:
case h.mpr.intro
p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k

Proof state:
p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Tactic:
rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]

Result:
p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1, (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ j, ∃ (_ : j < k), x = p ^ j

Proof state:
case h
p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a

Tactic:
constructor <;> intro h

Result:
case h.mp
p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k
⊢ a < k ∧ x = p ^ a

case h.mpr
p : ℕ
pp : Prime p
k x a : ℕ
h : a < k ∧ x = p ^ a
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k

Proof state:
case h.mp.intro.intro
p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ a < k ∧ p ^ a = p ^ a

Tactic:
exact ⟨h_right, rfl⟩

Result:
no goals

Proof state:
case h
p : ℕ
pp : Prime p
k x : ℕ
⊢ ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a

Tactic:
intro a

Result:
case h
p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem eval_indicator_apply_eq_one (a : σ → K) : eval a (indicator a) = 1

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
a✝ : Nontrivial K
⊢ (eval a) (indicator a) = 1

Tactic:
have : 0 < Fintype.card K - 1 := tsub_pos_of_lt Fintype.one_lt_card

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
a✝ : Nontrivial K
this : 0 < Fintype.card K - 1
⊢ (eval a) (indicator a) = 1

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
⊢ (eval a) (indicator a) = 1

Tactic:
nontriviality

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
a✝ : Nontrivial K
⊢ (eval a) (indicator a) = 1

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
a : σ → K
a✝ : Nontrivial K
this : 0 < Fintype.card K - 1
⊢ (eval a) (indicator a) = 1

Tactic:
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self,
  zero_pow this.ne', sub_zero, Finset.prod_const_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem Convex.isLittleO_alternate_sum_square {v w : E} (h4v : x + (4 : ℝ) • v ∈ interior s)
    (h4w : x + (4 : ℝ) • w ∈ interior s) :
    (fun h : ℝ => f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w))
        - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) - h ^ 2 • f'' v w) =o[𝓝[>] 0]
      fun h => h ^ 2

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h =>
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h => h ^ 2
TA2 :
  (fun h =>
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h => h ^ 2
⊢ (fun h =>
      f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w) =o[𝓝[>] 0]
    fun h => h ^ 2

Tactic:
convert TA1.sub TA2 using 1

Result:
case h.e'_7
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
h4v : x + 4 • v ∈ interior s
h4w : x + 4 • w ∈ interior s
A : 1 / 2 ∈ Ioc 0 1
B : 1 / 2 ∈ Icc 0 1
h2v2w : x + 2 • v + 2 • w ∈ interior s
h2vww : x + (2 • v + w) + w ∈ interior s
h2v : x + 2 • v ∈ interior s
h2w : x + 2 • w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (2 • v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  (fun h =>
      f (x + h • (2 • v + w) + h • w) - f (x + h • (2 • v + w)) - h • (f' x) w - h ^ 2 • (f'' (2 • v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h => h ^ 2
TA2 :
  (fun h =>
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - h • (f' x) w - h ^ 2 • (f'' (v + w)) w -
        (h ^ 2 / 2) • (f'' w) w) =o[𝓝[>] 0]
    fun h => h ^ 2
⊢ (fun h =>
      f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) -
        h ^ 2 • (f'' v) w) =
    fun x_1 =>
    f (x + x_1 • (2 • v + w) + x_1 • w) - f (x + x_1 • (2 • v + w)) - x_1 • (f' x) w - x_1 ^ 2 • (f'' (2 • v + w)) w -
        (x_1 ^ 2 / 2) • (f'' w) w -
      (f (x + x_1 • (v + w) + x_1 • w) - f (x + x_1 • (v + w)) - x_1 • (f' x) w - x_1 ^ 2 • (f'' (v + w)) w -
        (x_1 ^ 2 / 2) • (f'' w) w)
-- Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean
theorem measure_eq [mα : MeasurableSpace α] (m : AddContent C) (hC : IsSetSemiring C)
    (hC_gen : mα = MeasurableSpace.generateFrom C) (m_sigma_subadd : m.IsSigmaSubadditive)
    (hs : s ∈ C) :
    m.measure hC hC_gen.le m_sigma_subadd s = m s

Proof state:
case hs
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ MeasurableSet s

Tactic:
apply MeasurableSpace.measurableSet_generateFrom hs

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (m.measureCaratheodory hC m_sigma_subadd) s = m s

Tactic:
exact m.measureCaratheodory_eq hC m_sigma_subadd hs

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (m.measure hC ⋯ m_sigma_subadd) s = m s

Tactic:
rw [measure, trim_measurableSet_eq]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ (m.measureCaratheodory hC m_sigma_subadd) s = m s

case hs
α : Type u_1
C : Set (Set α)
s : Set α
mα : MeasurableSpace α
m : AddContent C
hC : IsSetSemiring C
hC_gen : mα = MeasurableSpace.generateFrom C
m_sigma_subadd : m.IsSigmaSubadditive
hs : s ∈ C
⊢ MeasurableSet s
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovEDist_triangle [OpensMeasurableSpace Ω] (μ ν κ : Measure Ω) :
    levyProkhorovEDist μ κ ≤ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal

Tactic:
rw [← hs_add_r, ← ENNReal.toReal_add]

Result:
case ha
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ s ≠ ⊤

case hb
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤
LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
half_ε_lt_top : ε / 2 < ⊤
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
⊢ r ≠ ⊤
-- Mathlib/Algebra/Order/UpperLower.lean
theorem IsUpperSet.div_left (ht : IsUpperSet t) : IsLowerSet (s / t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s / t)

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
ht : IsUpperSet t
⊢ IsLowerSet (s * t⁻¹)

Tactic:
exact ht.inv.mul_left

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_inv_of_pos {x : ℝ} (h : 0 < x) : arctan x⁻¹ = π / 2 - arctan x

Proof state:
case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2

Tactic:
rw [sub_lt_self_iff, ← arctan_zero]

Result:
case hx₂
x : ℝ
h : 0 < x
⊢ arctan 0 < arctan x

Proof state:
case hx₁
x : ℝ
h : 0 < x
⊢ arctan x < π

Tactic:
exact (arctan_lt_pi_div_two x).trans (half_lt_self_iff.mpr pi_pos)

Result:
no goals

Proof state:
case hx₂
x : ℝ
h : 0 < x
⊢ arctan 0 < arctan x

Tactic:
exact tanOrderIso.symm.strictMono h

Result:
no goals

Proof state:
case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

Tactic:
norm_num

Result:
case hx₁
x : ℝ
h : 0 < x
⊢ arctan x < π

Proof state:
x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = π / 2 - arctan x

Tactic:
rw [← arctan_tan (x := _ - _), tan_pi_div_two_sub, tan_arctan]

Result:
case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.equiv_mk0 [IsDedekindDomain R] (I : (Ideal R)⁰) :
    ClassGroup.equiv K (ClassGroup.mk0 I) =
      QuotientGroup.mk' (toPrincipalIdeal R K).range (FractionalIdeal.mk0 K I)

Proof state:
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (equiv K) (mk0 I) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)

Tactic:
rw [ClassGroup.mk0, MonoidHom.comp_apply, ClassGroup.equiv_mk]

Result:
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (QuotientGroup.mk' (toPrincipalIdeal R K).range)
      ((Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) ((FractionalIdeal.mk0 (FractionRing R)) I)) =
    (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)

Proof state:
case h.e_6.h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) ((FractionalIdeal.mk0 (FractionRing R)) I) =
    (FractionalIdeal.mk0 K) I

Tactic:
simp [← Units.eq_iff]

Result:
no goals

Proof state:
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (QuotientGroup.mk' (toPrincipalIdeal R K).range)
      ((Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) ((FractionalIdeal.mk0 (FractionRing R)) I)) =
    (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)

Tactic:
congr 1

Result:
case h.e_6.h
R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (Units.mapEquiv ↑(canonicalEquiv R⁰ (FractionRing R) K)) ((FractionalIdeal.mk0 (FractionRing R)) I) =
    (FractionalIdeal.mk0 K) I
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_smul_const (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
    derivWithin (fun y => c y • f) s x = derivWithin c s x • f

Proof state:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y • f) s x = derivWithin c s x • f

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y • f) s x = derivWithin c s x • f

Tactic:
exact (hc.hasDerivWithinAt.smul_const f).derivWithin hxs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
⊢ derivWithin (fun y => c y • f) s x = derivWithin c s x • f

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y • f) s x = derivWithin c s x • f

case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y • f) s x = derivWithin c s x • f
-- Mathlib/Algebra/Field/Rat.lean
@[simp]
lemma num_div_den (q : ℚ≥0) : (q.num : ℚ≥0) / q.den = q

Proof state:
case a
q : ℚ≥0
⊢ ↑↑(↑q).num.natAbs / ↑q.den = ↑q

Tactic:
exact (cast_def _).symm

Result:
no goals

Proof state:
q : ℚ≥0
⊢ ↑q.num / ↑q.den = q

Tactic:
ext1

Result:
case a
q : ℚ≥0
⊢ ↑(↑q.num / ↑q.den) = ↑q

Proof state:
case a
q : ℚ≥0
⊢ ↑(↑q.num / ↑q.den) = ↑q

Tactic:
rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_natCast]

Result:
case a
q : ℚ≥0
⊢ ↑↑(↑q).num.natAbs / ↑q.den = ↑q
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_eq_zero_iff {θ : ℂ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * π / 2

Proof state:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2

Tactic:
refine (iff_of_eq <| congr_arg _ ?_).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero)

Result:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ ↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)

Proof state:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ (↑π * I + ↑x * (2 * ↑π * I)) * 2 = 2 * I * ((2 * ↑x + 1) * ↑π)

Tactic:
ring

Result:
no goals

Proof state:
θ : ℂ
⊢ cexp (θ * I - -θ * I) = -1 ↔ cexp (2 * θ * I) = -1

Tactic:
ring_nf

Result:
no goals

Proof state:
θ : ℂ
⊢ (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1

Tactic:
rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul,
  add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]

Result:
θ : ℂ
⊢ cexp (θ * I - -θ * I) = -1 ↔ cexp (2 * θ * I) = -1

Proof state:
θ : ℂ
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 := by
  rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, zero_mul,
    add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub]
  ring_nf

Result:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Proof state:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ (∃ n, 2 * I * θ = ↑π * I + ↑n * (2 * ↑π * I)) ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
refine exists_congr fun x => ?_

Result:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ 2 * I * θ = ↑π * I + ↑x * (2 * ↑π * I) ↔ θ = (2 * ↑x + 1) * ↑π / 2

Proof state:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ ↑π * I + ↑x * (2 * ↑π * I) = 2 * I * ((2 * ↑x + 1) * ↑π / 2)

Tactic:
field_simp

Result:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
x : ℤ
⊢ (↑π * I + ↑x * (2 * ↑π * I)) * 2 = 2 * I * ((2 * ↑x + 1) * ↑π)

Proof state:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ cos θ = 0 ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2

Tactic:
rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm]

Result:
θ : ℂ
h : (cexp (θ * I) + cexp (-θ * I)) / 2 = 0 ↔ cexp (2 * θ * I) = -1
⊢ (∃ n, 2 * I * θ = ↑π * I + ↑n * (2 * ↑π * I)) ↔ ∃ k, θ = (2 * ↑k + 1) * ↑π / 2