harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_untop :
    ∀ (a : WithTop α) (ha : a ≠ ⊤),
      pred (a.untop ha) = (pred a).untop (by induction a <;> simp)
  | ⊤, ha => (ha rfl).elim
  | (a : α), _ => rfl

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha : a ≠ ⊤
⊢ pred a ≠ ⊤

Tactic:
induction a <;> simp

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
    δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Proof state:
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ j.succ = δ j ≫ δ i.castSucc

Tactic:
apply CategoryTheory.Quotient.sound

Result:
case h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel (Paths.of.map (FreeSimplexQuiver.Hom.δ i) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ j.succ))
    (Paths.of.map (FreeSimplexQuiver.Hom.δ j) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i.castSucc))

Proof state:
case h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ FreeSimplexQuiver.homRel (Paths.of.map (FreeSimplexQuiver.Hom.δ i) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ j.succ))
    (Paths.of.map (FreeSimplexQuiver.Hom.δ j) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i.castSucc))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_δ H

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem disjoint_sup_left : Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

Tactic:
simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem hnot_le_comm : ￢a ≤ b ↔ ￢b ≤ a

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ ￢a ≤ b ↔ ￢b ≤ a

Tactic:
rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]

Result:
no goals
-- Mathlib/LinearAlgebra/InvariantBasisNumber.lean
theorem card_le_of_surjective' [RankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Surjective f) : Fintype.card β ≤ Fintype.card α

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
exact
  card_le_of_surjective R ((P.toLinearMap.comp f).comp Q.toLinearMap)
    ((P.surjective.comp i).comp Q.surjective)

Result:
no goals

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
let P := Finsupp.linearEquivFunOnFinite R R β

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card β ≤ Fintype.card α

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card β ≤ Fintype.card α

Tactic:
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card β ≤ Fintype.card α
-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem first_of_chain_isUnit {q : Associates M} {n : ℕ} {c : Fin (n + 1) → Associates M}
    (h₁ : StrictMono c) (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) : IsUnit (c 0)

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ c 0 ≤ c i

Tactic:
exact h₁.monotone (Fin.zero_le i)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
⊢ IsUnit (c 0)

Tactic:
obtain ⟨i, hr⟩ := h₂.mp Associates.one_le

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ IsUnit (c 0)

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ IsUnit (c 0)

Tactic:
rw [Associates.isUnit_iff_eq_one, ← Associates.le_one_iff, hr]

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
q : Associates M
n : ℕ
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
i : Fin (n + 1)
hr : 1 = c i
⊢ c 0 ≤ c i
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma cpow_inv_two_im_eq_neg_sqrt {x : ℂ} (hx : x.im < 0) :
    (x ^ (2⁻¹ : ℂ)).im = -sqrt ((‖x‖ - x.re) / 2)

Proof state:
case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

Tactic:
linarith [pi_pos, neg_pi_lt_arg x]

Result:
no goals

Proof state:
case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0

Tactic:
exact (arg_neg_iff.2 hx).le

Result:
no goals

Proof state:
x : ℂ
hx : x.im < 0
⊢ (x ^ 2⁻¹).im = -√((‖x‖ - x.re) / 2)

Tactic:
rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
  ← Real.sqrt_eq_rpow, sin_half_eq_neg_sqrt, mul_neg, ← sqrt_mul (norm_nonneg _),
  ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]

Result:
case hl
x : ℂ
hx : x.im < 0
⊢ -(2 * π) ≤ x.arg

case hr
x : ℂ
hx : x.im < 0
⊢ x.arg ≤ 0
-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
theorem FiniteMultiplicity.of_not_isUnit [CancelCommMonoidWithZero α] [WfDvdMonoid α]
    {a b : α} (ha : ¬IsUnit a) (hb : b ≠ 0) : FiniteMultiplicity a b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ ¬a ^ (n + 1) ∣ a ^ n * c

Tactic:
rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : WfDvdMonoid α
a b : α
ha : ¬IsUnit a
hb : b ≠ 0
⊢ FiniteMultiplicity a b

Tactic:
obtain ⟨n, c, ndvd, rfl⟩ := WfDvdMonoid.max_power_factor' hb ha

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ FiniteMultiplicity a (a ^ n * c)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
ha : ¬IsUnit a
n : ℕ
c : α
ndvd : ¬a ∣ c
hb : a ^ n * c ≠ 0
⊢ FiniteMultiplicity a (a ^ n * c)

