harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem ramificationIdx_algebra_tower [IsDedekindDomain S] [IsDedekindDomain T]
    {p : Ideal R} {P : Ideal S} {Q : Ideal T} [hpm : P.IsPrime] [hqm : Q.IsPrime]
    (hg0 : map (algebraMap S T) P ≠ ⊥)
    (hfg : map (algebraMap R T) p ≠ ⊥) (hg : map (algebraMap S T) P ≤ Q) :
    ramificationIdx (algebraMap R T) p Q =
    ramificationIdx (algebraMap R S) p P * ramificationIdx (algebraMap S T) P Q

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map (algebraMap R T) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
⊢ ramificationIdx (algebraMap R T) p Q = ramificationIdx (algebraMap R S) p P * ramificationIdx (algebraMap S T) P Q

Tactic:
rw [IsScalarTower.algebraMap_eq R S T] at hfg ⊢

Result:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map ((algebraMap S T).comp (algebraMap R S)) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
⊢ ramificationIdx ((algebraMap S T).comp (algebraMap R S)) p Q =
    ramificationIdx (algebraMap R S) p P * ramificationIdx (algebraMap S T) P Q

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsDedekindDomain S
inst✝ : IsDedekindDomain T
p : Ideal R
P : Ideal S
Q : Ideal T
hpm : P.IsPrime
hqm : Q.IsPrime
hg0 : map (algebraMap S T) P ≠ ⊥
hfg : map ((algebraMap S T).comp (algebraMap R S)) p ≠ ⊥
hg : map (algebraMap S T) P ≤ Q
⊢ ramificationIdx ((algebraMap S T).comp (algebraMap R S)) p Q =
    ramificationIdx (algebraMap R S) p P * ramificationIdx (algebraMap S T) P Q

Tactic:
exact ramificationIdx_tower hg0 hfg hg

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem eq_of_map_eq_withDensity [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] (f : E → ℝ≥0∞)
    (hmf : AEMeasurable f μ) : map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᵐ[μ] f

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ map X ℙ = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f

Tactic:
rw [map_eq_withDensity_pdf X ℙ μ]

Result:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ℙ Set.univ ≠ ⊤

Tactic:
exact measure_ne_top _ _

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ μ.withDensity (pdf X ℙ μ) = μ.withDensity f ↔ pdf X ℙ μ =ᶠ[ae μ] f

Tactic:
apply withDensity_eq_iff (measurable_pdf X ℙ μ).aemeasurable hmf

Result:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ⊤

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ ≠ ⊤

Tactic:
rw [lintegral_eq_measure_univ]

Result:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → ℝ≥0∞
hmf : AEMeasurable f μ
⊢ ℙ Set.univ ≠ ⊤
-- Mathlib/LinearAlgebra/Determinant.lean
theorem AlternatingMap.map_basis_eq_zero_iff {ι : Type*} [Finite ι] (e : Basis ι R M)
    (f : M [⋀^ι]→ₗ[R] R) : f e = 0 ↔ f = 0 :=
  ⟨fun h => by
    cases nonempty_fintype ι
    letI := Classical.decEq ι
    simpa [h] using f.eq_smul_basis_det e,
   fun h => h.symm ▸ AlternatingMap.zero_apply _⟩

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ f = 0

Tactic:
simpa [h] using f.eq_smul_basis_det e

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
⊢ f = 0

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
val✝ : Fintype ι
⊢ f = 0

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
val✝ : Fintype ι
⊢ f = 0

Tactic:
letI := Classical.decEq ι

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_5
inst✝ : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : f ⇑e = 0
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ f = 0
-- Mathlib/Data/Nat/Init.lean
@[simp] protected lemma lt_mul_iff_one_lt_left (hb : 0 < b) : b < a * b ↔ 1 < a

Proof state:
a b : ℕ
hb : 0 < b
⊢ b < a * b ↔ 1 < a

Tactic:
simpa using Nat.mul_lt_mul_right (b := 1) hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_not_self : ∀ (x : Bool), (x   != !x) = true

Proof state:
⊢ ∀ (x : Bool), (x != !x) = true

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_append {as bs : Array α} {i : Nat} :
    (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]?

