harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_muld {a : ℤ√d} (ha : Nonneg a) : Nonneg (sqrtd * a) :=
  match a, nonneg_cases ha, ha with
  | _, ⟨_, _, Or.inl rfl⟩, _ => trivial
  | _, ⟨x, y, Or.inr <| Or.inl rfl⟩, ha => by
    simp only [muld_val, mul_neg]
    apply nonnegg_neg_pos.2
    simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)
  | _, ⟨x, y, Or.inr <| Or.inr rfl⟩, ha => by
    simp only [muld_val]
    apply nonnegg_pos_neg.2
    simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)

Proof state:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ { re := ↑d * ↑y, im := -↑x }.Nonneg

Tactic:
apply nonnegg_pos_neg.2

Result:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ SqLe x d (d * y) 1

Proof state:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ (sqrtd * { re := -↑x, im := ↑y }).Nonneg

Tactic:
simp only [muld_val]

Result:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ { re := ↑d * ↑y, im := -↑x }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
⊢ SqLe x d (d * y) 1

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_neg_pos.1 ha)

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ (sqrtd * { re := ↑x, im := -↑y }).Nonneg

Tactic:
simp only [muld_val, mul_neg]

Result:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ { re := -(↑d * ↑y), im := ↑x }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ { re := -(↑d * ↑y), im := ↑x }.Nonneg

Tactic:
apply nonnegg_neg_pos.2

Result:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ SqLe (d * y) 1 x d

Proof state:
d : ℕ
a : ℤ√↑d
ha✝ : a.Nonneg
x y : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
⊢ SqLe (d * y) 1 x d

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_left d (nonnegg_pos_neg.1 ha)

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
theorem not_lt_iff {z w : ℂ} : ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

Proof state:
z w : ℂ
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

Tactic:
rw [lt_def, not_and_or, not_lt]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem ContinuousLinearMap.toLinear_compLeftContinuousCompact (g : β →L[𝕜] γ) :
    (g.compLeftContinuousCompact X : C(X, β) →ₗ[𝕜] C(X, γ)) = g.compLeftContinuous 𝕜 X

Proof state:
case h.h
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : C(X, β)
a✝ : X
⊢ (↑(ContinuousLinearMap.compLeftContinuousCompact X g) f) a✝ = ((ContinuousLinearMap.compLeftContinuous 𝕜 X g) f) a✝

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
⊢ ↑(ContinuousLinearMap.compLeftContinuousCompact X g) = ContinuousLinearMap.compLeftContinuous 𝕜 X g

Tactic:
ext f

Result:
case h.h
X : Type u_1
𝕜 : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup β
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
f : C(X, β)
a✝ : X
⊢ (↑(ContinuousLinearMap.compLeftContinuousCompact X g) f) a✝ = ((ContinuousLinearMap.compLeftContinuous 𝕜 X g) f) a✝
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma exists_isNilRegular [Infinite R] : ∃ x : L, IsNilRegular φ x

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : IsDomain R
inst✝ : Infinite R
⊢ ↑(finrank R M) ≤ Cardinal.mk R

Tactic:
exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : IsDomain R
inst✝ : Infinite R
⊢ ∃ x, φ.IsNilRegular x

Tactic:
apply exists_isNilRegular_of_finrank_le_card

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : IsDomain R
inst✝ : Infinite R
⊢ ↑(finrank R M) ≤ Cardinal.mk R
-- Mathlib/Data/Set/Finite/Lemmas.lean
theorem exists_lower_bound_image [Nonempty α] [LinearOrder β] (s : Set α) (f : α → β)
    (h : s.Finite) : ∃ a : α, ∀ b ∈ s, f a ≤ f b

Proof state:
case inl
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : ∅.Finite
⊢ ∃ a, ∀ b ∈ ∅, f a ≤ f b

Tactic:
exact ‹Nonempty α›.elim fun a => ⟨a, fun _ => False.elim⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hs

