harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fract_zSpan_add (m : E) {v : E} (h : v ∈ span ℤ (Set.range b)) :
    fract b (v + m) = fract b m

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
⊢ fract b (v + m) = fract b m

Tactic:
classical
refine (Basis.ext_elem_iff b).mpr fun i => ?_
simp_rw [repr_fract_apply, Int.fract_eq_fract]
use (b.restrictScalars ℤ).repr ⟨v, h⟩ i
rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
  ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]

Result:
no goals

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (v + m)) i - (b.repr m) i = ↑(((Basis.restrictScalars ℤ b).repr ⟨v, h⟩) i)

Tactic:
rw [map_add, Finsupp.coe_add, Pi.add_apply, add_tsub_cancel_right,
  ← eq_intCast (algebraMap ℤ K) _, Basis.restrictScalars_repr_apply, coe_mk]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ ∃ z, (b.repr (v + m)) i - (b.repr m) i = ↑z

Tactic:
use (b.restrictScalars ℤ).repr ⟨v, h⟩ i

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (v + m)) i - (b.repr m) i = ↑(((Basis.restrictScalars ℤ b).repr ⟨v, h⟩) i)

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (fract b (v + m))) i = (b.repr (fract b m)) i

Tactic:
simp_rw [repr_fract_apply, Int.fract_eq_fract]

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ ∃ z, (b.repr (v + m)) i - (b.repr m) i = ↑z

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
⊢ fract b (v + m) = fract b m

Tactic:
refine (Basis.ext_elem_iff b).mpr fun i => ?_

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m v : E
h : v ∈ span ℤ (Set.range ⇑b)
i : ι
⊢ (b.repr (fract b (v + m))) i = (b.repr (fract b m)) i
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma firstReturn_lt_length : p.firstReturn < p.toList.length

Proof state:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x ∈ range (↑p).length, decide (count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)) = true

Tactic:
simp only [mem_range, decide_eq_true_eq]

Result:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x < (↑p).length, count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)

Proof state:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ (↑p).length - 1 < (↑p).length ∧
    count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)

Tactic:
exact ⟨by omega, by rw [Nat.sub_add_cancel lp, take_of_length_le (le_refl _),
  p.count_U_eq_count_D]⟩

Result:
no goals

Proof state:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)

Tactic:
rw [Nat.sub_add_cancel lp, take_of_length_le (le_refl _),
p.count_U_eq_count_D]

Result:
no goals

Proof state:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ (↑p).length - 1 < (↑p).length

Tactic:
omega

Result:
no goals

Proof state:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x < (↑p).length, count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)

Tactic:
use p.toList.length - 1

Result:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ (↑p).length - 1 < (↑p).length ∧
    count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)

Proof state:
p : DyckWord
h : p ≠ 0
⊢ p.firstReturn < (↑p).length

Tactic:
have lp := length_pos_of_ne_nil (toList_ne_nil.mpr h)

Result:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ p.firstReturn < (↑p).length

Proof state:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ p.firstReturn < (range (↑p).length).length

Tactic:
apply findIdx_lt_length_of_exists

Result:
case h
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ ∃ x ∈ range (↑p).length, decide (count U (List.take (x + 1) ↑p) = count D (List.take (x + 1) ↑p)) = true

Proof state:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ p.firstReturn < (↑p).length

Tactic:
rw [← length_range p.toList.length]

Result:
p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ p.firstReturn < (range (↑p).length).length
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma tendsto_deriv_mul_log_atTop :
    Tendsto (fun x ↦ deriv (fun x ↦ x * log x) x) atTop atTop

Proof state:
⊢ (fun x => deriv (fun x => x * log x) x) =ᶠ[atTop] fun x => log x + 1

Tactic:
rw [EventuallyEq, eventually_atTop]

Result:
⊢ ∃ a, ∀ b ≥ a, deriv (fun x => x * log x) b = log b + 1

Proof state:
⊢ Tendsto (fun x => deriv (fun x => x * log x) x) atTop atTop

