harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem cauchy_iff {f : Filter α} : Cauchy f ↔ NeBot f ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s :=
  cauchy_iff'.trans <| by
    simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
⊢ (f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s) ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s

Tactic:
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem exists_not_mem_row (μ : YoungDiagram) (i : ℕ) : ∃ j, (i, j) ∉ μ

Proof state:
μ : YoungDiagram
i : ℕ
⊢ ∃ j, (i, j) ∉ μ

Tactic:
obtain ⟨j, hj⟩ :=
  Infinite.exists_not_mem_finset
    (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
      cases h
      rfl)

Result:
case intro
μ : YoungDiagram
i j : ℕ
hj : j ∉ μ.cells.preimage (Prod.mk i) ⋯
⊢ ∃ j, (i, j) ∉ μ

Proof state:
case intro
μ : YoungDiagram
i j : ℕ
hj : (i, j) ∉ μ.cells
⊢ ∃ j, (i, j) ∉ μ

Tactic:
exact ⟨j, hj⟩

Result:
no goals

Proof state:
μ : YoungDiagram
i x✝³ : ℕ
x✝² : x✝³ ∈ Prod.mk i ⁻¹' ↑μ.cells
x✝¹ : ℕ
x✝ : x✝¹ ∈ Prod.mk i ⁻¹' ↑μ.cells
h : (i, x✝³) = (i, x✝¹)
⊢ x✝³ = x✝¹

Tactic:
cases h

Result:
case refl
μ : YoungDiagram
i x✝² : ℕ
x✝¹ x✝ : x✝² ∈ Prod.mk i ⁻¹' ↑μ.cells
⊢ x✝² = x✝²

Proof state:
case intro
μ : YoungDiagram
i j : ℕ
hj : j ∉ μ.cells.preimage (Prod.mk i) ⋯
⊢ ∃ j, (i, j) ∉ μ

Tactic:
rw [Finset.mem_preimage] at hj

Result:
case intro
μ : YoungDiagram
i j : ℕ
hj : (i, j) ∉ μ.cells
⊢ ∃ j, (i, j) ∉ μ

Proof state:
case refl
μ : YoungDiagram
i x✝² : ℕ
x✝¹ x✝ : x✝² ∈ Prod.mk i ⁻¹' ↑μ.cells
⊢ x✝² = x✝²

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem comap_op_one :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (1 : Submodule R Aᵐᵒᵖ) = 1

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ comap (↑(opLinearEquiv R)) 1 = 1

Tactic:
ext

Result:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 1 ↔ x✝ ∈ 1

Proof state:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 1 ↔ x✝ ∈ 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_empty : ∫ x in ∅, f x ∂μ = 0

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
⊢ ∫ (x : X) in ∅, f x ∂μ = 0

Tactic:
rw [Measure.restrict_empty, integral_zero_measure]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem exists_unit (w₁ : InfinitePlace K) :
    ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0

Proof state:
case intro.intro.intro.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
hu : Associated ↑(seq K w₁ hB n) ↑(seq K w₁ hB m)
w : InfinitePlace K
hw : w ≠ w₁
⊢ w ((algebraMap (𝓞 K) K) ↑(Exists.choose hu)) < 1

Tactic:
calc
  _ = w (algebraMap (𝓞 K) K (seq K w₁ hB m) * (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹) := by
    rw [← congr_arg (algebraMap (𝓞 K) K) hu.choose_spec, mul_comm, map_mul (algebraMap _ _),
    ← mul_assoc, inv_mul_cancel₀ (seq_ne_zero K w₁ hB n), one_mul]
_ = w (algebraMap (𝓞 K) K (seq K w₁ hB m)) * w (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹ :=
  _root_.map_mul _ _ _
_ < 1 := by
  rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]
  exact seq_decreasing K w₁ hB hnm w hw

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

Tactic:
rsuffices ⟨n, m, hnm, h⟩ : ∃ n m, n < m ∧
    (Ideal.span ({ (seq K w₁ hB n : 𝓞 K) }) = Ideal.span ({ (seq K w₁ hB m : 𝓞 K) }))

Result:
case intro.intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ n m, n < m ∧ Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
-- Mathlib/Geometry/Euclidean/Sphere/Power.lean
theorem mul_dist_eq_abs_sub_sq_dist {a b p q : P} (hp : ∃ k : ℝ, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p))
    (hq : dist a q = dist b q) : dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
have h3 := vsub_sub_vsub_cancel_left a q m

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
have h2 := vsub_sub_vsub_cancel_left p q m

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
have h1 := vsub_sub_vsub_cancel_left a p m

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|
-- Mathlib/Order/WellFoundedSet.lean
theorem IsWF.isPWO (hs : s.IsWF) : s.IsPWO

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
m : ℕ
hm : ∀ (i : ℕ), ↑(f m) ≤ ↑(f i)
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)

Tactic:
exact ⟨m, m + 1, by omega, hm _⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
⊢ s.IsPWO

Tactic:
intro f hf

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) (f m) (f n)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) (f m) (f n)