Result:
case inl
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
f : α → β
h : ∅.Finite
⊢ ∃ a, ∀ b ∈ ∅, f a ≤ f b

case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Proof state:
case inr.intro.intro
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ b ∈ s, f x₀ ≤ f b
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
exact ⟨x₀, fun x hx => hx₀ x hx⟩

Result:
no goals

Proof state:
case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
rcases Set.exists_min_image s f h hs with ⟨x₀, _, hx₀⟩

Result:
case inr.intro.intro
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ b ∈ s, f x₀ ≤ f b
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_le_iff_le_one_right [MulOneClass α] [MulLeftMono α]
    {a b : α} (ha : MulLECancellable a) :
    a * b ≤ a ↔ b ≤ 1 :=
  Iff.trans (by rw [mul_one]) ha.mul_le_mul_iff_left

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ a * b ≤ a ↔ a * b ≤ a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_map {A : Type*} [CommMonoid A] {U : Submonoid A} {R} [CommMonoid R]
    (j : LocalizationMap U R) {l : P →* A} (hl : ∀ w : T, l w ∈ U) (x) :
    k.map hl j (f.map hy k x) = f.map (fun x ↦ show l.comp g x ∈ U from hl ⟨g x, hy x⟩) j x

Proof state:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
x : N
⊢ (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x

Tactic:
rw [← f.map_comp_map (k := k) hy j hl]

Result:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
x : N
⊢ (k.map hl j) ((f.map hy k) x) = ((k.map hl j).comp (f.map hy k)) x

Proof state:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
x : N
⊢ (k.map hl j) ((f.map hy k) x) = ((k.map hl j).comp (f.map hy k)) x

Tactic:
simp only [MonoidHom.coe_comp, comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem contains (c) : ∀ {s}, Valid s → (s.contains c ↔ c ∈ s.toString.1)
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [h.contains, h.toString]

Proof state:
c : Char
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ x✝.contains c = true ↔ c ∈ x✝.toString.data

Tactic:
simp [h.contains, h.toString]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_neBot_iff : (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot

Tactic:
simp [neBot_iff, not_or]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
    (L.take j)[i] =
    L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _))

Proof state:
α : Type u_1
L : List α
j i : Nat
h✝ : i < (take j L).length
h : i < j ∧ i < L.length
⊢ (take j L)[i] = L[i]

Tactic:
rw [getElem_take' L _ h.1]

Result:
no goals

Proof state:
α : Type u_1
L : List α
j i : Nat
h : i < (take j L).length
⊢ (take j L)[i] = L[i]

Tactic:
rw [length_take, Nat.lt_min] at h

Result:
α : Type u_1
L : List α
j i : Nat
h✝ : i < (take j L).length
h : i < j ∧ i < L.length
⊢ (take j L)[i] = L[i]
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_mul (hp : p.Monic) (hq : q.Monic) :
    (p * q).natDegree = p.natDegree + q.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
apply natDegree_mul'

Result:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Proof state:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simp [hp.leadingCoeff, hq.leadingCoeff]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).natDegree = p.natDegree + q.natDegree
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem?_zero_filter (p : α → Bool) (l : Array α) :
    (l.filter p)[0]? = l.find? p

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ })[0]? = find? p { toList := toList✝ }

Tactic:
simp [← List.head?_eq_getElem?]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l)[0]? = find? p l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ (filter p { toList := toList✝ })[0]? = find? p { toList := toList✝ }
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem cos_angle_sub_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

Tactic:
rw [sub_eq_add_neg, cos_angle_add_mul_norm_of_inner_eq_zero h]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
/-- The left derivative of `klFun` is `log x`. This also holds at `x = 0` although `klFun` is not
differentiable there since the default value of `derivWithin` in that case is 0. -/
@[simp]
lemma leftDeriv_klFun : derivWithin klFun (Iio x) x = log x