Proof state:
α : Type u_1
as bs : Array α
i : Nat
h : ¬i < as.size
⊢ as.size ≤ i

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
as bs : Array α
i : Nat
h : i < as.size
⊢ (as ++ bs)[i]? = as[i]?

Tactic:
exact getElem?_append_left h

Result:
no goals

Proof state:
α : Type u_1
as bs : Array α
i : Nat
⊢ (as ++ bs)[i]? = if i < as.size then as[i]? else bs[i - as.size]?

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
as bs : Array α
i : Nat
h : i < as.size
⊢ (as ++ bs)[i]? = as[i]?

case isFalse
α : Type u_1
as bs : Array α
i : Nat
h : ¬i < as.size
⊢ (as ++ bs)[i]? = bs[i - as.size]?

Proof state:
case isFalse
α : Type u_1
as bs : Array α
i : Nat
h : ¬i < as.size
⊢ (as ++ bs)[i]? = bs[i - as.size]?

Tactic:
exact getElem?_append_right (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.get?_eq_getValue? [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} :
    Const.get? m a = getValue? a (toListModel m.1.buckets)

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
hm : Raw.WFImp m.val
a : α
⊢ get? m a = getValue? a (toListModel m.val.buckets)

Tactic:
rw [Const.get?_eq_get?ₘ, Const.get?ₘ_eq_getValue? hm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_eq_getElem? (l : BitVec w) (i : Nat) (h : i < w) :
    l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h])

Proof state:
w : Nat
l : BitVec w
i : Nat
h : i < w
⊢ l[i]?.isSome = true

Tactic:
simp [getElem?_eq_getElem, h]

Result:
no goals

Proof state:
w : Nat
l : BitVec w
i : Nat
h : i < w
⊢ l[i] = l[i]?.get ⋯

Tactic:
simp [getElem_eq_iff]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem nnnorm_le_iff {r : ℝ≥0} {A : Matrix m n α} : ‖A‖₊ ≤ r ↔ ∀ i j, ‖A i j‖₊ ≤ r

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ≥0
A : Matrix m n α
⊢ ‖A‖₊ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ ≤ r

Tactic:
simp_rw [nnnorm_def, pi_nnnorm_le_iff]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem inter_nil' (l : List α) : l ∩ [] = []

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [] ∩ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs ∩ [] = []
⊢ (x :: xs) ∩ [] = []

Tactic:
by_cases x ∈ xs <;> simp [ih]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l ∩ [] = []

Tactic:
induction l with
| nil => rfl
| cons x xs ih => by_cases x ∈ xs <;> simp [ih]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
@[simp]
lemma image_fst_graphOn (f : α → β) (s : Set α) : Prod.fst '' graphOn f s = s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Prod.fst '' graphOn f s = s

Tactic:
simp [graphOn, image_image]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem locallyIntegrableOn_iff_locallyIntegrable_restrict [OpensMeasurableSpace X]
    (hs : IsClosed s) : LocallyIntegrableOn f s μ ↔ LocallyIntegrable f (μ.restrict s)

Proof state:
case neg
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f sᶜ (μ.restrict s)

Tactic:
rw [IntegrableOn, restrict_restrict, inter_comm, inter_compl_self, ← IntegrableOn]

Result:
case neg
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f ∅ μ

case neg
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ MeasurableSet sᶜ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_ite_nil_right {x : α} [Decidable p] {l : List α} :
    (x ∈ if p then l else []) ↔ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : List α
⊢ (x ∈ if p then l else []) ↔ p ∧ x ∈ l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem pi_apply_single [Fintype ι] [DecidableEq ι]
    (Q : ∀ i, QuadraticMap R (Mᵢ i) P) (i : ι) (m : Mᵢ i) :
    pi Q (Pi.single i m) = Q i m

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
⊢ (pi Q) (Pi.single i m) = (Q i) m

Tactic:
rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]

Result:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ (Q j) (Pi.single i m j) = 0

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (Mᵢ i)
inst✝⁴ : AddCommMonoid P
inst✝³ : (i : ι) → Module R (Mᵢ i)
inst✝² : Module R P
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
i : ι
m : Mᵢ i
j : ι
hj : j ≠ i
⊢ (Q j) (Pi.single i m j) = 0