Tactic:
refine (tendsto_congr' ?_).mpr (tendsto_log_atTop.atTop_add (tendsto_const_nhds (x := 1)))

Result:
⊢ (fun x => deriv (fun x => x * log x) x) =ᶠ[atTop] fun x => log x + 1

Proof state:
⊢ ∃ a, ∀ b ≥ a, deriv (fun x => x * log x) b = log b + 1

Tactic:
exact ⟨1, fun _ hx ↦ deriv_mul_log (zero_lt_one.trans_le hx).ne'⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableWithinAt_congr_set' (y : M) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f t x

Tactic:
simp only [mdifferentiableWithinAt_iff_exists_hasMFDerivWithinAt]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (∃ f', HasMFDerivWithinAt I I' f s x f') ↔ ∃ f', HasMFDerivWithinAt I I' f t x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
y : M
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ (∃ f', HasMFDerivWithinAt I I' f s x f') ↔ ∃ f', HasMFDerivWithinAt I I' f t x f'

Tactic:
exact exists_congr fun _ => hasMFDerivWithinAt_congr_set' _ h

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma log_coverMincard_le_add {T : X → X} {F : Set X} (F_inv : MapsTo T F F)
    {U : Set (X × X)} (U_symm : SymmetricRel U) {m n : ℕ} (m_pos : 0 < m) (n_pos : 0 < n) :
    log (coverMincard T F (U ○ U) n) / n
    ≤ log (coverMincard T F U m) / m + log (coverMincard T F U m) / n

Proof state:
case inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ (↑(coverMincard T F U m)).log * (↑(n / m) / ↑n) + (↑(coverMincard T F U m)).log / ↑n ≤
    (↑(coverMincard T F U m)).log * (↑m)⁻¹ + (↑(coverMincard T F U m)).log / ↑n

Tactic:
apply add_le_add_right (mul_le_mul_of_nonneg_left _ h_log)

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
m n : ℕ
m_pos : 0 < m
n_pos : 0 < n
F_nemp : F.Nonempty
h_nm : 0 ≤ ↑(n / m)
h_log : 0 ≤ (↑(coverMincard T F U m)).log
n_div_n : ↑n / ↑n = 1
⊢ ↑(n / m) / ↑n ≤ (↑m)⁻¹
-- Mathlib/NumberTheory/GaussSum.lean
theorem gaussSum_mul_aux {χ : MulChar R R'} (hχ : χ ≠ 1) (ψ : AddChar R R')
    (b : R) :
    ∑ a, χ (a * b⁻¹) * ψ (a - b) = ∑ c, χ c * ψ (b * (c - 1))

Proof state:
case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
⊢ χ x * ψ (b * (x - 1)) = χ (b * x * b⁻¹) * ψ (b * x - b)

Tactic:
rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b = 0
⊢ ∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))

Tactic:
simp only [hb, inv_zero, mul_zero, MulChar.map_zero, zero_mul,
  Finset.sum_const_zero, map_zero_eq_one, mul_one, χ.sum_eq_zero_of_ne_one hχ]

Result:
no goals

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
⊢ ∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))

Tactic:
rcases eq_or_ne b 0 with hb | hb

Result:
case inl
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b = 0
⊢ ∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))

case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
⊢ ∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))

Proof state:
case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
⊢ ∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))

Tactic:
refine (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x ↦ ?_).symm

Result:
case inr
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
⊢ χ x * ψ (b * (x - 1)) = χ (b * x * b⁻¹) * ψ (b * x - b)
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
to the integers, or is densely ordered, exclusively. -/
lemma LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered (G : Type*)
    [LinearOrderedAddCommGroup G] [Archimedean G] :
    Nonempty (G ≃+o ℤ) ↔ ¬ DenselyOrdered G

Proof state:
case inl.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
h : G ≃+o ℤ
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
simpa [this h] using ⟨h⟩

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩|h

Result:
case inl.intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
h : G ≃+o ℤ
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

case inr
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
h : DenselyOrdered G
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Proof state:
case intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered ℤ
w✝ : ℤ
h✝ : 0 < w✝ ∧ w✝ < 1
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case inr
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
h : DenselyOrdered G
⊢ IsEmpty (G ≃+o ℤ)

Tactic:
exact ⟨fun H ↦ (this H) h⟩

Result:
no goals

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered ℤ
⊢ False

Tactic:
obtain ⟨_, _⟩ := exists_between (one_pos (α := ℤ))

Result:
case intro
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered ℤ
w✝ : ℤ
h✝ : 0 < w✝ ∧ w✝ < 1
⊢ False

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
⊢ (G ≃+o ℤ) → ¬DenselyOrdered G

Tactic:
intro e H

Result:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered G
⊢ False

Proof state:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered G
⊢ False

Tactic:
rw [denselyOrdered_iff_of_orderIsoClass e] at H

Result:
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
e : G ≃+o ℤ
H : DenselyOrdered ℤ
⊢ False

Proof state:
case inr
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
h : DenselyOrdered G
⊢ Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G

Tactic:
simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]

Result:
case inr
G : Type u_2
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : Archimedean G
this : (G ≃+o ℤ) → ¬DenselyOrdered G
h : DenselyOrdered G
⊢ IsEmpty (G ≃+o ℤ)
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_ideal_over_prime_of_isIntegral_of_isPrime
    [Algebra.IsIntegral R S] (P : Ideal R) [IsPrime P]
    (I : Ideal S) [IsPrime I] (hIP : I.comap (algebraMap R S) ≤ P) :
    ∃ Q ≥ I, IsPrime Q ∧ Q.comap (algebraMap R S) = P