Proof state:
x : ℝ
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
by_cases h0 : x = 0

Result:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio x) x = log x

case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Proof state:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
simp only [h0, log_zero]

Result:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio 0) 0 = 0

Proof state:
case pos
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio 0) 0 = 0

Tactic:
exact derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Iio_zero

Result:
no goals

Proof state:
case neg
x : ℝ
h0 : ¬x = 0
⊢ derivWithin klFun (Iio x) x = log x

Tactic:
exact (hasDerivAt_klFun h0).hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_succ (a) : lift.{v, u} (succ a) = succ (lift.{v, u} a) :=
  le_antisymm
    (le_of_not_gt fun h => by
      rcases lt_lift_iff.1 h with ⟨b, h, e⟩
      rw [lt_succ_iff, ← lift_le, e] at h
      exact h.not_lt (lt_succ _))
    (succ_le_of_lt <| lift_lt.2 <| lt_succ a)

Proof state:
a : Cardinal.{u}
h : lift.{v, u} (succ a) > succ (lift.{v, u} a)
⊢ False

Tactic:
rcases lt_lift_iff.1 h with ⟨b, h, e⟩

Result:
case intro.intro
a : Cardinal.{u}
h✝ : lift.{v, u} (succ a) > succ (lift.{v, u} a)
b : Cardinal.{u}
h : b < succ a
e : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Proof state:
case intro.intro
a : Cardinal.{u}
h✝ : lift.{v, u} (succ a) > succ (lift.{v, u} a)
b : Cardinal.{u}
h : succ (lift.{v, u} a) ≤ lift.{v, u} a
e : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
exact h.not_lt (lt_succ _)

Result:
no goals

Proof state:
case intro.intro
a : Cardinal.{u}
h✝ : lift.{v, u} (succ a) > succ (lift.{v, u} a)
b : Cardinal.{u}
h : b < succ a
e : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
rw [lt_succ_iff, ← lift_le, e] at h

Result:
case intro.intro
a : Cardinal.{u}
h✝ : lift.{v, u} (succ a) > succ (lift.{v, u} a)
b : Cardinal.{u}
h : succ (lift.{v, u} a) ≤ lift.{v, u} a
e : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False
-- Mathlib/Data/PNat/Prime.lean
theorem Coprime.coprime_dvd_left {m k n : ℕ+} : m ∣ k → k.Coprime n → m.Coprime n

Proof state:
m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n

Tactic:
repeat rw [← coprime_coe]

Result:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n

Proof state:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → m.Coprime n

Tactic:
rw [← coprime_coe]

Result:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n

Proof state:
m k n : ℕ+
⊢ ↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n

Tactic:
apply Nat.Coprime.coprime_dvd_left

Result:
no goals

Proof state:
m k n : ℕ+
⊢ m ∣ k → k.Coprime n → m.Coprime n

Tactic:
rw [dvd_iff]

Result:
m k n : ℕ+
⊢ ↑m ∣ ↑k → k.Coprime n → m.Coprime n
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem eq_δ₀ {n : ℕ} {i : ⦋n⦌ ⟶ ⦋n + 1⦌} [Mono i] (hi : Isδ₀ i) :
    i = SimplexCategory.δ 0

Proof state:
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
hi : Isδ₀ i
⊢ i = SimplexCategory.δ 0

Tactic:
obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono i

Result:
case intro
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Proof state:
case intro
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Tactic:
rw [iff] at hi

Result:
case intro
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Proof state:
case intro
n : ℕ
j : Fin (n + 2)
inst✝ : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Tactic:
rw [hi]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem end_mem_support {u v : V} (p : G.Walk u v) : v ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.support

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
lemma tangentCoordChange_self {x z : M} {v : E} (h : z ∈ (extChartAt I x).source) :
    tangentCoordChange I x x z v = v

Proof state:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (tangentBundleCore I M).baseSet (achart H x)