Tactic:
rw [Pi.single_eq_of_ne hj, map_zero]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the upper shadow of `𝒜` iff there is a `s ∈ 𝒜` from which we can remove one element
to get `t`. -/
lemma mem_upShadow_iff : t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t

Tactic:
simp_rw [upShadow, mem_sup, mem_image, mem_compl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem holderOnWith_singleton (C r : ℝ≥0) (f : X → Y) (x : X) : HolderOnWith C r f {x}

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
x : X
⊢ HolderOnWith C r f {x}

Tactic:
rintro a (rfl : a = x) b (rfl : b = a)

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
b : X
⊢ edist (f b) (f b) ≤ ↑C * edist b b ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
b : X
⊢ edist (f b) (f b) ≤ ↑C * edist b b ^ ↑r

Tactic:
rw [edist_self]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
b : X
⊢ 0 ≤ ↑C * edist b b ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
C r : ℝ≥0
f : X → Y
b : X
⊢ 0 ≤ ↑C * edist b b ^ ↑r

Tactic:
exact zero_le _

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P3_of_ih (hy : Numeric y) (ihyx : IH1 y x) (i k l) :
    P3 (x.moveLeft i) x (y.moveLeft k) (-(-y).moveLeft l) :=
  P3_comm.2 <| ((ihyx (IsOption.moveLeft k) (isOption_neg.1 <| .moveLeft l) <| Or.inl rfl).2
    (by rw [moveLeft_neg, neg_neg]; apply hy.left_lt_right)).1 i

Proof state:
x y : PGame
hy : y.Numeric
ihyx : IH1 y x
i : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ y.moveLeft k < -(-y).moveLeft l

Tactic:
rw [moveLeft_neg, neg_neg]

Result:
x y : PGame
hy : y.Numeric
ihyx : IH1 y x
i : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ y.moveLeft k < y.moveRight (toLeftMovesNeg.symm l)

Proof state:
x y : PGame
hy : y.Numeric
ihyx : IH1 y x
i : x.LeftMoves
k : y.LeftMoves
l : (-y).LeftMoves
⊢ y.moveLeft k < y.moveRight (toLeftMovesNeg.symm l)

Tactic:
apply hy.left_lt_right

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finite_mulSupport {I : Ideal R} (hI : I ≠ 0) :
    (mulSupport fun v : HeightOneSpectrum R => v.maxPowDividing I).Finite :=
  haveI h_subset : {v : HeightOneSpectrum R | v.maxPowDividing I ≠ 1} ⊆
      {v : HeightOneSpectrum R |
        ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ) ≠ 0}

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ v.maxPowDividing I = 1

Tactic:
rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.natCast_eq_zero.mp h_zero,
  pow_zero _]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | v.maxPowDividing I ≠ 1} ⊆ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}

Tactic:
intro v hv h_zero

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ False

Tactic:
have hv' : v.maxPowDividing I = 1 := by
  rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.natCast_eq_zero.mp h_zero,
    pow_zero _]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
hv' : v.maxPowDividing I = 1
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
hv' : v.maxPowDividing I = 1
⊢ False

Tactic:
exact hv hv'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_emod (a b : Int) : (a % b) % b = a % b

Proof state:
a b : Int
⊢ a % b % b = a % b

Tactic:
conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem nnnorm_inr (m : M) : ‖(inr m : tsze R M)‖₊ = ‖m‖₊

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
m : M
⊢ ‖inr m‖₊ = ‖m‖₊

