harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finsupp/Multiset.lean
@[simp] lemma coe_equivNatSumOfFintype_symm_apply [Fintype α] (P : {P : α → ℕ // ∑ i, P i = n}) :
    ((equivNatSumOfFintype α n).symm P : Multiset α) = ∑ a, ((P : α → ℕ) a) • {a}

Proof state:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
⊢ Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = (Multiset.map (fun a => ↑⟨P, hP⟩ a • {a}) univ.val).sum

Tactic:
ext a

Result:
case mk.a
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    Multiset.count a (Multiset.map (fun a => ↑⟨P, hP⟩ a • {a}) univ.val).sum

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : { P // ∑ i : α, P i = n }
⊢ ↑((equivNatSumOfFintype α n).symm P) = ∑ a : α, ↑P a • {a}

Tactic:
obtain ⟨P, hP⟩ := P

Result:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
⊢ ↑((equivNatSumOfFintype α n).symm ⟨P, hP⟩) = ∑ a : α, ↑⟨P, hP⟩ a • {a}

Proof state:
case mk.a
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    Multiset.count a (Multiset.map (fun a => ↑⟨P, hP⟩ a • {a}) univ.val).sum

Tactic:
rw [Multiset.count_sum]

Result:
case mk.a
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    (Multiset.map (fun b => Multiset.count a (↑⟨P, hP⟩ b • {b})) univ.val).sum

Proof state:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
⊢ ↑((equivNatSumOfFintype α n).symm ⟨P, hP⟩) = ∑ a : α, ↑⟨P, hP⟩ a • {a}

Tactic:
change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _

Result:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
⊢ Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = (Multiset.map (fun a => ↑⟨P, hP⟩ a • {a}) univ.val).sum

Proof state:
case mk.a
α : Type u_1
inst✝¹ : DecidableEq α
n : ℕ
inst✝ : Fintype α
P : α → ℕ
hP : ∑ i : α, P i = n
a : α
⊢ Multiset.count a (Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P)) =
    (Multiset.map (fun b => Multiset.count a (↑⟨P, hP⟩ b • {b})) univ.val).sum

Tactic:
simp [Multiset.count_singleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_pow_succ (p : R[X]) (n : ℕ) :
    derivative (p ^ (n + 1)) = C (n + 1 : R) * p ^ n * derivative p :=
  Nat.recOn n (by simp) fun n ih => by
    rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
      add_mul, add_mul, pow_succ, ← mul_assoc, C_1, one_mul]; simp [add_mul]

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
⊢ derivative (p ^ (Nat.zero + 1)) = C (↑Nat.zero + 1) * p ^ Nat.zero * derivative p

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + p ^ n * p) * derivative p + p ^ n * p * derivative p = C (↑n.succ + 1) * p ^ n * p * derivative p

Tactic:
simp [add_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ derivative (p ^ (n.succ + 1)) = C (↑n.succ + 1) * p ^ n.succ * derivative p

Tactic:
rw [pow_succ, derivative_mul, ih, Nat.add_one, mul_right_comm, C_add,
  add_mul, add_mul, pow_succ, ← mul_assoc, C_1, one_mul]

Result:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n✝ n : ℕ
ih : derivative (p ^ (n + 1)) = C (↑n + 1) * p ^ n * derivative p
⊢ (C ↑n * p ^ n * p + p ^ n * p) * derivative p + p ^ n * p * derivative p = C (↑n.succ + 1) * p ^ n * p * derivative p
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/--
The uniform norm of the `k`-th Mahler basis function is 1, for every `k`.
-/
@[simp] lemma norm_mahler_eq (k : ℕ) : ‖(mahler k : C(ℤ_[p], ℚ_[p]))‖ = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ ‖mahler k‖ = 1

Tactic:
apply le_antisymm

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ ‖mahler k‖ ≤ 1

case a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ 1 ≤ ‖mahler k‖

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ 1 = ‖(mahler k) ↑k‖

Tactic:
rw [mahler_natCast_eq, Nat.choose_self, Nat.cast_one, norm_one]

Result:
no goals

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ 1 ≤ ‖mahler k‖

Tactic:
refine (le_of_eq ?_).trans ((mahler k).norm_coe_le_norm k)

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ 1 = ‖(mahler k) ↑k‖

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ ‖mahler k‖ ≤ 1

Tactic:
exact (mahler k).norm_le_of_nonempty.mpr (fun _ ↦ PadicInt.norm_le_one _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_reverse (a : Array α) : a.reverse.size = a.size

Proof state:
α : Type u_1
a as : Array α
i : Nat
j : Fin as.size
⊢ (reverse.loop as i j).size = as.size

Tactic:
rw [reverse.loop]

Result:
α : Type u_1
a as : Array α
i : Nat
j : Fin as.size
⊢ (if h : i < ↑j then
        let_fun this := ⋯;
        let as_1 := as.swap i ↑j ⋯ ⋯;
        let_fun this := ⋯;
        reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩
      else as).size =
    as.size

Proof state:
α : Type u_1
a : Array α
⊢ (if h : a.size ≤ 1 then a else reverse.loop a 0 ⟨a.size - 1, ⋯⟩).size = a.size

Tactic:
split <;> simp [go]

Result:
no goals

Proof state:
α : Type u_1
a as : Array α
i : Nat
j : Fin as.size
h : ¬i < ↑j
⊢ (if h : i < ↑j then
        let_fun this := ⋯;
        let as_1 := as.swap i ↑j ⋯ ⋯;
        let_fun this := ⋯;
        reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩
      else as).size =
    as.size

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
a : Array α
⊢ a.reverse.size = a.size

Tactic:
simp only [reverse]

Result:
α : Type u_1
a : Array α
⊢ (if h : a.size ≤ 1 then a else reverse.loop a 0 ⟨a.size - 1, ⋯⟩).size = a.size
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_int_mul_two_pi_sub_pi (n : ℤ) : cos (n * (2 * π) - π) = -1

Proof state:
n : ℤ
⊢ cos (↑n * (2 * ↑π) - ↑π) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
/-- In a preconnected space, if a symmetric transitive relation `P x y` is true for `y` close
enough to `x`, then it holds for all `x, y`. This is a version of the fact that, if an equivalence
relation has open classes, then it has a single equivalence class. -/
lemma PreconnectedSpace.induction₂ [PreconnectedSpace α] (P : α → α → Prop)
    (h : ∀ x, ∀ᶠ y in 𝓝 x, P x y) (h' : Transitive P) (h'' : Symmetric P) (x y : α) :
    P x y

Proof state:
case h
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : Transitive P
h'' : Symmetric P
x y z a : α
ha : P z a
⊢ P z a ∧ P a z

Tactic:
exact ⟨ha, h'' ha⟩

Result:
no goals

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : Transitive P
h'' : Symmetric P
x y : α
⊢ P x y

Tactic:
refine PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y

Result:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : Transitive P
h'' : Symmetric P
x y z : α
⊢ ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : Transitive P
h'' : Symmetric P
x y z : α
⊢ ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z

Tactic:
filter_upwards [h z] with a ha

Result:
case h
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : Transitive P
h'' : Symmetric P
x y z a : α
ha : P z a
⊢ P z a ∧ P a z
-- Mathlib/Data/Nat/Find.lean
@[simp] lemma findGreatest_pos : 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Proof state:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (Exists fun ⦃n⦄ => 0 < n ∧ n ≤ k ∧ P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
rfl

Result:
no goals

Proof state:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
push_neg

Result:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (Exists fun ⦃n⦄ => 0 < n ∧ n ≤ k ∧ P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Proof state:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ 0 < findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]

Result:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem exists_of_eraseP : ∀ {l : List α} {a} (_ : a ∈ l) (_ : p a),
    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂
  | b :: l, _, al, pa =>
    if pb : p b then
      ⟨b, [], l, forall_mem_nil _, pb, by simp [pb]⟩
    else
      match al with
      | .head .. => nomatch pb pa
      | .tail _ al =>
        let ⟨c, l₁, l₂, h₁, h₂, h₃, h₄⟩ := exists_of_eraseP al pa
        ⟨c, b::l₁, l₂, (forall_mem_cons ..).2 ⟨pb, h₁⟩,
          h₂, by rw [h₃, cons_append], by simp [pb, h₄]⟩

Proof state:
α : Type u_1
p : α → Bool
b✝ : α
l : List α
x✝ : α
al✝ : x✝ ∈ b✝ :: l
pa : p x✝ = true
b : α
al : Mem x✝ l
pb : ¬p b = true
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ eraseP p (b :: l) = b :: l₁ ++ l₂

Tactic:
simp [pb, h₄]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
b✝ : α
l : List α
x✝ : α
al✝ : x✝ ∈ b✝ :: l
pa : p x✝ = true
b : α
al : Mem x✝ l
pb : ¬p b = true
c : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ b :: l = b :: l₁ ++ c :: l₂

Tactic:
rw [h₃, cons_append]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
b : α
l : List α
x✝ : α
al : x✝ ∈ b :: l
pa : p x✝ = true
pb : p b = true
⊢ b :: l = [] ++ b :: l ∧ eraseP p (b :: l) = [] ++ l

Tactic:
simp [pb]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem Fintype.prod_dite [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β]
    (f : ∀ a, p a → β) (g : ∀ a, ¬p a → β) :
    (∏ a, dite (p a) (f a) (g a)) =
    (∏ a : { a // p a }, f a a.2) * ∏ a : { a // ¬p a }, g a a.2

Proof state:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x ⋯ = ∏ a : { a // p a }, f ↑a ⋯

Tactic:
exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // p x } => f x x.2

Result:
no goals

Proof state:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x ⋯ = ∏ a : { a // ¬p a }, g ↑a ⋯

Tactic:
exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // ¬p x } => g x x.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x ⋯) * ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x ⋯ =
    (∏ a : { a // p a }, f ↑a ⋯) * ∏ a : { a // ¬p a }, g ↑a ⋯

Tactic:
congr 1

Result:
case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x ⋯ = ∏ a : { a // p a }, f ↑a ⋯

case e_a
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x ⋯ = ∏ a : { a // ¬p a }, g ↑a ⋯

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => p x) univ ↔ p x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∏ a : α, dite (p a) (f a) (g a) = (∏ a : { a // p a }, f ↑a ⋯) * ∏ a : { a // ¬p a }, g ↑a ⋯

Tactic:
simp only [prod_dite, attach_eq_univ]

Result:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ (∏ x : { x // x ∈ filter (fun x => p x) univ }, f ↑x ⋯) * ∏ x : { x // x ∈ filter (fun x => ¬p x) univ }, g ↑x ⋯ =
    (∏ a : { a // p a }, f ↑a ⋯) * ∏ a : { a // ¬p a }, g ↑a ⋯

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), x ∈ filter (fun x => ¬p x) univ ↔ ¬p x

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem ae_empty_or_univ (hf : PreErgodic f μ) (hs : MeasurableSet s) (hfs : f ⁻¹' s = s) :
    s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
hf : PreErgodic f μ
hs : MeasurableSet s
hfs : f ⁻¹' s = s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
simpa only [eventuallyConst_set'] using hf.aeconst_set hs hfs

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem isUnit_res_toΓSpecMapBasicOpen : IsUnit (X.toToΓSpecMapBasicOpen r r)

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsUnit ((ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r)

Tactic:
convert
  (X.presheaf.map <| (eqToHom <| X.toΓSpecMapBasicOpen_eq r).op).hom.isUnit_map
    (X.toRingedSpace.isUnit_res_basicOpen r)

Result:
case h.e'_3
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (X.toRingedSpace.presheaf.map (homOfLE ⋯).op)) r)

Proof state:
case h.e'_3
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r

Tactic:
congr

Result:
no goals

Proof state:
case h.e'_3
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op))
      ((ConcreteCategory.hom (X.toRingedSpace.presheaf.map (homOfLE ⋯).op)) r)

Tactic:
rw [← CommRingCat.comp_apply, ← Functor.map_comp]

Result:
case h.e'_3
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r
-- Mathlib/RingTheory/Ideal/Height.lean
theorem Ideal.height_mono {I J : Ideal R} (h : I ≤ J) : I.height ≤ J.height

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ I.height ≤ J.height

Tactic:
simp only [height]

Result:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ ⨅ J_1, ⨅ (h : J_1 ∈ J.minimalPrimes), J_1.primeHeight

Proof state:
case h.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this✝ : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
this : q.IsPrime
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Tactic:
exact (iInf₂_le q hq).trans (Ideal.primeHeight_mono e)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ ⨅ J_1, ⨅ (h : J_1 ∈ J.minimalPrimes), J_1.primeHeight

Tactic:
apply le_iInf₂

Result:
case h
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ ∀ (i : Ideal R) (j : i ∈ J.minimalPrimes), ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ i.primeHeight

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Tactic:
obtain ⟨q, hq, e⟩ := Ideal.exists_minimalPrimes_le (h.trans hp.1.2)

Result:
case h.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
⊢ ∀ (i : Ideal R) (j : i ∈ J.minimalPrimes), ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ i.primeHeight

Tactic:
intro p hp

Result:
case h
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Tactic:
have := Ideal.minimalPrimes_isPrime hp

Result:
case h
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Proof state:
case h.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight

Tactic:
haveI := Ideal.minimalPrimes_isPrime hq

Result:
case h.intro.intro
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I ≤ J
p : Ideal R
hp : p ∈ J.minimalPrimes
this✝ : p.IsPrime
q : Ideal R
hq : q ∈ I.minimalPrimes
e : q ≤ p
this : q.IsPrime
⊢ ⨅ J, ⨅ (h : J ∈ I.minimalPrimes), J.primeHeight ≤ p.primeHeight
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem reflectsColimit_of_comp {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B}
    [ReflectsColimit (F ⋙ G) H] : ReflectsColimit G H where
  reflects {c} hc

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ IsColimit (H.mapCocone (Cocone.whisker F c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocones.ext (Iso.refl _) (by simp))

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨isColimitWhiskerEquiv F _ (isColimitOfReflects H ?_)⟩

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
⊢ IsColimit (H.mapCocone (Cocone.whisker F c))

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ ∀ (j : C),
    (Cocone.whisker F (H.mapCocone c)).ι.app j ≫ (Iso.refl (Cocone.whisker F (H.mapCocone c)).pt).hom =
      (H.mapCocone (Cocone.whisker F c)).ι.app j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
⊢ IsColimit (H.mapCocone (Cocone.whisker F c))

Tactic:
let hc' := (isColimitWhiskerEquiv F _).symm hc

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) := (isColimitWhiskerEquiv F (H.mapCocone c)).symm hc
⊢ IsColimit (H.mapCocone (Cocone.whisker F c))
-- Mathlib/Order/SuccPred/Basic.lean
theorem Icc_succ_left_of_not_isMax (ha : ¬IsMax a) : Icc (succ a) b = Ioc a b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Icc (succ a) b = Ioc a b

Tactic:
rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys

Proof state:
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ ++ [a] = toList✝ ++ [b]
⊢ [a].length = [b].length

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.push a = { toList := toList✝ }.push b
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
simp at h

Result:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ ++ [a] = toList✝ ++ [b]
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
case mk
α : Type u_1
a b : α
ys : Array α
toList✝ : List α
h : { toList := toList✝ }.push a = ys.push b
⊢ { toList := toList✝ } = ys

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : { toList := toList✝¹ }.push a = { toList := toList✝ }.push b
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
α : Type u_1
a b : α
xs ys : Array α
h : xs.push a = ys.push b
⊢ xs = ys

Tactic:
cases xs

Result:
case mk
α : Type u_1
a b : α
ys : Array α
toList✝ : List α
h : { toList := toList✝ }.push a = ys.push b
⊢ { toList := toList✝ } = ys

Proof state:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ ++ [a] = toList✝ ++ [b]
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
replace h := List.append_inj_left' h (by simp)

Result:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ = toList✝
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
case mk.mk
α : Type u_1
a b : α
toList✝¹ toList✝ : List α
h : toList✝¹ = toList✝
⊢ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
simp [h]

Result:
no goals