Tactic:
lift f to ℕ → s using hf

Result:
case intro
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
m : ℕ
hm : ∀ (i : ℕ), ↑(f m) ≤ ↑(f i)
⊢ m < m + 1

Tactic:
omega

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)

Tactic:
rcases hs.has_min (range f) (range_nonempty _) with ⟨_, ⟨m, rfl⟩, hm⟩

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
m : ℕ
hm : ∀ x ∈ range f, ¬(fun x1 x2 => x1 < x2) ↑x ↑(f m)
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
m : ℕ
hm : ∀ x ∈ range f, ¬(fun x1 x2 => x1 < x2) ↑x ↑(f m)
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)

Tactic:
simp only [forall_mem_range, not_lt] at hm

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrder α
s : Set α
hs : s.IsWF
f : ℕ → ↑s
m : ℕ
hm : ∀ (i : ℕ), ↑(f m) ≤ ↑(f i)
⊢ ∃ m n, m < n ∧ (fun x1 x2 => x1 ≤ x2) ((fun i => ↑(f i)) m) ((fun i => ↑(f i)) n)
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem contMDiff_finprod_cond (hc : ∀ i, p i → ContMDiff I' I n (f i))
    (hf : LocallyFinite fun i => mulSupport (f i)) :
    ContMDiff I' I n fun x => ∏ᶠ (i) (_ : p i), f i x

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : ι → M → G
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (j : Subtype p), f (↑j) x

Tactic:
exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : ι → M → G
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (i : ι) (_ : p i), f i x

Tactic:
simp only [← finprod_subtype_eq_finprod_cond]

Result:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_3
inst✝¹¹ : TopologicalSpace H
E : Type u_4
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_5
inst✝⁸ : CommMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_6
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_7
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : ι → M → G
p : ι → Prop
hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)
hf : LocallyFinite fun i => mulSupport (f i)
⊢ ContMDiff I' I n fun x => ∏ᶠ (j : Subtype p), f (↑j) x
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem ideal_prod_prime_aux {I : Ideal R} {J : Ideal S} :
    (Ideal.prod I J).IsPrime → I = ⊤ ∨ J = ⊤

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (1, 0) ∉ I.prod J

Tactic:
simp [hI]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) ∉ I.prod J

Tactic:
simp [hJ]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ 1 ∉ I ∧ 1 ∉ J → 1 ∉ I.prod J → ∃ x x_1, ∃ (_ : x * x_1 ∈ I.prod J), x ∉ I.prod J ∧ x_1 ∉ I.prod J

Tactic:
exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x✝¹ : 1 ∉ I ∧ 1 ∉ J
x✝ : 1 ∉ I.prod J
hI : 1 ∉ I
hJ : 1 ∉ J
⊢ (0, 1) * (1, 0) ∈ I.prod J

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ (I.prod J).IsPrime → I = ⊤ ∨ J = ⊤

Tactic:
contrapose!

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬(I.prod J).IsPrime

Tactic:
simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ 1 ∉ I ∧ 1 ∉ J → 1 ∉ I.prod J → ∃ x x_1, ∃ (_ : x * x_1 ∈ I.prod J), x ∉ I.prod J ∧ x_1 ∉ I.prod J
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_map_le (f : M →ₗ[R] M') (p : Submodule R M) :
    Cardinal.lift.{v} (Module.rank R (p.map f)) ≤ Cardinal.lift.{v'} (Module.rank R p)

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
have h := lift_rank_range_le (f.comp (Submodule.subtype p))

Result:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(LinearMap.range (f ∘ₗ p.subtype))) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
h : lift.{v, v'} (Module.rank R ↥(LinearMap.range (f ∘ₗ p.subtype))) ≤ lift.{v', v} (Module.rank R ↥p)
⊢ lift.{v, v'} (Module.rank R ↥(Submodule.map f p)) ≤ lift.{v', v} (Module.rank R ↥p)

Tactic:
rwa [LinearMap.range_comp, range_subtype] at h

Result:
no goals
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The auxiliary function agrees on `re s > 1` with the L-series of the von Mangoldt function
restricted to the residue class `a : ZMod q` minus the principal part `(q.totient)⁻¹/(s-1)`
of its pole at `s = 1`. -/
lemma eqOn_LFunctionResidueClassAux (ha : IsUnit a) :
    Set.EqOn (LFunctionResidueClassAux a)
      (fun s ↦ L ↗(residueClass a) s - (q.totient : ℂ)⁻¹ / (s - 1))
      {s | 1 < s.re}

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s = deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
rw [deriv_LFunctionTrivChar₁_apply_of_ne_one _ hs₁, LFunctionTrivChar₁,
  Function.update_of_ne hs₁, LFunctionTrivChar, add_div,
  mul_div_mul_left _ _ (sub_ne_zero_of_ne hs₁)]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)

Tactic:
conv_lhs => enter [2, 1]; rw [← mul_one (LFunction ..)]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
⊢ deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s * 1 / ((s - 1) * LFunction 1 s) =
    deriv (LFunction 1) s / LFunction 1 s + 1 / (s - 1)