Tactic:
simp [nnnorm_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Lemmas.lean
theorem eventually_norm_sub_lt (x₀ : E) {ε : ℝ} (ε_pos : 0 < ε) :
    ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖ < ε :=
  (continuousAt_id.sub continuousAt_const).norm (gt_mem_nhds <| by simpa)

Proof state:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
x₀ : E
ε : ℝ
ε_pos : 0 < ε
⊢ (fun x => ‖id x - x₀‖) x₀ < ε

Tactic:
simpa

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Indization/Products.lean
theorem isIndObject_pi (h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g))
    (f : α → Cᵒᵖ ⥤ Type v) (hf : ∀ a, IsIndObject (f a)) : IsIndObject (∏ᶜ f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a => ⋯.presentation.F ⋙ yoneda
⊢ ∏ᶜ f ≅ colimit (pointwiseProduct F)

Tactic:
refine Pi.mapIso (fun s => ?_) ≪≫ (asIso (colimitPointwiseProductToProductColimit F)).symm

Result:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a => ⋯.presentation.F ⋙ yoneda
s : α
⊢ f s ≅ colimit (F s)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a => ⋯.presentation.F ⋙ yoneda
⊢ IsIndObject (∏ᶜ f)

Tactic:
suffices (∏ᶜ f ≅ colimit (pointwiseProduct F)) from
  (isIndObject_colimit _ _ (fun i => h _)).map this.inv

Result:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a => ⋯.presentation.F ⋙ yoneda
⊢ ∏ᶜ f ≅ colimit (pointwiseProduct F)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a => ⋯.presentation.F ⋙ yoneda
s : α
⊢ f s ≅ colimit (F s)

Tactic:
exact IsColimit.coconePointUniqueUpToIso (hf s).presentation.isColimit (colimit.isColimit _)

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
⊢ IsIndObject (∏ᶜ f)

Tactic:
let F := fun a => (hf a).presentation.F ⋙ yoneda

Result:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a => ⋯.presentation.F ⋙ yoneda
⊢ IsIndObject (∏ᶜ f)
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem subgroupOf_map_subtype (H K : Subgroup G) : (H.subgroupOf K).map K.subtype = H ⊓ K :=
  SetLike.ext' <| by refine Subtype.image_preimage_coe _ _ |>.trans ?_; apply Set.inter_comm

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑(map K.subtype (H.subgroupOf K)) = ↑(H ⊓ K)

Tactic:
refine Subtype.image_preimage_coe _ _ |>.trans ?_

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑K ∩ H.toSubsemigroup.1 = ↑(H ⊓ K)

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ ↑K ∩ H.toSubsemigroup.1 = ↑(H ⊓ K)

Tactic:
apply Set.inter_comm

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem findEntry?_congr [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k₁ k₂ = .eq) :
    t.findEntry? k₁ = t.findEntry? k₂

Proof state:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k₁ k₂ : α
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k₁ k₂ = Ordering.eq
⊢ t.findEntry? k₁ = t.findEntry? k₂

Tactic:
simp [findEntry?, TransCmp.cmp_congr_left' h]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
@[simp] lemma ssubset_singleton_iff : s ⊂ {a} ↔ s = 0

Proof state:
case refine_1
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
⊢ {b} ⊆ s

Tactic:
rwa [singleton_subset]

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
a : α
⊢ s ⊂ {a} ↔ s = 0

Tactic:
refine ⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩

Result:
case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s

case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Proof state:
case refine_1
α : Type u_1
s : Multiset α
a : α
hs : s ⊂ {a}
b : α
hb : b ∈ s
⊢ {a} ⊆ s

Tactic:
obtain rfl := mem_singleton.1 (hs.1 hb)

Result:
case refine_1
α : Type u_1
s : Multiset α
b : α
hb : b ∈ s
hs : s ⊂ {b}
⊢ {b} ⊆ s

Proof state:
case refine_2
α : Type u_1
a : α
⊢ 0 ⊂ {a}

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → s ⊂ {a}

Tactic:
rintro rfl

Result:
case refine_2
α : Type u_1
a : α
⊢ 0 ⊂ {a}
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
⊢ ⅟A = A⁻¹

Tactic:
letI := detInvertibleOfInvertible A

Result:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ ⅟A = A⁻¹

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
this : Invertible A.det := A.detInvertibleOfInvertible
⊢ ⅟A = A⁻¹

Tactic:
rw [inv_def, Ring.inverse_invertible, invOf_eq]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rootD_lt {self : UnionFind} {x : Nat} : self.rootD x < self.size ↔ x < self.size

Proof state:
self : UnionFind
x : Nat
⊢ (if h : x < self.arr.size then ↑(self.root ⟨x, ⋯⟩) else x) < self.arr.size ↔ x < self.arr.size

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
self : UnionFind
x : Nat
⊢ self.rootD x < self.size ↔ x < self.size

Tactic:
simp only [rootD, Array.length_toList]

Result:
self : UnionFind
x : Nat
⊢ (if h : x < self.arr.size then ↑(self.root ⟨x, ⋯⟩) else x) < self.arr.size ↔ x < self.arr.size