harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_div_mul_mul (A B C : Finset G) :
    #(A / C) * #B ≤ #(A * B) * #(C * B)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A * B) * #(C * B)

Tactic:
simpa using ruzsa_triangle_inequality_div_div_div A B⁻¹ C

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem hasBasis_coclosedCompact :
    (Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set X),
    IsClosed i ∧ IsCompact i →
      ∀ (j : Set X), IsClosed j ∧ IsCompact j → ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ

Tactic:
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs₁ : IsClosed s
hs₂ : IsCompact s
t : Set X
ht₁ : IsClosed t
ht₂ : IsCompact t
⊢ ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ (coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl

Tactic:
simp only [Filter.coclosedCompact, iInf_and']

Result:
X : Type u
inst✝ : TopologicalSpace X
⊢ (⨅ s, ⨅ (_ : IsClosed s ∧ IsCompact s), 𝓟 sᶜ).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs₁ : IsClosed s
hs₂ : IsCompact s
t : Set X
ht₁ : IsClosed t
ht₂ : IsCompact t
⊢ ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Tactic:
exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
  compl_subset_compl.2 subset_union_right⟩⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ (⨅ s, ⨅ (_ : IsClosed s ∧ IsCompact s), 𝓟 sᶜ).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl

Tactic:
refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩

Result:
X : Type u
inst✝ : TopologicalSpace X
⊢ ∀ (i : Set X),
    IsClosed i ∧ IsCompact i →
      ∀ (j : Set X), IsClosed j ∧ IsCompact j → ∃ k, (IsClosed k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem isCoprime_one_right : IsCoprime x 1 :=
  ⟨0, 1, by rw [one_mul, zero_mul, zero_add]⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
⊢ 0 * x + 1 * 1 = 1

Tactic:
rw [one_mul, zero_mul, zero_add]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma ringHomComp_inv {R : Type*} [CommRing R] (χ : MulChar R R') (f : R' →+* R'') :
    (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f

Proof state:
R' : Type u_2
inst✝² : CommRing R'
R'' : Type u_3
inst✝¹ : CommRing R''
R : Type u_4
inst✝ : CommRing R
χ : MulChar R R'
f : R' →+* R''
⊢ (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f

Tactic:
ext1

Result:
case h
R' : Type u_2
inst✝² : CommRing R'
R'' : Type u_3
inst✝¹ : CommRing R''
R : Type u_4
inst✝ : CommRing R
χ : MulChar R R'
f : R' →+* R''
a✝ : Rˣ
⊢ (χ.ringHomComp f)⁻¹ ↑a✝ = (χ⁻¹.ringHomComp f) ↑a✝

Proof state:
case h
R' : Type u_2
inst✝² : CommRing R'
R'' : Type u_3
inst✝¹ : CommRing R''
R : Type u_4
inst✝ : CommRing R
χ : MulChar R R'
f : R' →+* R''
a✝ : Rˣ
⊢ (χ.ringHomComp f)⁻¹ ↑a✝ = (χ⁻¹.ringHomComp f) ↑a✝

Tactic:
simp only [inv_apply, Ring.inverse_unit, ringHomComp_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem ker_prodMap (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄) :
    ker (LinearMap.prodMap f g) = Submodule.prod (ker f) (ker g)

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
⊢ ker (f.prodMap g) = (ker f).prod (ker g)

Tactic:
dsimp only [ker]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
M₄ : Type z
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
⊢ Submodule.comap (f.prodMap g) ⊥ = (Submodule.comap f ⊥).prod (Submodule.comap g ⊥)

Tactic:
rw [← prodMap_comap_prod, Submodule.prod_bot]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Defs.lean
theorem fg_iff_addSubmonoid_fg (P : Submodule ℕ M) : P.FG ↔ P.toAddSubmonoid.FG :=
  ⟨fun ⟨S, hS⟩ => ⟨S, by simpa [← span_nat_eq_addSubmonoid_closure] using hS⟩, fun ⟨S, hS⟩ =>
    ⟨S, by simpa [← span_nat_eq_addSubmonoid_closure] using hS⟩⟩

Proof state:
M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : AddSubmonoid.closure ↑S = P.toAddSubmonoid
⊢ span ℕ ↑S = P

Tactic:
simpa [← span_nat_eq_addSubmonoid_closure] using hS

Result:
no goals

Proof state:
M : Type u_2
inst✝ : AddCommMonoid M
P : Submodule ℕ M
x✝ : P.FG
S : Finset M
hS : span ℕ ↑S = P
⊢ AddSubmonoid.closure ↑S = P.toAddSubmonoid

Tactic:
simpa [← span_nat_eq_addSubmonoid_closure] using hS

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_fintypeIco : Fintype.card (Set.Ico a b) = b - a

Proof state:
a b : ℕ
⊢ Fintype.card ↑(Set.Ico a b) = b - a

Tactic:
rw [Fintype.card_ofFinset, card_Ico]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sub_le_of_le_add {a b c : EReal} (h : a ≤ b + c) : a - c ≤ b

Proof state:
case h_real
a b : EReal
c : ℝ
h : a ≤ b + ↑c
⊢ a - ↑c ≤ b

Tactic:
exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h

Result:
no goals

Proof state:
case h_top
a b : EReal
h : a ≤ b + ⊤
⊢ a - ⊤ ≤ b

Tactic:
simp only [sub_top, bot_le]

Result:
no goals

Proof state:
case h_bot
a b : EReal
h : a = ⊥
⊢ a - ⊥ ≤ b

Tactic:
simp only [h, bot_sub, bot_le]

Result:
no goals

Proof state:
a b c : EReal
h : a ≤ b + c
⊢ a - c ≤ b

Tactic:
induction c with
| h_bot => rw [add_bot, le_bot_iff] at h; simp only [h, bot_sub, bot_le]
| h_real c => exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h
| h_top => simp only [sub_top, bot_le]

Result:
no goals

Proof state:
case h_bot
a b : EReal
h : a ≤ b + ⊥
⊢ a - ⊥ ≤ b

Tactic:
rw [add_bot, le_bot_iff] at h

Result:
case h_bot
a b : EReal
h : a = ⊥
⊢ a - ⊥ ≤ b
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma single₀_map_f_zero {A B : V} (f : A ⟶ B) :
    ((single₀ V).map f).f 0 = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f

Tactic:
rw [comp_id, id_comp]

Result:
no goals

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A).hom ≫
      f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B).inv =
    f

Tactic:
dsimp [HomologicalComplex.singleObjXSelf, HomologicalComplex.singleObjXIsoOfEq]

Result:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ ((single₀ V).map f).f 0 = f

Tactic:
rw [HomologicalComplex.single_map_f_self]

Result:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 A).hom ≫
      f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 0 B).inv =
    f
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem prod_top : (prod ⊤ ⊤ : NonUnitalStarSubalgebra R (A × B)) = ⊤

Proof state:
R : Type u
A : Type v
B : Type w
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalSemiring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Module R A
inst✝⁹ : NonUnitalSemiring B
inst✝⁸ : StarRing B
inst✝⁷ : Module R B
inst✝⁶ : StarRing R
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalSemiring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Module R A
inst✝⁹ : NonUnitalSemiring B
inst✝⁸ : StarRing B
inst✝⁷ : Module R B
inst✝⁶ : StarRing R
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝¹³ : CommSemiring R
inst✝¹² : NonUnitalSemiring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Module R A
inst✝⁹ : NonUnitalSemiring B
inst✝⁸ : StarRing B
inst✝⁷ : Module R B
inst✝⁶ : StarRing R
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : SMulCommClass R A A
inst✝³ : StarModule R A
inst✝² : IsScalarTower R B B
inst✝¹ : SMulCommClass R B B
inst✝ : StarModule R B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
@[simp]
lemma tendsto_image_smallSets {f : α → β} :
    Tendsto (f '' ·) la.smallSets lb.smallSets ↔ Tendsto f la lb

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb

Tactic:
refine forall₂_congr fun u hu ↦ ?_

Result:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun x => f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
rw [tendsto_smallSets_iff]

Result:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la

Tactic:
simp only [image_subset_iff, exists_mem_subset_iff, mem_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ u) ↔ u ∈ map f la

Tactic:
rw [eventually_smallSets' fun s t hst ht ↦ (image_subset _ hst).trans ht]

Result:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
u : Set β
hu : u ∈ lb
⊢ (∃ s ∈ la, f '' s ⊆ u) ↔ u ∈ map f la
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDerivWithin_clm_apply_const_apply
    {s : Set E} (hs : UniqueDiffOn 𝕜 s) {c : E → F →L[𝕜] G}
    (hc : ContDiffOn 𝕜 n c s) {i : ℕ} (hi : i ≤ n) {x : E} (hx : x ∈ s) {u : F} {m : Fin i → E} :
    (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = (iteratedFDerivWithin 𝕜 i c s x) m u

Proof state:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (((iteratedFDerivWithin 𝕜 i c s x) (tail m)).comp (fderivWithin 𝕜 (fun x => u) s x) +
        (fderivWithin 𝕜 (fun y => (iteratedFDerivWithin 𝕜 i c s y) (tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (tail m)) u

Tactic:
rw [fderivWithin_const_apply]

Result:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (((iteratedFDerivWithin 𝕜 i c s x) (tail m)).comp 0 +
        (fderivWithin 𝕜 (fun y => (iteratedFDerivWithin 𝕜 i c s y) (tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (tail m)) u
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem normUnit_X : normUnit (X : Polynomial R) = 1

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
⊢ normUnit X = 1

Tactic:
have := coe_normUnit (R := R) (p := X)

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
this : ↑(normUnit X) = C ↑(normUnit X.leadingCoeff)
⊢ normUnit X = 1

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
this : ↑(normUnit X) = C ↑(normUnit X.leadingCoeff)
⊢ normUnit X = 1

Tactic:
rwa [leadingCoeff_X, normUnit_one, Units.val_one, map_one, Units.val_eq_one] at this

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem nat_find_mem_find {p : Fin n → Prop} [DecidablePred p]
    (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
    (⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p

Proof state:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ p ⟨↑f, ⋯⟩

Tactic:
convert find_spec p hf

Result:
no goals

Proof state:
case none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
hf : ∀ (i : Fin n), ¬p i
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ none

Tactic:
exact (hf ⟨i, hin⟩ hi).elim

Result:
no goals

Proof state:
case some
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ some f

Tactic:
refine Option.some_inj.2 (Fin.le_antisymm ?_ ?_)

Result:
case some.refine_1
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ f ≤ ⟨Nat.find ⋯, ⋯⟩

case some.refine_2
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ ⟨Nat.find ⋯, ⋯⟩ ≤ f

Proof state:
case some.refine_1
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ f ≤ ⟨Nat.find ⋯, ⋯⟩

Tactic:
exact find_min' hf (Nat.find_spec h).snd

Result:
no goals

Proof state:
case none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
hf : find p = none
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ none

Tactic:
rw [find_eq_none_iff] at hf

Result:
case none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
hf : ∀ (i : Fin n), ¬p i
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ none

Proof state:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ find p

Tactic:
rcases hf : find p with - | f

Result:
case none
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
hf : find p = none
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ none

case some
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ some f

Proof state:
case some.refine_2
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
f : Fin n
hf : find p = some f
⊢ ⟨Nat.find ⋯, ⋯⟩ ≤ f

Tactic:
exact Nat.find_min' _ ⟨f.2, by convert find_spec p hf⟩

Result:
no goals

Proof state:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
⊢ ⟨Nat.find h, ⋯⟩ ∈ find p

Tactic:
let ⟨i, hin, hi⟩ := h

Result:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i, ∃ (hin : i < n), p ⟨i, hin⟩
i : ℕ
hin : i < n
hi : p ⟨i, hin⟩
⊢ ⟨Nat.find ⋯, ⋯⟩ ∈ find p
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem polar_pi (Q : ∀ i, QuadraticMap R (Mᵢ i) P) (x y : ∀ i, Mᵢ i) :
    polar (pi Q) x y = ∑ i, polar (Q i) (x i) (y i)

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ (pi Q) (x + y) - (pi Q) x - (pi Q) y = ∑ i : ι, ((Q i) (x i + y i) - (Q i) (x i) - (Q i) (y i))

Tactic:
simp_rw [Finset.sum_sub_distrib, pi_apply, Pi.add_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ polar (⇑(pi Q)) x y = ∑ i : ι, polar (⇑(Q i)) (x i) (y i)

Tactic:
dsimp [polar]

Result:
ι : Type u_1
R : Type u_2
P : Type u_7
Mᵢ : ι → Type u_8
inst✝⁵ : CommRing R
inst✝⁴ : (i : ι) → AddCommGroup (Mᵢ i)
inst✝³ : AddCommGroup P
inst✝² : (i : ι) → Module R (Mᵢ i)
inst✝¹ : Module R P
inst✝ : Fintype ι
Q : (i : ι) → QuadraticMap R (Mᵢ i) P
x y : (i : ι) → Mᵢ i
⊢ (pi Q) (x + y) - (pi Q) x - (pi Q) y = ∑ i : ι, ((Q i) (x i + y i) - (Q i) (x i) - (Q i) (y i))
-- Mathlib/Data/Sum/Basic.lean
theorem isLeft_left (h : LiftRel r s x (inl c)) : x.isLeft

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (inl c)
⊢ x.isLeft = true

Tactic:
cases h

Result:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
c : γ
a✝¹ : α
a✝ : r a✝¹ c
⊢ (inl a✝¹).isLeft = true

Proof state:
case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
c : γ
a✝¹ : α
a✝ : r a✝¹ c
⊢ (inl a✝¹).isLeft = true

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_div_dvd (p : K[X]) {q : K[X]} (hq : q ≠ 0) :
    num (algebraMap _ _ p / algebraMap _ _ q) ∣ p

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0

Tactic:
simpa only [Ne, inv_eq_zero, Polynomial.leadingCoeff_eq_zero] using right_div_gcd_ne_zero hq

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ p / gcd p q ∣ p

Tactic:
exact EuclideanDomain.div_dvd_of_dvd (gcd_dvd_left p q)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num ∣ p

Tactic:
rw [num_div _ q, C_mul_dvd]

Result:
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ p / gcd p q ∣ p

K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ (q / gcd p q).leadingCoeff⁻¹ ≠ 0
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_pos (hx : 1 < x) : 0 < logb b x

Proof state:
b x : ℝ
hb : 1 < b
hx : 1 < x
⊢ 0 < logb b x

Tactic:
rw [logb_pos_iff hb (lt_trans zero_lt_one hx)]

Result:
b x : ℝ
hb : 1 < b
hx : 1 < x
⊢ 1 < x

Proof state:
b x : ℝ
hb : 1 < b
hx : 1 < x
⊢ 1 < x

Tactic:
exact hx

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem minSqFac_le_of_dvd {n d : ℕ} (h : n.minSqFac = some d) {m} (m2 : 2 ≤ m) (md : m * m ∣ n) :
    d ≤ m

Proof state:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
⊢ d ≤ m

Tactic:
have := minSqFac_has_prop n

Result:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ d ≤ m

Proof state:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
fd : m.minFac ∣ m
⊢ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ d ≤ m

Tactic:
rw [h] at this

Result:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ d ≤ m

Proof state:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ d ≤ m

Tactic:
have fd := minFac_dvd m

Result:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
fd : m.minFac ∣ m
⊢ d ≤ m

Proof state:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
fd : m.minFac ∣ m
⊢ d ≤ m

Tactic:
exact
  le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
    (minFac_le <| lt_of_lt_of_le (by decide) m2)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem degree_pos_iff_exists_adj : 0 < G.degree v ↔ ∃ w, G.Adj v w

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ 0 < G.degree v ↔ ∃ w, G.Adj v w

Tactic:
simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_pos_iff_of_pos_right [MulPosStrictMono α] [MulPosReflectLT α] (h : 0 < b) :
    0 < a * b ↔ 0 < a

Proof state:
α : Type u_3
a b : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : MulPosStrictMono α
inst✝ : MulPosReflectLT α
h : 0 < b
⊢ 0 < a * b ↔ 0 < a

Tactic:
simpa using mul_lt_mul_right (b := 0) h

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c₆_of_char_three : W.c₆ = -W.b₂ ^ 3

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ -W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆ = -W.b₂ ^ 3

Tactic:
linear_combination (12 * W.b₂ * W.b₄ - 72 * W.b₆) * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.c₆ = -W.b₂ ^ 3

Tactic:
rw [c₆]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ -W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆ = -W.b₂ ^ 3