-- Mathlib/Data/DFinsupp/Defs.lean
theorem update_self : f.update i (f i) = f

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (f.update i (f i)) i✝ = f i✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update i (f i) = f

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (f.update i (f i)) i✝ = f i✝
-- Mathlib/Analysis/Convex/Continuous.lean
protected lemma ConcaveOn.locallyLipschitz (hf : ConcaveOn ℝ univ f) : LocallyLipschitz f

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hf : ConcaveOn ℝ univ f
⊢ LocallyLipschitz f

Tactic:
simpa using hf.locallyLipschitzOn_interior

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem sub_mem_orthogonal_of_inner_right {x y : E} (h : ∀ v : K, ⟪(v : E), x⟫ = ⟪(v : E), y⟫) :
    x - y ∈ Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u x = inner u y

Tactic:
exact h ⟨u, hu⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner (↑v) x = inner (↑v) y
⊢ x - y ∈ Kᗮ

Tactic:
intro u hu

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u (x - y) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u (x - y) = 0

Tactic:
rw [inner_sub_right, sub_eq_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u x = inner u y
-- Mathlib/Data/Nat/Dist.lean
theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
  calc
    dist (n + k) (m + k) = n + k - (m + k) + (m + k - (n + k)) := rfl
    _ = n - m + (m + k - (n + k))

Proof state:
n k m : ℕ
⊢ n + k - (m + k) + (m + k - (n + k)) = n - m + (m + k - (n + k))

Tactic:
rw [@add_tsub_add_eq_tsub_right]

Result:
no goals

Proof state:
n k m : ℕ
⊢ n - m + (m + k - (n + k)) = n - m + (m - n)

Tactic:
rw [@add_tsub_add_eq_tsub_right]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaEquiv_symm_naturality_left {X X' : C} (f : X' ⟶ X) (F : Sheaf J (Type v))
    (x : F.val.obj ⟨X⟩) : J.yoneda.map f ≫ J.yonedaEquiv.symm x = J.yonedaEquiv.symm
      ((F.val.map f.op) x)

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.val.obj (op X)
⊢ J.yonedaEquiv (J.yoneda.map f ≫ J.yonedaEquiv.symm x) = J.yonedaEquiv (J.yonedaEquiv.symm (F.val.map f.op x))

Tactic:
simp only [yonedaEquiv_comp, yoneda_obj_obj, yonedaEquiv_symm_app_apply, Equiv.apply_symm_apply]

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.val.obj (op X)
⊢ F.val.map (Quiver.Hom.op (J.yonedaEquiv (J.yoneda.map f))) x = F.val.map f.op x

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.val.obj (op X)
⊢ F.val.map (Quiver.Hom.op (J.yonedaEquiv (J.yoneda.map f))) x = F.val.map f.op x

Tactic:
rw [yonedaEquiv_yoneda_map]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.val.obj (op X)
⊢ J.yoneda.map f ≫ J.yonedaEquiv.symm x = J.yonedaEquiv.symm (F.val.map f.op x)

Tactic:
apply J.yonedaEquiv.injective

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type v)
x : F.val.obj (op X)
⊢ J.yonedaEquiv (J.yoneda.map f ≫ J.yonedaEquiv.symm x) = J.yonedaEquiv (J.yonedaEquiv.symm (F.val.map f.op x))
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_mono (h : s ⊆ t) : s.sym2 ⊆ t.sym2

Proof state:
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.val.sym2 ≤ t.val.sym2

Tactic:
apply Multiset.sym2_mono

Result:
case h
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.val ≤ t.val

Proof state:
case h
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.val ≤ t.val

Tactic:
rwa [val_le_iff]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.sym2 ⊆ t.sym2

Tactic:
rw [← val_le_iff, sym2_val, sym2_val]

Result:
α : Type u_1
s t : Finset α
h : s ⊆ t
⊢ s.val.sym2 ≤ t.val.sym2
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_toMeasurable_add_inter_left {s t : Set α} (hs : MeasurableSet s)
    (ht : (μ + ν) t ≠ ∞) : μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : ¬μ t = ⊤ ∧ ¬ν t = ⊤
⊢ μ t ≠ ⊤

Tactic:
exact ht.1

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ μ t = μ (toMeasurable (μ + ν) t)

Tactic:
refine
  measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
    (measure_toMeasurable t).symm

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ (μ + ν) (toMeasurable (μ + ν) t) ≠ ⊤

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ μ t ≠ ⊤

Tactic:
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht

Result:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : ¬μ t = ⊤ ∧ ¬ν t = ⊤
⊢ μ t ≠ ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ μ (toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)

Tactic:
refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ μ t = μ (toMeasurable (μ + ν) t)

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ μ t ≠ ⊤

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : (μ + ν) t ≠ ⊤
⊢ (μ + ν) (toMeasurable (μ + ν) t) ≠ ⊤

Tactic:
rwa [measure_toMeasurable t]

Result:
no goals