Tactic:
exact ⟨n, by rwa [pow_succ, mul_dvd_mul_iff_left (left_ne_zero_of_mul hb)]⟩

Result:
no goals
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
@[ext]
lemma SecondObj.ext (z₁ z₂ : SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X)
    (hf : S.arrows f), (Pi.π _ ⟨Y, Z, g, f, hf⟩ : SecondObj P S ⟶ _) z₁ =
      (Pi.π _ ⟨Y, Z, g, f, hf⟩ : SecondObj P S ⟶ _) z₂) : z₁ = z₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂
⊢ ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j z₁ =
      limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j z₂

Proof state:
case w.mk.mk.mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) { as := ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ } z₁ =
    limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) { as := ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ } z₂

Tactic:
apply h

Result:
no goals

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂
⊢ ∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })),
    limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j z₁ =
      limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j z₂

Tactic:
rintro ⟨⟨Y, Z, g, f, hf⟩⟩

Result:
case w.mk.mk.mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
z₁ z₂ : SecondObj P S
h :
  ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ =
      Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂
Y Z : C
g : Z ⟶ Y
f : Y ⟶ X
hf : S.arrows f
⊢ limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) { as := ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ } z₁ =
    limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) { as := ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ } z₂
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma symmetry_symmetry [Full F] [Faithful F] : hf'.symmetry hg ≫ hg.symmetry hf' = 𝟙 _ :=
  hom_ext' hf' (by simp) (by simp)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (hf'.symmetry hg ≫ hg.symmetry hf') ≫ hf'.snd g = 𝟙 (hf'.pullback g) ≫ hf'.snd g

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
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ (hf'.symmetry hg ≫ hg.symmetry hf') ≫ hf'.fst' g = 𝟙 (hf'.pullback g) ≫ hf'.fst' g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
lemma translate_prod_right (a : G) (f : ι → G → M) (s : Finset ι) :
    τ a (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i)

Proof state:
case h
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, τ a (f i)) x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
⊢ τ a (∏ i ∈ s, f i) = ∏ i ∈ s, τ a (f i)

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_4
G : Type u_5
inst✝¹ : AddCommGroup G
inst✝ : CommMonoid M
a : G
f : ι → G → M
s : Finset ι
x✝ : G
⊢ τ a (∏ i ∈ s, f i) x✝ = (∏ i ∈ s, τ a (f i)) x✝
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma freeLocus_eq_univ [Module.FinitePresentation R M] [Module.Flat R M] :
    freeLocus R M = Set.univ

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
⊢ ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)

Tactic:
exact fun x ↦ Module.free_of_flat_of_isLocalRing

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
⊢ freeLocus R M = Set.univ

Tactic:
simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
⊢ ∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
-- Mathlib/Topology/Homotopy/Product.lean
theorem projRight_prod : projRight (prod q₁ q₂) = q₂

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ projRight (prod ⟦a✝⟧ ⟦b✝⟧) = ⟦b✝⟧

Tactic:
rw [projRight, prod_lift, ← Path.Homotopic.map_lift]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ ⟦(a✝.prod b✝).map ⋯⟧ = ⟦b✝⟧

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
⊢ projRight (prod q₁ q₂) = q₂

Tactic:
induction q₁, q₂ using Quotient.inductionOn₂

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ projRight (prod ⟦a✝⟧ ⟦b✝⟧) = ⟦b✝⟧

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ : α
b₁ b₂ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ ⟦(a✝.prod b✝).map ⋯⟧ = ⟦b✝⟧

Tactic:
congr

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem Prime.not_dvd_one {p : ℕ+} : p.Prime → ¬p ∣ 1 := fun pp : p.Prime => by
  rw [dvd_iff]
  apply Nat.Prime.not_dvd_one pp

Proof state:
p : ℕ+
pp : p.Prime
⊢ ¬↑p ∣ ↑1

Tactic:
apply Nat.Prime.not_dvd_one pp

Result:
no goals

Proof state:
p : ℕ+
pp : p.Prime
⊢ ¬p ∣ 1

Tactic:
rw [dvd_iff]

Result:
p : ℕ+
pp : p.Prime
⊢ ¬↑p ∣ ↑1
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
    diam (s ∪ t) ≤ diam s + dist x y + diam t