Tactic:
rw [tangentBundleCore_baseSet, coe_achart, ← extChartAt_source I]

Result:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (extChartAt I x).source

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ (tangentCoordChange I x x z) v = v

Tactic:
apply (tangentBundleCore I M).coordChange_self

Result:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (tangentBundleCore I M).baseSet (achart H x)

Proof state:
case a
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_4
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_6
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x z : M
v : E
h : z ∈ (extChartAt I x).source
⊢ z ∈ (extChartAt I x).source

Tactic:
exact h

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_filter_le_of_left_le {a b c : α} [DecidablePred (c ≤ ·)] (hac : a ≤ c) :
    {x ∈ Ico a b | c ≤ x} = Ico c b

Proof state:
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico c b

Tactic:
ext x

Result:
case h
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
x : α
⊢ x ∈ filter (fun x => c ≤ x) (Ico a b) ↔ x ∈ Ico c b

Proof state:
case h
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
x : α
⊢ a ≤ x ∧ c ≤ x ∧ x < b ↔ c ≤ x ∧ x < b

Tactic:
exact and_iff_right_of_imp fun h => hac.trans h.1

Result:
no goals

Proof state:
case h
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
x : α
⊢ x ∈ filter (fun x => c ≤ x) (Ico a b) ↔ x ∈ Ico c b

Tactic:
rw [mem_filter, mem_Ico, mem_Ico, and_comm, and_left_comm]

Result:
case h
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
x : α
⊢ a ≤ x ∧ c ≤ x ∧ x < b ↔ c ≤ x ∧ x < b
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem primPart_mul {p q : R[X]} (h0 : p * q ≠ 0) :
    (p * q).primPart = p.primPart * q.primPart

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : p * q ≠ 0
⊢ (p * q).primPart = p.primPart * q.primPart

Tactic:
rw [Ne, ← content_eq_zero_iff, ← C_eq_zero] at h0

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ (p * q).primPart = p.primPart * q.primPart

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ (p * q).primPart = p.primPart * q.primPart

Tactic:
apply mul_left_cancel₀ h0

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C (p * q).content * (p * q).primPart = C (p * q).content * (p.primPart * q.primPart)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C (p * q).content * (p.primPart * q.primPart)

Tactic:
rw [content_mul, RingHom.map_mul]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C p.content * C q.content * (p.primPart * q.primPart)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C p.content * C q.content * (p.primPart * q.primPart)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C (p * q).content * (p * q).primPart = C (p * q).content * (p.primPart * q.primPart)

Tactic:
conv_lhs =>
  rw [← (p * q).eq_C_content_mul_primPart, p.eq_C_content_mul_primPart,
    q.eq_C_content_mul_primPart]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C (p * q).content * (p.primPart * q.primPart)
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem comap_supp {S : Type*} [CommRing S] (f : S →+* R) :
    supp (v.comap f) = Ideal.comap f v.supp :=
  Ideal.ext fun x => by rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝² : CommRing R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S : Type u_7
inst✝ : CommRing S
f : S →+* R
x : S
⊢ x ∈ (comap f v).supp ↔ x ∈ Ideal.comap f v.supp

Tactic:
rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_zero_X (s : σ) : coeff R (0 : σ →₀ ℕ) (X s : MvPowerSeries σ R) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ (coeff R 0) (X s) = 0

Tactic:
classical
rw [coeff_X, if_neg]
intro h
exact one_ne_zero (single_eq_zero.mp h.symm)

Result:
no goals

Proof state:
case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ ¬0 = single s 1

Tactic:
intro h

Result:
case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
h : 0 = single s 1
⊢ False

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ (coeff R 0) (X s) = 0

Tactic:
rw [coeff_X, if_neg]

Result:
case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ ¬0 = single s 1

Proof state:
case hnc
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
h : 0 = single s 1
⊢ False

Tactic:
exact one_ne_zero (single_eq_zero.mp h.symm)

Result:
no goals