harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma edist_eq_top_of_not_reachable (h : ¬G.Reachable u v) :
    G.edist u v = ⊤

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : ¬G.Reachable u v
⊢ G.edist u v = ⊤

Tactic:
simp [edist, not_reachable_iff_isEmpty_walk.mp h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_eq_getValueCastD [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    {fallback : β a} (h : containsKey a l = true) :
    getValueCast a l h = getValueCastD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
fallback : β a
h : containsKey a l = true
⊢ getValueCast a l h = getValueCastD a l fallback

Tactic:
rw [getValueCastD_eq_getValueCast?, getValueCast, Option.get_eq_getD]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_bot : reflection (⊥ : Submodule 𝕜 E) = LinearIsometryEquiv.neg 𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ reflection ⊥ = LinearIsometryEquiv.neg 𝕜

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x✝ : E
⊢ (reflection ⊥) x✝ = (LinearIsometryEquiv.neg 𝕜) x✝

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x✝ : E
⊢ (reflection ⊥) x✝ = (LinearIsometryEquiv.neg 𝕜) x✝

Tactic:
simp [reflection_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem univ_mem_measurableCylinders (α : ι → Type*) [∀ i, MeasurableSpace (α i)] :
    Set.univ ∈ measurableCylinders α

Proof state:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ univ ∈ measurableCylinders α

Tactic:
rw [← compl_empty]

Result:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∅ᶜ ∈ measurableCylinders α

Proof state:
ι : Type u_2
α : ι → Type u_1
inst✝ : (i : ι) → MeasurableSpace (α i)
⊢ ∅ᶜ ∈ measurableCylinders α

Tactic:
exact compl_mem_measurableCylinders (empty_mem_measurableCylinders α)

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
theorem card_Ioc_finset (h : s ⊆ t) : (Ioc s t).card = 2 ^ (t.card - s.card) - 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Ioc s t) = 2 ^ (#t - #s) - 1

Tactic:
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc_finset h]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem mapShortComplexH1_zero :
    mapShortComplexH1 (A := A) (B := B) f 0 = 0

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
⊢ mapShortComplexH1 f 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a ≠ b
l : List α
⊢ (count a l + if (b == a) = true then 1 else 0) = count a l

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a ≠ b
l : List α
⊢ count a (b :: l) = count a l

Tactic:
simp only [count_cons, cond_eq_if, beq_iff_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a ≠ b
l : List α
⊢ (count a l + if (b == a) = true then 1 else 0) = count a l
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem Monic.isUnit_leadingCoeff_of_dvd {a p : R[X]} (hp : Monic p) (hap : a ∣ p) :
    IsUnit a.leadingCoeff :=
  isUnit_of_dvd_one (by simpa only [hp.leadingCoeff] using leadingCoeff_dvd_leadingCoeff hap)

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a p : R[X]
hp : p.Monic
hap : a ∣ p
⊢ a.leadingCoeff ∣ 1

Tactic:
simpa only [hp.leadingCoeff] using leadingCoeff_dvd_leadingCoeff hap

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_congr_set (hst : s =ᵐ[μ] t) : ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
hst : s =ᶠ[ae μ] t
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ

Tactic:
rw [Measure.restrict_congr_set hst]

Result:
no goals
-- Mathlib/GroupTheory/PresentedGroup.lean
theorem toGroup.unique (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) (g : PresentedGroup rels →* G)
    (hg : ∀ x : α, g (PresentedGroup.of x) = f x) : ∀ {x}, g x = toGroup h x

Proof state:
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ g x = (toGroup h) x

Tactic:
refine QuotientGroup.induction_on x ?_

Result:
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ ∀ (z : FreeGroup α), g ↑z = (toGroup h) ↑z

Proof state:
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), g (PresentedGroup.of x) = f x
⊢ ∀ {x : PresentedGroup rels}, g x = (toGroup h) x

Tactic:
intro x

Result:
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ g x = (toGroup h) x

Proof state:
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ ∀ (z : FreeGroup α), g ↑z = (toGroup h) ↑z

Tactic:
exact fun _ ↦ FreeGroup.lift.unique (g.comp (QuotientGroup.mk' _)) hg

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_δ' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j) :
    δ i ≫ δ j =
      δ (j.pred fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) ≫
        δ (Fin.castSucc i)

Proof state:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
hj : j = 0
⊢ False

Tactic:
simp [hj, Fin.not_lt_zero] at H

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ i ≤ j.pred ⋯

Tactic:
simpa only [Fin.le_iff_val_le_val, ← Nat.lt_succ_iff, Nat.succ_eq_add_one, ← Fin.val_succ,
  j.succ_pred, Fin.lt_iff_val_lt_val] using H

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ (j.pred ⋯) ≫ δ i.castSucc

Tactic:
rw [← δ_comp_δ]

Result:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ

n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ i ≤ j.pred ⋯

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

Tactic:
rw [Fin.succ_pred]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
lemma mk_add {x y : PGame} (hx : x.Numeric) (hy : y.Numeric) :
    Surreal.mk (x + y) (hx.add hy) = Surreal.mk x hx + Surreal.mk y hy

Proof state:
x y : PGame
hx : x.Numeric
hy : y.Numeric
⊢ mk (x + y) ⋯ = mk x hx + mk y hy

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Erase.lean
theorem coe_erase (a : α) (s : Finset α) : ↑(erase s a) = (s \ {a} : Set α) :=
  Set.ext fun _ => mem_erase.trans <| by rw [and_comm, Set.mem_diff, Set.mem_singleton_iff, mem_coe]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
x✝ : α
⊢ x✝ ≠ a ∧ x✝ ∈ s ↔ x✝ ∈ ↑s \ {a}

Tactic:
rw [and_comm, Set.mem_diff, Set.mem_singleton_iff, mem_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_singleton_iff {l : List α} {f : Nat → α → β} {b : β} :
    mapIdx f l = [b] ↔ ∃ (a : α), l = [a] ∧ f 0 a = b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
b : β
⊢ mapIdx f l = [b] ↔ ∃ a, l = [a] ∧ f 0 a = b

Tactic:
simp [mapIdx_eq_cons_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_ne_empty_of_right_ne_empty (s : Array α) : t ≠ #[] → s ++ t ≠ #[]

Proof state:
α : Type u_1
t s : Array α
⊢ t ≠ #[] → s ++ t ≠ #[]

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem le_div_iff_mul_le {I J K : Submodule R A} : I ≤ J / K ↔ I * K ≤ J

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I J K : Submodule R A
⊢ I ≤ J / K ↔ I * K ≤ J

Tactic:
rw [le_div_iff, mul_le]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem decompId_i_toKaroubi (X : C) : decompId_i ((toKaroubi C).obj X) = 𝟙 _

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : C
⊢ ((toKaroubi C).obj X).decompId_i = 𝟙 ((toKaroubi C).obj X)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem Integrable.inner_const (hf : Integrable f μ) (c : E) :
    Integrable (fun x => ⟪f x, c⟫) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f μ
c : E
⊢ Integrable (fun x => inner (f x) c) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f 1 μ
c : E
⊢ MemLp (fun x => inner (f x) c) 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f 1 μ
c : E
⊢ MemLp (fun x => inner (f x) c) 1 μ

Tactic:
exact hf.inner_const c

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem tsum_div_const [T2Space α] : ∑' x, f x / a = (∑' x, f x) / a

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑' (x : ι), f x / a = (∑' (x : ι), f x) / a

Tactic:
simpa only [div_eq_mul_inv] using tsum_mul_right

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem Inseparable.mem_measurableSet_iff {x y : γ} (h : Inseparable x y) {s : Set γ}
    (hs : MeasurableSet s) : x ∈ s ↔ y ∈ s :=
  MeasurableSet.induction_on_open (fun _ ↦ h.mem_open_iff) (fun _ _ ↦ Iff.not)
    (fun _ _ _ h ↦ by simp [h]) s hs

Proof state:
γ : Type u_3
inst✝² : TopologicalSpace γ
inst✝¹ : MeasurableSpace γ
inst✝ : BorelSpace γ
x y : γ
h✝ : Inseparable x y
s : Set γ
hs : MeasurableSet s
x✝² : ℕ → Set γ
x✝¹ : Pairwise (Function.onFun Disjoint x✝²)
x✝ : ∀ (i : ℕ), MeasurableSet (x✝² i)
h : ∀ (i : ℕ), x ∈ x✝² i ↔ y ∈ x✝² i
⊢ x ∈ ⋃ i, x✝² i ↔ y ∈ ⋃ i, x✝² i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_5 :
    (coordinate 5).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5

Proof state:
a0 a1 a2 a3 a4 a5 : Int
t : List Int
⊢ (coordinate 5).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: t)) = a5

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma intCast_cast_sub (x y : ZMod n) : (cast (x - y) : ℤ) = (cast x - cast y) % n

Proof state:
n : ℕ
x y : ZMod n
⊢ (x - y).cast = (x.cast - y.cast) % ↑n

Tactic:
rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/OfFn.lean
theorem getElem?_ofFn (f : Fin n → α) (i : Nat) :
    (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
⊢ (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_bool (f : Bool → Measure α) : sum f = f true + f false

Proof state:
α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
⊢ sum f = f true + f false

Tactic:
rw [sum_fintype, Fintype.sum_bool]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem iInf_toSubmodule {ι} (p : ι → LieSubmodule R L M) :
    (↑(⨅ i, p i) : Submodule R M) = ⨅ i, (p i : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⨅ i, ↑(p i)

Tactic:
rw [iInf, sInf_toSubmodule]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ sInf {x | ∃ s ∈ range fun i => p i, ↑s = x} = ⨅ i, ↑(p i)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ sInf {x | ∃ s ∈ range fun i => p i, ↑s = x} = ⨅ i, ↑(p i)

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x✝ : M
⊢ x✝ ∈ sInf {x | ∃ s ∈ range fun i => p i, ↑s = x} ↔ x✝ ∈ ⨅ i, ↑(p i)

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
x✝ : M
⊢ x✝ ∈ sInf {x | ∃ s ∈ range fun i => p i, ↑s = x} ↔ x✝ ∈ ⨅ i, ↑(p i)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negMap_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.negMap ⟦P⟧ = ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negMap ⟦P⟧ = ⟦![P x / P z, (toAffine W).negY (P x / P z) (P y / P z), 1]⟧

Tactic:
rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_one : ascPochhammer S 1 = X

Proof state:
S : Type u
inst✝ : Semiring S
⊢ ascPochhammer S 1 = X

Tactic:
simp [ascPochhammer]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_comp_mono (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) [Mono h] :
    kernelSubobject (f ≫ h) = kernelSubobject f :=
  le_antisymm (le_kernelSubobject _ _ ((cancel_mono h).mp (by simp))) (kernelSubobject_comp_le f h)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ ((kernelSubobject (f ≫ h)).arrow ≫ f) ≫ h = 0 ≫ h

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem of_smul_eq_smul {i : ι} (g : G i) (w : NormalWord d) :
    of (φ := φ) i g • w = g • w

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (of i) g • w = g • w

Tactic:
rw [summand_smul_def, summand_smul_def']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p*q).natDegree = p.natDegree + q.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
  Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem HasProd.map [CommMonoid γ] [TopologicalSpace γ] (hf : HasProd f a) {G}
    [FunLike G α γ] [MonoidHomClass G α γ] (g : G) (hg : Continuous g) :
    HasProd (g ∘ f) (g a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
⊢ HasProd (⇑g ∘ f) (g a)

Tactic:
have : (g ∘ fun s : Finset β ↦ ∏ b ∈ s, f b) = fun s : Finset β ↦ ∏ b ∈ s, (g ∘ f) b :=
  funext <| map_prod g _

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b
⊢ HasProd (⇑g ∘ f) (g a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b
⊢ Tendsto (⇑g ∘ fun s => ∏ b ∈ s, f b) atTop (𝓝 (g a))

Tactic:
exact (hg.tendsto a).comp hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b
⊢ Tendsto (fun s => ∏ b ∈ s, (⇑g ∘ f) b) atTop (𝓝 (g a))

Tactic:
rw [← this]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b
⊢ Tendsto (⇑g ∘ fun s => ∏ b ∈ s, f b) atTop (𝓝 (g a))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b
⊢ HasProd (⇑g ∘ f) (g a)

Tactic:
unfold HasProd

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
f : β → α
a : α
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
hf : HasProd f a
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : Continuous ⇑g
this : (⇑g ∘ fun s => ∏ b ∈ s, f b) = fun s => ∏ b ∈ s, (⇑g ∘ f) b
⊢ Tendsto (fun s => ∏ b ∈ s, (⇑g ∘ f) b) atTop (𝓝 (g a))
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem isoIsPullback_inv_fst (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
    (h.isoIsPullback _ _ h').inv ≫ fst = fst'

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
P' : C
fst' : P' ⟶ X
snd' : P' ⟶ Y
h : IsPullback fst snd f g
h' : IsPullback fst' snd' f g
⊢ (isoIsPullback X Y h h').inv ≫ fst = fst'

Tactic:
simp only [Iso.inv_comp_eq, isoIsPullback_hom_fst]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_pos_iff : 0 < orderOf x ↔ IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ 0 < orderOf x ↔ IsOfFinOrder x

Tactic:
rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem map_iInf {ι : Sort*} [Nonempty ι]
    [IsScalarTower R B B] [SMulCommClass R B B] (f : F)
    (hf : Function.Injective f) (S : ι → NonUnitalSubalgebra R A) :
    ((⨅ i, S i).map f : NonUnitalSubalgebra R B) = ⨅ i, (S i).map f

Proof state:
case a
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : FunLike F A B
inst✝⁵ : NonUnitalAlgHomClass F R A B
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ ↑(NonUnitalSubalgebra.map f (⨅ i, S i)) = ↑(⨅ i, NonUnitalSubalgebra.map f (S i))

Tactic:
simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S)

Result:
no goals

Proof state:
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : FunLike F A B
inst✝⁵ : NonUnitalAlgHomClass F R A B
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ NonUnitalSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalSubalgebra.map f (S i)

Tactic:
apply SetLike.coe_injective

Result:
case a
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : FunLike F A B
inst✝⁵ : NonUnitalAlgHomClass F R A B
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ ↑(NonUnitalSubalgebra.map f (⨅ i, S i)) = ↑(⨅ i, NonUnitalSubalgebra.map f (S i))
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).coeff n = 1

Tactic:
simp

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma klFun_zero : klFun 0 = 1

Proof state:
⊢ klFun 0 = 1

Tactic:
simp [klFun]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem min_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min (f x) a

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => f x ⊓ a

Tactic:
simpa only [max_eq_left (zero_le Kf)] using hf.min (LipschitzWith.const a)

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem mono_of_epi_of_epi_of_mono (hR₁ : R₁.Exact) (hR₂ : R₂.Exact)
    (hR₁' : Epi (R₁.map' 1 2)) (h₀ : Epi (app' φ 0)) (h₁ : Mono (app' φ 1)) :
    Mono (app' φ 2) :=
  mono_of_epi_of_epi_mono' φ (by simpa only [map'_comp R₁ 0 1 2] using hR₁.toIsComplex.zero 0)
    hR₁' hR₂ h₀ h₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)
h₀ : Epi (app' φ 0 ⋯)
h₁ : Mono (app' φ 1 ⋯)
⊢ R₁.map' 0 2 ⋯ ⋯ = 0

Tactic:
simpa only [map'_comp R₁ 0 1 2] using hR₁.toIsComplex.zero 0

Result:
no goals