Proof state:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s = ⊤ → EMetric.diam (s ∪ t) = ⊤

Tactic:
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono subset_union_left

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t

Tactic:
simp only [diam, dist_edist]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ (EMetric.diam (s ∪ t)).toReal ≤ (EMetric.diam s).toReal + (edist x y).toReal + (EMetric.diam t).toReal

Proof state:
case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam t = ⊤ → EMetric.diam (s ∪ t) = ⊤

Tactic:
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono subset_union_right

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ (EMetric.diam (s ∪ t)).toReal ≤ (EMetric.diam s).toReal + (edist x y).toReal + (EMetric.diam t).toReal

Tactic:
refine (ENNReal.toReal_le_add' (EMetric.diam_union xs yt) ?_ ?_).trans
  (add_le_add_right ENNReal.toReal_add_le _)

Result:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s + edist x y = ⊤ → EMetric.diam (s ∪ t) = ⊤

case refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam t = ⊤ → EMetric.diam (s ∪ t) = ⊤

Proof state:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s + edist x y = ⊤ → EMetric.diam (s ∪ t) = ⊤

Tactic:
simp only [ENNReal.add_eq_top, edist_ne_top, or_false]

Result:
case refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s = ⊤ → EMetric.diam (s ∪ t) = ⊤
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem EquicontinuousAt.tendsto_of_mem_closure {l : Filter ι} {F : ι → X → α} {f : X → α}
    {s : Set X} {x : X} {z : α} (hF : EquicontinuousAt F x) (hf : Tendsto f (𝓝[s] x) (𝓝 z))
    (hs : ∀ y ∈ s, Tendsto (F · y) l (𝓝 (f y))) (hx : x ∈ closure s) :
    Tendsto (F · x) l (𝓝 z)

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
have : ∀ᶠ y in 𝓝[s] x, y ∈ s ∧ (∀ i, (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V :=
  eventually_mem_nhdsWithin.and <| ((hF V hV).filter_mono nhdsWithin_le_nhds).and (hf V hV)

Result:
case intro.intro.intro
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x => F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem AddSubmonoidClass.IsHomogeneous.mem_iff
    {P : Type*} [SetLike P M] [AddSubmonoidClass P M] (p : P)
    (hp : SetLike.IsHomogeneous ℳ p) {x} :
    x ∈ p ↔ ∀ i, (decompose ℳ x i : M) ∈ p

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
⊢ x ∈ p ↔ ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p

Tactic:
classical
refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩
rw [← DirectSum.sum_support_decompose ℳ x]
exact sum_mem (fun i _ ↦ hx i)

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ x ∈ p

Tactic:
rw [← DirectSum.sum_support_decompose ℳ x]

Result:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) x), ↑(((decompose ℳ) x) i) ∈ p

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ ∑ i ∈ DFinsupp.support ((decompose ℳ) x), ↑(((decompose ℳ) x) i) ∈ p

Tactic:
exact sum_mem (fun i _ ↦ hx i)

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
⊢ x ∈ p ↔ ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p

Tactic:
refine ⟨fun hx i ↦ hp i hx, fun hx ↦ ?_⟩

Result:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid M
inst✝⁴ : SetLike σ M
inst✝³ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝² : Decomposition ℳ
P : Type u_5
inst✝¹ : SetLike P M
inst✝ : AddSubmonoidClass P M
p : P
hp : SetLike.IsHomogeneous ℳ p
x : M
hx : ∀ (i : ι), ↑(((decompose ℳ) x) i) ∈ p
⊢ x ∈ p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_append' (f : α → β → β) (b) (l l' : Array α)
    (w : start = l.size + l'.size) :
    (l ++ l').foldr f b start 0 = l.foldr f (l'.foldr f b)

Proof state:
α : Type u_1
β : Type u_2
start : Nat
f : α → β → β
b : β
l l' : Array α
w : start = l.size + l'.size
⊢ foldr f b (l ++ l') start = foldr f (foldr f b l') l

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l l' : Array α
⊢ foldr f b (l ++ l') (l.size + l'.size) = foldr f (foldr f b l') l

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l l' : Array α
⊢ foldr f b (l ++ l') (l.size + l'.size) = foldr f (foldr f b l') l

Tactic:
simp [foldr_eq_foldrM]

Result:
no goals