Proof state:
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap (algebraMap R S) (comap (Quotient.mk I) Q') = P

Tactic:
rw [comap_comap]

Result:
case intro.intro
R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
Q' : Ideal (S ⧸ I)
Q'_prime : Q'.IsPrime
hQ' : comap (algebraMap (R ⧸ comap (algebraMap R S) I) (S ⧸ I)) Q' = map (Quotient.mk (comap (algebraMap R S) I)) P
⊢ comap ((Quotient.mk I).comp (algebraMap R S)) Q' = P
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_le_sub_one_of_pos {x : ℝ} (hx : 0 < x) : log x ≤ x - 1

Proof state:
x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x

Tactic:
convert add_one_le_exp (log x)

Result:
case h.e'_4
x : ℝ
hx : 0 < x
⊢ x = rexp (log x)

Proof state:
case h.e'_4
x : ℝ
hx : 0 < x
⊢ x = rexp (log x)

Tactic:
rw [exp_log hx]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
⊢ log x ≤ x - 1

Tactic:
rw [le_sub_iff_add_le]

Result:
x : ℝ
hx : 0 < x
⊢ log x + 1 ≤ x
-- Mathlib/Analysis/Convex/Cone/Extension.lean
theorem step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
    (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) (hdom : f.domain ≠ ⊤) :
    ∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x

Proof state:
case refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
⊢ ∀ x ∈ Sn, ∀ y ∈ Sp, x ≤ y

Tactic:
rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩

Result:
case refine_2.intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
xn : ↥f.domain
hxn : xn ∈ {x | -↑x - y ∈ s}
xp : ↥f.domain
hxp : xp ∈ {x | ↑x + y ∈ s}
⊢ ↑f xn ≤ ↑f xp

Proof state:
case intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
⊢ f < f.supSpanSingleton y (-c) hy

Tactic:
refine lt_iff_le_not_le.2 ⟨f.left_le_sup _ _, fun H => ?_⟩

Result:
case intro.intro.intro.intro.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : ConvexCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
H : f.supSpanSingleton y (-c) hy ≤ f
⊢ False
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[simp]
lemma homologyMap_neg : homologyMap (-φ) i = -homologyMap φ i

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) =
    ShortComplex.homologyMap (-(shortComplexFunctor C c i).map φ)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) =
    -ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ)

Tactic:
rw [← ShortComplex.homologyMap_neg]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) =
    ShortComplex.homologyMap (-(shortComplexFunctor C c i).map φ)

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (-φ) i = -homologyMap φ i

Tactic:
dsimp [homologyMap]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (-φ)) =
    -ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ)
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
lemma deltaGenerated_mono {X : Type*} {t₁ t₂ : TopologicalSpace X} (h : t₁ ≤ t₂) :
    @deltaGenerated X t₁ ≤ @deltaGenerated X t₂

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
⊢ deltaGenerated X ≤ deltaGenerated X

Tactic:
rw [← continuous_id_iff_le, @continuous_to_deltaGenerated _ _
  (@deltaGenerated X t₁) t₂ deltaGeneratedSpace_deltaGenerated id]

Result:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
⊢ Continuous id

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h : t₁ ≤ t₂
⊢ Continuous id

Tactic:
exact continuous_id_iff_le.2 <| (@deltaGenerated_le X t₁).trans h

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem eval_ker {ι : Type*} (b : Basis ι R M) :
    LinearMap.ker (Dual.eval R M) = ⊥

Proof state:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ∀ (x : Dual R M), x m = 0
⊢ m = 0

Tactic:
exact (Basis.forall_coord_eq_zero_iff _).mp fun i => hm (b.coord i)

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m : M
hm : (Dual.eval R M) m = 0
⊢ m = 0

Tactic:
simp_rw [LinearMap.ext_iff, Dual.eval_apply, zero_apply] at hm

Result:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ∀ (x : Dual R M), x m = 0
⊢ m = 0

Proof state:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
⊢ ∀ (m : M), (Dual.eval R M) m = 0 → m = 0

Tactic:
intro m hm

Result:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m : M
hm : (Dual.eval R M) m = 0
⊢ m = 0

Proof state:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
⊢ ker (Dual.eval R M) = ⊥

Tactic:
rw [ker_eq_bot']

Result:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
⊢ ∀ (m : M), (Dual.eval R M) m = 0 → m = 0
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_subtype {s : Set α} (hs : MeasurableSet s) (t : Set s) (f : α → ℝ≥0∞) :
    ∫⁻ x in t, f x ∂(μ.comap (↑)) = ∫⁻ x in (↑) '' t, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set ↑s
f : α → ℝ≥0∞
⊢ ∫⁻ (x : ↑s) in t, f ↑x ∂Measure.comap Subtype.val μ = ∫⁻ (x : α) in Subtype.val '' t, f x ∂μ

Tactic:
rw [(MeasurableEmbedding.subtype_coe hs).restrict_comap, lintegral_subtype_comap hs,
  restrict_restrict hs, inter_eq_right.2 (Subtype.coe_image_subset _ _)]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_tri_left' (n m : ℕ) : n ≤ dist n m + m

Proof state:
n m : ℕ
⊢ n ≤ n.dist m + m

Tactic:
rw [dist_comm]

Result:
n m : ℕ
⊢ n ≤ m.dist n + m

Proof state:
n m : ℕ
⊢ n ≤ m.dist n + m

Tactic:
apply dist_tri_left

Result:
no goals