harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_lt_intCast {m : ℚ} {n : ℤ} : (m : K) < n ↔ m < (n : ℚ)

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℚ
n : ℤ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
rw [← cast_lt (K := K), cast_intCast]

Result:
no goals
-- Mathlib/Topology/Algebra/ContinuousAffineMap.lean
theorem toAffineMap_injective {f g : P →ᴬ[R] Q} (h : (f : P →ᵃ[R] Q) = (g : P →ᵃ[R] Q)) :
    f = g

Proof state:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f g : P →ᴬ[R] Q
h : ↑f = ↑g
⊢ f = g

Tactic:
cases f

Result:
case mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
g : P →ᴬ[R] Q
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : ↑{ toAffineMap := toAffineMap✝, cont := cont✝ } = ↑g
⊢ { toAffineMap := toAffineMap✝, cont := cont✝ } = g

Proof state:
case mk.mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
toAffineMap✝¹ : P →ᵃ[R] Q
cont✝¹ : Continuous toAffineMap✝¹.toFun
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : ↑{ toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = ↑{ toAffineMap := toAffineMap✝, cont := cont✝ }
⊢ { toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = { toAffineMap := toAffineMap✝, cont := cont✝ }

Tactic:
congr

Result:
no goals

Proof state:
case mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
g : P →ᴬ[R] Q
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : ↑{ toAffineMap := toAffineMap✝, cont := cont✝ } = ↑g
⊢ { toAffineMap := toAffineMap✝, cont := cont✝ } = g

Tactic:
cases g

Result:
case mk.mk
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
toAffineMap✝¹ : P →ᵃ[R] Q
cont✝¹ : Continuous toAffineMap✝¹.toFun
toAffineMap✝ : P →ᵃ[R] Q
cont✝ : Continuous toAffineMap✝.toFun
h : ↑{ toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = ↑{ toAffineMap := toAffineMap✝, cont := cont✝ }
⊢ { toAffineMap := toAffineMap✝¹, cont := cont✝¹ } = { toAffineMap := toAffineMap✝, cont := cont✝ }
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem rootOrdered_iff {p : Path α} (hp : p.Ordered cmp) :
    p.RootOrdered cmp v ↔ (∀ a ∈ p.listL, cmpLT cmp a v) ∧ (∀ a ∈ p.listR, cmpLT cmp v a)

Proof state:
case left
α : Type u_1
cmp : α → α → Ordering
v : α
c✝ : RBColor
parent✝ : Path α
x : α
r✝ : RBNode α
ih :
  Ordered cmp parent✝ →
    (RootOrdered cmp parent✝ v ↔
      (∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp v a)
hp :
  Ordered cmp parent✝ ∧
    (∀ (x_1 : α), x_1 ∈ r✝ → cmpLT cmp x x_1) ∧
      RootOrdered cmp parent✝ x ∧ (∀ (x : α), x ∈ r✝ → RootOrdered cmp parent✝ x) ∧ RBNode.Ordered cmp r✝
⊢ cmpLT cmp v x →
    (∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a v) →
      (∀ (a : α), a ∈ parent✝.listR → cmpLT cmp v a) → ∀ (x : α), x ∈ r✝ → cmpLT cmp v x

Tactic:
exact fun vx _ _ _ ha => vx.trans (hp.2.1 _ ha)

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
v : α
p : Path α
hp : Ordered cmp p
⊢ RootOrdered cmp p v ↔ (∀ (a : α), a ∈ p.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ p.listR → cmpLT cmp v a

Tactic:
induction p with
  (simp [All_def] at hp; simp [*, and_assoc, and_left_comm, and_comm, or_imp, forall_and])
| left _ _ x _ ih => exact fun vx _ _ _ ha => vx.trans (hp.2.1 _ ha)
| right _ _ x _ ih => exact fun xv _ _ _ ha => (hp.2.1 _ ha).trans xv

Result:
no goals

Proof state:
case root
α : Type u_1
cmp : α → α → Ordering
v : α
hp : Ordered cmp root
⊢ RootOrdered cmp root v ↔ (∀ (a : α), a ∈ root.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ root.listR → cmpLT cmp v a

Tactic:
simp [All_def] at hp

Result:
case root
α : Type u_1
cmp : α → α → Ordering
v : α
hp : True
⊢ RootOrdered cmp root v ↔ (∀ (a : α), a ∈ root.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ root.listR → cmpLT cmp v a

Proof state:
case root
α : Type u_1
cmp : α → α → Ordering
v : α
hp : True
⊢ RootOrdered cmp root v ↔ (∀ (a : α), a ∈ root.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ root.listR → cmpLT cmp v a

Tactic:
simp [*, and_assoc, and_left_comm, and_comm, or_imp, forall_and]

Result:
no goals

Proof state:
case right
α : Type u_1
cmp : α → α → Ordering
v : α
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ →
    (RootOrdered cmp parent✝ v ↔
      (∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ parent✝.listR → cmpLT cmp v a)
hp :
  Ordered cmp parent✝ ∧
    (∀ (x_1 : α), x_1 ∈ l✝ → cmpLT cmp x_1 x) ∧
      RootOrdered cmp parent✝ x ∧ (∀ (x : α), x ∈ l✝ → RootOrdered cmp parent✝ x) ∧ RBNode.Ordered cmp l✝
⊢ cmpLT cmp x v →
    (∀ (a : α), a ∈ parent✝.listL → cmpLT cmp a v) →
      (∀ (a : α), a ∈ parent✝.listR → cmpLT cmp v a) → ∀ (x : α), x ∈ l✝ → cmpLT cmp x v

Tactic:
exact fun xv _ _ _ ha => (hp.2.1 _ ha).trans xv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem le_refl [LT α] [i₀ : Std.Irrefl (· < · : α → α → Prop)] (l : List α) : l ≤ l

Proof state:
α : Type u_1
inst✝ : LT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
l : List α
⊢ l ≤ l

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  intro
  | .rel h => exact i₀.irrefl _ h
  | .cons h₃ => exact ih h₃

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
a : α
l : List α
ih : l ≤ l
x✝ : a :: l < a :: l
h₃ : Lex (fun x1 x2 => x1 < x2) l l
⊢ False

Tactic:
exact ih h₃

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : LT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
⊢ [] ≤ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : LT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
a : α
l : List α
ih : l ≤ l
⊢ a :: l ≤ a :: l

Tactic:
intro
| .rel h => exact i₀.irrefl _ h
| .cons h₃ => exact ih h₃

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
i₀ : Std.Irrefl fun x1 x2 => x1 < x2
a : α
l : List α
ih : l ≤ l
x✝ : a :: l < a :: l
h : a < a
⊢ False

Tactic:
exact i₀.irrefl _ h

Result:
no goals
-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem Associates.isAtom_iff {p : Associates M} (h₁ : p ≠ 0) : IsAtom p ↔ Irreducible p :=
  ⟨fun hp =>
    ⟨by simpa only [Associates.isUnit_iff_eq_one] using hp.1, fun a b h =>
      (hp.le_iff.mp ⟨_, h⟩).casesOn (fun ha => Or.inl (a.isUnit_iff_eq_one.mpr ha)) fun ha =>
        Or.inr
          (show IsUnit b by
            rw [ha] at h
            apply isUnit_of_associated_mul (show Associated (p * b) p by conv_rhs => rw [h]) h₁)⟩,
    fun hp =>
    ⟨by simpa only [Associates.isUnit_iff_eq_one, Associates.bot_eq_one] using hp.1,
      fun b ⟨⟨a, hab⟩, hb⟩ =>
      (hp.isUnit_or_isUnit hab).casesOn
        (fun hb => show b = ⊥ by rwa [Associates.isUnit_iff_eq_one, ← Associates.bot_eq_one] at hb)
        fun ha =>
        absurd
          (show p ∣ b from
            ⟨(ha.unit⁻¹ : Units _), by rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]⟩)
          hb⟩⟩

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ Associated (p * b) p

Tactic:
conv_rhs => rw [h]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
⊢ p ≠ ⊥

Tactic:
simpa only [Associates.isUnit_iff_eq_one, Associates.bot_eq_one] using hp.1

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ IsUnit b

Tactic:
apply isUnit_of_associated_mul (show Associated (p * b) p by conv_rhs => rw [h]) h₁

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
⊢ ¬IsUnit p

Tactic:
simpa only [Associates.isUnit_iff_eq_one] using hp.1

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = a * b
ha : a = p
⊢ IsUnit b

Tactic:
rw [ha] at h

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = p * b
ha : a = p
⊢ IsUnit b

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb✝ : ¬p ∣ b
hb : IsUnit b
⊢ b = ⊥

Tactic:
rwa [Associates.isUnit_iff_eq_one, ← Associates.bot_eq_one] at hb

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : Associates M
h₁ : p ≠ 0
hp : Irreducible p
b : Associates M
x✝ : b < p
a : Associates M
hab : p = b * a
hb : ¬p ∣ b
ha : IsUnit a
⊢ b = p * ↑ha.unit⁻¹

Tactic:
rw [hab, mul_assoc, IsUnit.mul_val_inv ha, mul_one]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem coeff_ofSubring (p : T[X]) (n : ℕ) : coeff (ofSubring T p) n = (coeff p n : T)

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ (ofSubring T p).coeff n = ↑(p.coeff n)

Tactic:
simp only [ofSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
  ite_eq_right_iff, Ne, ite_not, Classical.not_not, ite_eq_left_iff]

Result:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ p.coeff n = 0 → 0 = ↑(p.coeff n)

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
⊢ p.coeff n = 0 → 0 = ↑(p.coeff n)

Tactic:
intro h

Result:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = ↑(p.coeff n)

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
n : ℕ
h : p.coeff n = 0
⊢ 0 = ↑(p.coeff n)

Tactic:
rw [h, ZeroMemClass.coe_zero]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem IsTorsionFree.quotient_torsion : IsTorsionFree <| G ⧸ torsion G := fun g hne hfin =>
  hne <| by
    induction' g using QuotientGroup.induction_on with g
    obtain ⟨m, mpos, hm⟩ := hfin.exists_pow_eq_one
    obtain ⟨n, npos, hn⟩ := ((QuotientGroup.eq_one_iff _).mp hm).exists_pow_eq_one
    exact
      (QuotientGroup.eq_one_iff g).mpr
        (isOfFinOrder_iff_pow_eq_one.mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)

Proof state:
case H.intro.intro.intro.intro
G : Type u_1
inst✝ : CommGroup G
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x => x ^ m) g ^ n = 1
⊢ ↑g = 1

Tactic:
exact
  (QuotientGroup.eq_one_iff g).mpr
    (isOfFinOrder_iff_pow_eq_one.mpr ⟨m * n, mul_pos mpos npos, (pow_mul g m n).symm ▸ hn⟩)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : CommGroup G
g : G ⧸ torsion G
hne : g ≠ 1
hfin : IsOfFinOrder g
⊢ g = 1

Tactic:
induction' g using QuotientGroup.induction_on with g

Result:
case H
G : Type u_1
inst✝ : CommGroup G
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
⊢ ↑g = 1

Proof state:
case H
G : Type u_1
inst✝ : CommGroup G
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
⊢ ↑g = 1

Tactic:
obtain ⟨m, mpos, hm⟩ := hfin.exists_pow_eq_one

Result:
case H.intro.intro
G : Type u_1
inst✝ : CommGroup G
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
⊢ ↑g = 1

Proof state:
case H.intro.intro
G : Type u_1
inst✝ : CommGroup G
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
⊢ ↑g = 1

Tactic:
obtain ⟨n, npos, hn⟩ := ((QuotientGroup.eq_one_iff _).mp hm).exists_pow_eq_one

Result:
case H.intro.intro.intro.intro
G : Type u_1
inst✝ : CommGroup G
g : G
hne : ↑g ≠ 1
hfin : IsOfFinOrder ↑g
m : ℕ
mpos : 0 < m
hm : ↑g ^ m = 1
n : ℕ
npos : 0 < n
hn : (fun x => x ^ m) g ^ n = 1
⊢ ↑g = 1
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem exists_list_transvec_mul_mul_list_transvec_eq_diagonal (M : Matrix n n 𝕜) :
    ∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e

Result:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
⊢ Fintype.card n = Fintype.card (Fin (Fintype.card n))

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
have e : n ≃ Fin (Fintype.card n) := Fintype.equivOfCardEq (by simp)

Result:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
e : n ≃ Fin (Fintype.card n)
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuation_exists_uniformizer : ∃ π : K,
    v.valuation K π = Multiplicative.ofAdd (-1 : ℤ)

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : v.intValuationDef r = ↑(ofAdd (-1))
⊢ v.intValuation r = ↑(ofAdd (-1))

Tactic:
exact hr

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ ∃ π, (valuation K v) π = ↑(ofAdd (-1))

Tactic:
obtain ⟨r, hr⟩ := v.intValuation_exists_uniformizer

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : v.intValuationDef r = ↑(ofAdd (-1))
⊢ ∃ π, (valuation K v) π = ↑(ofAdd (-1))

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : v.intValuationDef r = ↑(ofAdd (-1))
⊢ ∃ π, (valuation K v) π = ↑(ofAdd (-1))

Tactic:
use algebraMap R K r

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : v.intValuationDef r = ↑(ofAdd (-1))
⊢ (valuation K v) ((algebraMap R K) r) = ↑(ofAdd (-1))

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : v.intValuationDef r = ↑(ofAdd (-1))
⊢ (valuation K v) ((algebraMap R K) r) = ↑(ofAdd (-1))

Tactic:
rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
hr : v.intValuationDef r = ↑(ofAdd (-1))
⊢ v.intValuation r = ↑(ofAdd (-1))
-- Mathlib/Control/Traversable/Instances.lean
theorem traverse_eq_map_id {α β} (f : α → β) (x : σ ⊕ α) :
    Sum.traverse ((pure : _ → Id _) ∘ f) x = (pure : _ → Id _) (f <$> x)

Proof state:
σ α β : Type u
f : α → β
x : σ ⊕ α
⊢ Sum.traverse (pure ∘ f) x = pure (f <$> x)

Tactic:
induction x <;> simp! [*, functor_norm] <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.le_multiplicity_of_le_emultiplicity (hfin : FiniteMultiplicity a b)
    {n : ℕ} (h : n ≤ emultiplicity a b) : n ≤ multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ emultiplicity a b
⊢ n ≤ multiplicity a b

Tactic:
rw [emultiplicity_eq_multiplicity hfin] at h

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ ↑(multiplicity a b)
⊢ n ≤ multiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : ↑n ≤ ↑(multiplicity a b)
⊢ n ≤ multiplicity a b

Tactic:
assumption_mod_cast

Result:
no goals
-- Mathlib/Data/Nat/Choose/Bounds.lean
theorem choose_le_pow_div (r n : ℕ) : (n.choose r : α) ≤ (n ^ r : α) / r !

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

Tactic:
norm_cast

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ r ! * n.choose r ≤ n ^ r

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(n.choose r) ≤ ↑n ^ r / ↑r !

Tactic:
rw [le_div_iff₀']

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑r ! * ↑(n.choose r) ≤ ↑n ^ r

α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ r ! * n.choose r ≤ n ^ r

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ n.descFactorial r ≤ n ^ r

Tactic:
exact n.descFactorial_le_pow r

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !

Tactic:
exact mod_cast r.factorial_pos

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_lt_tsub_iff_right (hc : AddLECancellable c) (h : c ≤ a) :
    a - c < b - c ↔ a < b

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b

Tactic:
rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma commShiftIso_add' {a b c : A} (h : a + b = c) :
    F.commShiftIso c = CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b c : A
h : a + b = c
⊢ F.commShiftIso c = CommShift.isoAdd' h (F.commShiftIso a) (F.commShiftIso b)

Tactic:
subst h

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
⊢ F.commShiftIso (a + b) = CommShift.isoAdd' ⋯ (F.commShiftIso a) (F.commShiftIso b)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_7, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
⊢ F.commShiftIso (a + b) = CommShift.isoAdd' ⋯ (F.commShiftIso a) (F.commShiftIso b)

Tactic:
simp only [commShiftIso_add, CommShift.isoAdd]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
@[to_additive (attr := simp) zero_mem_addCentralizer]
lemma one_mem_centralizer : (1 : M) ∈ centralizer S

Proof state:
M : Type u_1
S : Set M
inst✝ : MulOneClass M
⊢ 1 ∈ S.centralizer

Tactic:
simp [mem_centralizer_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : Array β) (init : α₁)
    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init)

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
toList✝ : List β
⊢ foldl g₂ (f init) { toList := toList✝ } = f (foldl g₁ init { toList := toList✝ })

Tactic:
simp

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
toList✝ : List β
⊢ List.foldl g₂ (f init) toList✝ = f (List.foldl g₁ init toList✝)

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
toList✝ : List β
⊢ List.foldl g₂ (f init) toList✝ = f (List.foldl g₁ init toList✝)

Tactic:
rw [List.foldl_hom _ _ _ _ _ H]

Result:
no goals

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
l : Array β
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
⊢ foldl g₂ (f init) l = f (foldl g₁ init l)

Tactic:
cases l

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
toList✝ : List β
⊢ foldl g₂ (f init) { toList := toList✝ } = f (foldl g₁ init { toList := toList✝ })
-- Mathlib/Data/Set/Card.lean
theorem encard_univ_coe (s : Set α) : encard (univ : Set s) = encard s

Proof state:
α : Type u_1
s : Set α
⊢ univ.encard = s.encard

Tactic:
rw [encard, encard, ENat.card_congr (Equiv.Set.univ ↑s)]

Result:
no goals