harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem le_cof_iff_lsub {o : Ordinal} {a : Cardinal} :
    a ≤ cof o ↔ ∀ {ι} (f : ι → Ordinal), lsub.{u, u} f = o → a ≤ #ι

Proof state:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ b

Tactic:
rw [← hb]

Result:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι

Proof state:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
exact
  (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
    ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ => by
      rw [← hb]
      exact H _ hf⟩

Result:
no goals

Proof state:
o : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
b : Cardinal.{u}
x✝ : b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = o
hb : #ι = b
⊢ a ≤ #ι

Tactic:
exact H _ hf

Result:
no goals

Proof state:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
rw [cof_eq_sInf_lsub]

Result:
o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ sInf {a | ∃ ι f, lsub f = o ∧ #ι = a} ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_eq_emod {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : tmod a b = a % b

Proof state:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a.tmod b = a % b

Tactic:
simp [emod_def, tmod_def, tdiv_eq_ediv ha hb]

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem lipschitz (hf : ApproximatesLinearOn f f' s c) :
    LipschitzWith (‖f'‖₊ + c) (s.restrict f)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f f' s c
⊢ LipschitzWith (‖f'‖₊ + c) (s.restrict f)

Tactic:
simpa only [restrict_apply, add_sub_cancel] using
  (f'.lipschitz.restrict s).add hf.lipschitz_sub

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem covBy_iff_add_one_eq [Add α] [One α] [SuccAddOrder α] [NoMaxOrder α] :
    x ⋖ y ↔ x + 1 = y

Proof state:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ x + 1 = y

Tactic:
rw [← succ_eq_add_one]

Result:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ succ x = y

Proof state:
α : Type u_1
x y : α
inst✝⁴ : PartialOrder α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x ⋖ y ↔ succ x = y

Tactic:
exact succ_eq_iff_covBy.symm

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma inter_mem (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : s ∩ t ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s \ (s \ t) ∈ C

Tactic:
exact hC.diff_mem hs (hC.diff_mem hs ht)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s ∩ t ∈ C

Tactic:
rw [← diff_diff_right_self]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ s \ (s \ t) ∈ C
-- Mathlib/Order/Filter/Prod.lean
theorem top_prod : (⊤ : Filter α) ×ˢ g = g.comap Prod.snd

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
⊢ ⊤ ×ˢ g = comap Prod.snd g

Tactic:
rw [prod_eq_inf, comap_top, top_inf_eq]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem closure_isSquare : closure {x : T | IsSquare x} = sumSq T

Proof state:
T : Type u_2
inst✝ : CommSemiring T
⊢ (closure {x | IsSquare x}).toNonUnitalSubsemiring = (sumSq T).toNonUnitalSubsemiring

Tactic:
simp [← Submonoid.square_subsemiringClosure]

Result:
no goals

Proof state:
T : Type u_2
inst✝ : CommSemiring T
⊢ closure {x | IsSquare x} = sumSq T

Tactic:
apply_fun toNonUnitalSubsemiring using toNonUnitalSubsemiring_injective

Result:
T : Type u_2
inst✝ : CommSemiring T
⊢ (closure {x | IsSquare x}).toNonUnitalSubsemiring = (sumSq T).toNonUnitalSubsemiring
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_mem (I : Ideal S) : ↑(Ideal.absNorm I) ∈ I

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
⊢ ↑(absNorm I) ∈ I

Tactic:
rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
  Quotient.index_eq_zero]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem add_modEq_right : a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p]

Tactic:
simp [← modEq_sub_iff_add_modEq]

Result:
no goals
-- Mathlib/Algebra/Small/Group.lean
@[to_additive (attr := simp)]
lemma equivShrink_inv [Inv α] [Small α] (x : α) :
    equivShrink α x⁻¹ = (equivShrink α x)⁻¹

Proof state:
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ (equivShrink α) x⁻¹ = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x))⁻¹

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ (equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹

Tactic:
rw [Equiv.inv_def]

Result:
α : Type u_1
inst✝¹ : Inv α
inst✝ : Small.{u_2, u_1} α
x : α
⊢ (equivShrink α) x⁻¹ = (equivShrink α).symm.symm ((equivShrink α).symm ((equivShrink α) x))⁻¹
-- Mathlib/Data/Multiset/Filter.lean
lemma filter_comm (q) [DecidablePred q] (s : Multiset α) :
    filter p (filter q s) = filter q (filter p s)

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ filter p (filter q s) = filter q (filter p s)

Tactic:
simp [and_comm]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_cases {i} (p : π i → Prop) (hf : p (f i)) (hg : p (g i)) :
    p (s.piecewise f g i)

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
⊢ p (s.piecewise f g i)

Tactic:
by_cases hi : i ∈ s <;> simpa [hi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_or_eq_true_self : ∀(b : Bool), (b = false ∨ b = true) ↔ True

Proof state:
⊢ ∀ (b : Bool), b = false ∨ b = true ↔ True

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_sdiff [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) (b : P) :
    (s \ s₂).weightedVSubOfPoint p b w + s₂.weightedVSubOfPoint p b w =
      s.weightedVSubOfPoint p b w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
b : P
⊢ ((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w

Tactic:
simp_rw [weightedVSubOfPoint_apply, sum_sdiff h]

Result:
no goals
-- Mathlib/Analysis/Convex/Extreme.lean
theorem isExtreme_biInter {F : Set (Set E)} (hF : F.Nonempty) (hA : ∀ B ∈ F, IsExtreme 𝕜 A B) :
    IsExtreme 𝕜 A (⋂ B ∈ F, B)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hA : ∀ B ∈ F, IsExtreme 𝕜 A B
this : Nonempty ↑F
⊢ IsExtreme 𝕜 A (⋂ B ∈ F, B)

Tactic:
simpa only [iInter_subtype] using isExtreme_iInter fun i : F ↦ hA _ i.2

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hA : ∀ B ∈ F, IsExtreme 𝕜 A B
⊢ IsExtreme 𝕜 A (⋂ B ∈ F, B)

Tactic:
haveI := hF.to_subtype

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
A : Set E
F : Set (Set E)
hF : F.Nonempty
hA : ∀ B ∈ F, IsExtreme 𝕜 A B
this : Nonempty ↑F
⊢ IsExtreme 𝕜 A (⋂ B ∈ F, B)
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
theorem extChartAt_transDiffeomorph_target (x : M) :
    (extChartAt (I.transDiffeomorph e) x).target = e.symm ⁻¹' (extChartAt I x).target

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H : Type u_5
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
e : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
inst✝ : NeZero n
x : M
⊢ (extChartAt (I.transDiffeomorph e) x).target = ⇑e.symm ⁻¹' (extChartAt I x).target

Tactic:
simp only [e.range_comp, preimage_preimage, mfld_simps]

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H : Type u_5
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
e : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
inst✝ : NeZero n
x : M
⊢ ⇑e.symm ⁻¹' range ↑I ∩ ↑I.symm ∘ ⇑e.symm ⁻¹' (chartAt H x).target =
    ⇑e.symm ⁻¹' range ↑I ∩ (fun x => ↑I.symm (e.symm x)) ⁻¹' (chartAt H x).target

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E' : Type u_3
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H : Type u_5
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
e : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
inst✝ : NeZero n
x : M
⊢ ⇑e.symm ⁻¹' range ↑I ∩ ↑I.symm ∘ ⇑e.symm ⁻¹' (chartAt H x).target =
    ⇑e.symm ⁻¹' range ↑I ∩ (fun x => ↑I.symm (e.symm x)) ⁻¹' (chartAt H x).target

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingularLift_negMap {P : PointClass F} (hP : W.NonsingularLift P) :
    W.NonsingularLift <| W.negMap P

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : PointClass F
hP : W.NonsingularLift P
⊢ W.NonsingularLift (W.negMap P)

Tactic:
rcases P with ⟨_⟩

Result:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Proof state:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Tactic:
exact nonsingular_neg hP

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem dExt_iff {f g : E →ₗ.[R] F} :
    f = g ↔
      ∃ _domain_eq : f.domain = g.domain,
        ∀ ⦃x : f.domain⦄ ⦃y : g.domain⦄ (_h : (x : E) = y), f x = g y :=
  ⟨fun EQ =>
    EQ ▸
      ⟨rfl, fun x y h => by
        congr
        exact mod_cast h⟩,
    fun ⟨deq, feq⟩ => dExt deq feq⟩

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ ↑f x = ↑f y

Tactic:
congr

Result:
case e_a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ x = y

Proof state:
case e_a
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
EQ : f = g
x y : ↥f.domain
h : ↑x = ↑y
⊢ x = y

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/Topology/GDelta/Basic.lean
/-- A countable union of meagre sets is meagre. -/
lemma isMeagre_iUnion {s : ℕ → Set X} (hs : ∀ n, IsMeagre (s n)) : IsMeagre (⋃ n, s n)

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : ℕ → Set X
hs : ∀ (n : ℕ), IsMeagre (s n)
⊢ IsMeagre (⋃ n, s n)

Tactic:
rw [IsMeagre, compl_iUnion]

Result:
X : Type u_5
inst✝ : TopologicalSpace X
s : ℕ → Set X
hs : ∀ (n : ℕ), IsMeagre (s n)
⊢ ⋂ i, (s i)ᶜ ∈ residual X

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : ℕ → Set X
hs : ∀ (n : ℕ), IsMeagre (s n)
⊢ ⋂ i, (s i)ᶜ ∈ residual X

Tactic:
exact countable_iInter_mem.mpr hs

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioc_sub_one_sub_one_eq_Ico (a b : α) : Ioc (a - 1) (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico a b

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_subset_iff {x y : ZFSet} : x.toSet ⊆ y.toSet ↔ x ⊆ y

Proof state:
x y : ZFSet.{u_1}
⊢ x.toSet ⊆ y.toSet ↔ x ⊆ y

Tactic:
simp [subset_def, Set.subset_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem aeval_sumIDeriv_eq_eval (p : R[X]) (r : A) :
    aeval r (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p))

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ (aeval r) (sumIDeriv p) = eval r (sumIDeriv (map (algebraMap R A) p))

Tactic:
rw [aeval_def, eval, sumIDeriv_map, eval₂_map, RingHom.id_comp]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem isComplete_iff_ultrafilter' {s : Set α} :
    IsComplete s ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x :=
  isComplete_iff_ultrafilter.trans <| by simp only [le_principal_iff, Ultrafilter.mem_coe]

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ (∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x) ↔
    ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x

Tactic:
simp only [le_principal_iff, Ultrafilter.mem_coe]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_num_den (h : normalize n d z = ⟨n', d', z', c⟩) :
    ∃ m : Nat, m ≠ 0 ∧ n = n' * m ∧ d = d' * m

Proof state:
n : Int
d : Nat
z : d ≠ 0
n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
h : normalize n d z = { num := n', den := d', den_nz := z', reduced := c }
⊢ ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

Tactic:
have := normalize_num_den' n d z

Result:
n : Int
d : Nat
z : d ≠ 0
n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
h : normalize n d z = { num := n', den := d', den_nz := z', reduced := c }
this : ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d z).num * ↑d_1 ∧ d = (normalize n d z).den * d_1
⊢ ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

Proof state:
n : Int
d : Nat
z : d ≠ 0
n' : Int
d' : Nat
z' : d' ≠ 0
c : n'.natAbs.Coprime d'
h : normalize n d z = { num := n', den := d', den_nz := z', reduced := c }
this : ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d z).num * ↑d_1 ∧ d = (normalize n d z).den * d_1
⊢ ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

Tactic:
rwa [h] at this

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_X [DecidableEq σ] (i j : σ) :
    pderiv i (X j : MvPolynomial σ R) = Pi.single (f := fun _ => _) i 1 j

Proof state:
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
⊢ (pderiv i) (X j) = Pi.single i 1 j

Tactic:
rw [pderiv_def, mkDerivation_X]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesSummable.add {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s)
    (hg : LSeriesSummable g s) :
    LSeriesSummable (f + g) s

Proof state:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f + g) s

Tactic:
simpa [LSeriesSummable, ← term_add_apply] using Summable.add hf hg

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem cofan_inj_comp_PInfty_eq_zero {X : SimplicialObject C} (s : SimplicialObject.Splitting X)
    {n : ℕ} (A : SimplicialObject.Splitting.IndexSet (op ⦋n⦌)) (hA : ¬A.EqId) :
    (s.cofan _).inj A ≫ PInfty.f n = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : Splitting X
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ PInfty.f n = 0

Tactic:
rw [SimplicialObject.Splitting.cofan_inj_eq, assoc, degeneracy_comp_PInfty X n A.e hA, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : Splitting X
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬A.EqId
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ PInfty.f n = 0

Tactic:
rw [SimplicialObject.Splitting.IndexSet.eqId_iff_mono] at hA

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
s : Splitting X
n : ℕ
A : IndexSet (op ⦋n⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋n⦌)).inj A ≫ PInfty.f n = 0
-- Mathlib/Computability/Reduce.lean
theorem disjoin_manyOneReducible {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ]
    {p : α → Prop} {q : β → Prop} {r : γ → Prop} : p ≤₀ r → q ≤₀ r → (p ⊕' q) ≤₀ r
  | ⟨f, c₁, h₁⟩, ⟨g, c₂, h₂⟩ =>
    ⟨Sum.elim f g,
      Computable.id.sumCasesOn (c₁.comp Computable.snd).to₂ (c₂.comp Computable.snd).to₂,
      fun x => by cases x <;> [apply h₁; apply h₂]⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
p : α → Prop
q : β → Prop
r : γ → Prop
f : α → γ
c₁ : Computable f
h₁ : ∀ (a : α), p a ↔ r (f a)
g : β → γ
c₂ : Computable g
h₂ : ∀ (a : β), q a ↔ r (g a)
x : α ⊕ β
⊢ (p ⊕' q) x ↔ r ((f ⊕' g) x)

Tactic:
cases x <;> [apply h₁; apply h₂]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) : normalize z = z

Proof state:
z : ℤ
h : 0 ≤ z
⊢ normalize z = z

Tactic:
rw [normalize_apply, normUnit_eq, if_pos h, Units.val_one, mul_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_le_of_trailingDegree_le {n : ℕ} {hp : p ≠ 0}
    (H : (n : ℕ∞) ≤ trailingDegree p) : n ≤ natTrailingDegree p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : ↑n ≤ p.trailingDegree
⊢ n ≤ p.natTrailingDegree

Tactic:
rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
lemma exp_abs_le (x : ℝ) : exp |x| ≤ exp x + exp (-x)

Proof state:
x : ℝ
⊢ rexp |x| ≤ rexp x + rexp (-x)

Tactic:
cases le_total x 0 <;> simp [abs_of_nonpos, abs_of_nonneg, exp_nonneg, *]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem one_le_count_iff_mem {a : α} {s : Multiset α} : 1 ≤ count a s ↔ a ∈ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ 1 ≤ count a s ↔ a ∈ s

Tactic:
rw [succ_le_iff, count_pos]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `a ≠ 0`. See `inv_mul_cancel_left`. -/
lemma le_inv_mul_left (hb : b ≤ 0) : b ≤ a⁻¹ * (a * b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
hb : b ≤ 0
⊢ b ≤ a⁻¹ * (a * b)

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Ring/Regular.lean
theorem isLeftRegular_of_non_zero_divisor [NonUnitalNonAssocRing α] (k : α)
    (h : ∀ x : α, k * x = 0 → x = 0) : IsLeftRegular k

Proof state:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * (x - y) = 0

Tactic:
rw [mul_sub, sub_eq_zero, h']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
⊢ IsLeftRegular k

Tactic:
refine fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ ?_)

Result:
α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * (x - y) = 0
-- Mathlib/Algebra/Order/Ring/Canonical.lean
lemma mul_tsub_one [AddLeftReflectLE α] (a b : α) :
    a * (b - 1) = a * b - a

Proof state:
α : Type u
inst✝⁶ : NonAssocSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : CanonicallyOrderedAdd α
inst✝³ : Sub α
inst✝² : OrderedSub α
inst✝¹ : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝ : AddLeftReflectLE α
a b : α
⊢ a * (b - 1) = a * b - a

Tactic:
rw [mul_tsub, mul_one]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem Prime.divisors {p : ℕ} (pp : p.Prime) : divisors p = {1, p}

Proof state:
case h
p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ ∈ p.divisors ↔ a✝ ∈ {1, p}

Tactic:
rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]

Result:
no goals

Proof state:
p : ℕ
pp : Prime p
⊢ p.divisors = {1, p}

Tactic:
ext

Result:
case h
p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ ∈ p.divisors ↔ a✝ ∈ {1, p}
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem coe_support_append' [DecidableEq V] {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    ((p.append p').support : Multiset V) = p.support + p'.support - {v}

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + (↑p'.support.tail + {v}) - {v}

Tactic:
simp only [← add_assoc, add_tsub_cancel_right]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑p.support + ↑p'.support.tail = ↑p.support + ↑p'.support - {v}

Tactic:
simp only [coe_support]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + ({v} + ↑p'.support.tail) - {v}

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + ({v} + ↑p'.support.tail) - {v}

Tactic:
rw [add_comm ({v} : Multiset V)]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ {u} + ↑p.support.tail + ↑p'.support.tail = {u} + ↑p.support.tail + (↑p'.support.tail + {v}) - {v}

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑(p.append p').support = ↑p.support + ↑p'.support - {v}

Tactic:
rw [support_append, ← Multiset.coe_add]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑p.support + ↑p'.support.tail = ↑p.support + ↑p'.support - {v}
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem measure_preimage_mul (μ : Measure G) [IsMulLeftInvariant μ] (g : G) (A : Set G) :
    μ ((fun h => g * h) ⁻¹' A) = μ A :=
  calc
    μ ((fun h => g * h) ⁻¹' A) = map (fun h => g * h) μ A :=
      ((MeasurableEquiv.mulLeft g).map_apply A).symm
    _ = μ A

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulLeftInvariant
g : G
A : Set G
⊢ (Measure.map (fun h => g * h) μ) A = μ A

Tactic:
rw [map_mul_left_eq_self μ g]

Result:
no goals