harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bind_comm (p : PMF α) (q : PMF β) (f : α → β → PMF γ) :
    (p.bind fun a => q.bind (f a)) = q.bind fun b => p.bind fun a => f a b :=
  PMF.ext fun b => by
    simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm,
      ENNReal.tsum_mul_right.symm, mul_assoc, mul_left_comm, mul_comm] using ENNReal.tsum_comm

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : α → β → PMF γ
b : γ
⊢ (p.bind fun a => q.bind (f a)) b = (q.bind fun b => p.bind fun a => f a b) b

Tactic:
simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm,
  ENNReal.tsum_mul_right.symm, mul_assoc, mul_left_comm, mul_comm] using ENNReal.tsum_comm

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem card_cycleType_eq_zero {σ : Perm α} : Multiset.card σ.cycleType = 0 ↔ σ = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType.card = 0 ↔ σ = 1

Tactic:
rw [card_eq_zero, cycleType_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem neg : mapFun f (-x) = -mapFun f x

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ mapFun (⇑f) (-x) = -mapFun (⇑f) x

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem mk_apply (i : ι) : Basis.mk hli hsp i = v i :=
  show Finsupp.linearCombination _ v _ = v i by simp

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
i : ι
⊢ (linearCombination R v) (single i 1) = v i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
/-- Formula for `IsLocalizedModule.map` when each localized module is a `LocalizedModule`. -/
lemma map_LocalizedModules (g : M₀ →ₗ[R] M₁) (m : M₀) (s : S) :
    ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g)
    (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
have := (iso_apply_mk S (mkLinearMap S M₁) (g m) s).symm

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = (iso S (mkLinearMap S M₁)) (LocalizedModule.mk (g m) s)
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
simpa [map, lift, iso_localizedModule_eq_refl S M₀]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = (iso S (mkLinearMap S M₁)) (LocalizedModule.mk (g m) s)
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s

Tactic:
rw [iso_localizedModule_eq_refl, refl_apply] at this

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
inst✝³ : AddCommMonoid M₀
inst✝² : Module R M₀
M₁ : Type u_7
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
g : M₀ →ₗ[R] M₁
m : M₀
s : ↥S
this : ↑⋯.unit⁻¹ ((mkLinearMap S M₁) (g m)) = LocalizedModule.mk (g m) s
⊢ ((map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) (LocalizedModule.mk m s) = LocalizedModule.mk (g m) s
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem AnalyticAt.div {f g : E → 𝕝} {x : E}
    (fa : AnalyticAt 𝕜 f x) (ga : AnalyticAt 𝕜 g x) (g0 : g x ≠ 0) :
    AnalyticAt 𝕜 (f / g) x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f * g⁻¹) x

Tactic:
exact fa.mul (ga.inv g0)

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f / g) x

Tactic:
simp_rw [div_eq_mul_inv]

Result:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
x : E
fa : AnalyticAt 𝕜 f x
ga : AnalyticAt 𝕜 g x
g0 : g x ≠ 0
⊢ AnalyticAt 𝕜 (f * g⁻¹) x
-- Mathlib/CategoryTheory/Preadditive/Schur.lean
theorem isIso_iff_nonzero [HasKernels C] {X Y : C} [Simple X] [Simple Y] (f : X ⟶ Y) :
    IsIso f ↔ f ≠ 0 :=
  ⟨fun I => by
    intro h
    apply id_nonzero X
    simp only [← IsIso.hom_inv_id f, h, zero_comp],
   fun w => isIso_of_hom_simple w⟩

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
⊢ f ≠ 0

Tactic:
intro h

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ False

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ 𝟙 X = 0

Tactic:
simp only [← IsIso.hom_inv_id f, h, zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ False

Tactic:
apply id_nonzero X

Result:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ 𝟙 X = 0
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ π) :
    (-θ : Angle).sign ≤ 0

Proof state:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin

Tactic:
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

Result:
no goals

Proof state:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ (-↑θ).sign ≤ 0

Tactic:
rw [sign, sign_nonpos_iff, sin_neg, Left.neg_nonpos_iff]

Result:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem cancel_left {g : sInfHom β γ} {f₁ f₂ : sInfHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : InfSet α
inst✝¹ : InfSet β
inst✝ : InfSet γ
g : sInfHom β γ
f₁ f₂ : sInfHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem mem_div_iff_smul_subset {x : A} {I J : Submodule R A} : x ∈ I / J ↔ x • (J : Set A) ⊆ I :=
  ⟨fun h y ⟨y', hy', xy'_eq_y⟩ => by
    rw [← xy'_eq_y]
    apply h
    assumption, fun h _ hy => h (Set.smul_mem_smul_set hy)⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ y ∈ ↑I

Tactic:
rw [← xy'_eq_y]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ (fun x_1 => x • x_1) y' ∈ ↑I

Proof state:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ y' ∈ J

Tactic:
assumption

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ (fun x_1 => x • x_1) y' ∈ ↑I

Tactic:
apply h

Result:
case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ y' ∈ J
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
  Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]

Proof state:
a b : Int
Hpos : b ≠ 0
H : b * a = b
⊢ b * a = b * 1

Tactic:
rw [Int.mul_one, H]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.add_smul_sub_mem_interior' {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ closure s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) :
    x + t • (y - x) ∈ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • (y - x) ∈ interior s

Tactic:
simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm] using
  hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2)
    (add_sub_cancel _ _)

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem disjoint_lift'_closure_nhds [T25Space X] {x y : X} :
    Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y :=
  ⟨fun h hxy => by simp [hxy, nhds_neBot.ne] at h, fun h => T25Space.t2_5 h⟩

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T25Space X
x y : X
h : Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure)
hxy : x = y
⊢ False

Tactic:
simp [hxy, nhds_neBot.ne] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_congr {l₁ l₂ : Array α} (w : l₁ = l₂) {P : α → Prop} {H : ∀ x ∈ l₁, P x} :
    l₁.attachWith P H = l₂.attachWith P fun _ h => H _ (w ▸ h)

Proof state:
α : Type u_1
l₁ : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₁.attachWith P ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : Array α
w : l₁ = l₂
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₂.attachWith P ⋯

Tactic:
subst w

Result:
α : Type u_1
l₁ : Array α
P : α → Prop
H : ∀ (x : α), x ∈ l₁ → P x
⊢ l₁.attachWith P H = l₁.attachWith P ⋯
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@[simp]
lemma Γevaluation_eq_zero_iff_not_mem_basicOpen (x : X) (f : X.presheaf.obj (op ⊤)) :
    X.Γevaluation x f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f :=
  evaluation_eq_zero_iff_not_mem_basicOpen X ⟨x, show x ∈ ⊤ by trivial⟩ f

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
f : ↑(X.presheaf.obj (op ⊤))
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_center_homothety (p₁ p₂ : P) (c : 𝕜) :
    dist p₁ (homothety p₁ c p₂) = ‖c‖ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist p₁ ((homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂

Tactic:
simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Ioo_iff_Ioi (h : a < b) :
    ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIciTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioo a b) a ↔ ContinuousWithinAt f (Ioi a) a

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsGT h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
lemma volume_closedBall_of_dim_odd {k : ℕ} (hk : finrank ℝ E = 2 * k + 1) (x : E) (r : ℝ) :
    volume (closedBall x r) =
      .ofReal r ^ finrank ℝ E * .ofReal (π ^ k * 2 ^ (k + 1) / (finrank ℝ E : ℕ)‼)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ volume (closedBall x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(finrank ℝ E)‼)

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_odd hk x r]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
⊢ volume (closedBall x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(finrank ℝ E)‼)

Tactic:
have : Nontrivial E := Module.nontrivial_of_finrank_pos (R := ℝ) (hk ▸ (2 * k).succ_pos)

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
k : ℕ
hk : finrank ℝ E = 2 * k + 1
x : E
r : ℝ
this : Nontrivial E
⊢ volume (closedBall x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k * 2 ^ (k + 1) / ↑(finrank ℝ E)‼)
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_or_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∀ᶠ x in f, p x ∨ q) ↔ (∀ᶠ x in f, p x) ∨ q

Proof state:
α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q

Tactic:
simp only [@or_comm _ q, eventually_or_distrib_left]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem exists_reduced_word (w : W) : ∃ ω, ω.length = ℓ w ∧ w = π ω

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω

Tactic:
have := Nat.find_spec (cs.exists_word_with_prod w)

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
this : ∃ ω, ω.length = Nat.find ⋯ ∧ cs.wordProd ω = w
⊢ ∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
this : ∃ ω, ω.length = Nat.find ⋯ ∧ cs.wordProd ω = w
⊢ ∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω

Tactic:
tauto

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ ω, ω.length = cs.length w ∧ w = cs.wordProd ω

Tactic:
classical
have := Nat.find_spec (cs.exists_word_with_prod w)
tauto

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_self_sub_mul_self_eq (a b : Nat) : a * a - b * b = (a + b) * (a - b)

Proof state:
a b : Nat
⊢ a * a - b * b = (a + b) * (a - b)

Tactic:
rw [Nat.mul_sub_left_distrib, Nat.right_distrib, Nat.right_distrib, Nat.mul_comm b a,
  Nat.sub_add_eq, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma cauchy_pi_iff [Nonempty ι] {l : Filter (∀ i, α i)} :
    Cauchy l ↔ ∀ i, Cauchy (map (eval i) l)

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
inst✝ : Nonempty ι
l : Filter ((i : ι) → α i)
⊢ Cauchy l ↔ ∀ (i : ι), Cauchy (map (eval i) l)

Tactic:
simp_rw [Pi.uniformSpace_eq, cauchy_iInf_uniformSpace, cauchy_comap_uniformSpace]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/WithTop.lean
theorem map_sub [Sub β] [Bot β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y) (h₀ : f ⊥ = ⊥) :
    ∀ x y : WithTop α, (x - y).map f = x.map f - y.map f
  | _, ⊤ => by simp only [sub_top, map_coe, h₀, map_top]
  | ⊤, (x : α) => rfl
  | (x : α), (y : α) => by simp only [← coe_sub, map_coe, h]

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Bot α
inst✝¹ : Sub β
inst✝ : Bot β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f ⊥ = ⊥
x y : α
⊢ map f (↑x - ↑y) = map f ↑x - map f ↑y

Tactic:
simp only [← coe_sub, map_coe, h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Bot α
inst✝¹ : Sub β
inst✝ : Bot β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f ⊥ = ⊥
x✝ : WithTop α
⊢ map f (x✝ - ⊤) = map f x✝ - map f ⊤

Tactic:
simp only [sub_top, map_coe, h₀, map_top]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_eq_left (ha : a ≠ 0) : a * b = a ↔ b = 1

Proof state:
a b : ℕ
ha : a ≠ 0
⊢ a * b = a ↔ b = 1

Tactic:
simpa using Nat.mul_right_inj ha (c := 1)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuousOn_sub :
    ContinuousOn (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) { p : ℝ≥0∞ × ℝ≥0∞ | p ≠ ⟨∞, ∞⟩ }

Proof state:
⊢ ContinuousOn (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)}

Tactic:
rw [ContinuousOn]

Result:
⊢ ∀ x ∈ {p | p ≠ (⊤, ⊤)}, ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} x

Proof state:
case mk
x y : ℝ≥0∞
hp : (x, y) ∈ {p | p ≠ (⊤, ⊤)}
⊢ ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} (x, y)

Tactic:
simp only [Ne, Set.mem_setOf_eq, Prod.mk.inj_iff] at hp

Result:
case mk
x y : ℝ≥0∞
hp : ¬(x = ⊤ ∧ y = ⊤)
⊢ ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} (x, y)

Proof state:
case mk
x y : ℝ≥0∞
hp : ¬(x = ⊤ ∧ y = ⊤)
⊢ ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} (x, y)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (tendsto_sub (not_and_or.mp hp))

Result:
no goals

Proof state:
⊢ ∀ x ∈ {p | p ≠ (⊤, ⊤)}, ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} x

Tactic:
rintro ⟨x, y⟩ hp

Result:
case mk
x y : ℝ≥0∞
hp : (x, y) ∈ {p | p ≠ (⊤, ⊤)}
⊢ ContinuousWithinAt (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)} (x, y)
-- Mathlib/Algebra/Polynomial/Module/Basic.lean
lemma smul_def (f : R[X]) (m : PolynomialModule R M) :
    f • m = aeval (Finsupp.lmapDomain M R Nat.succ) f m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R[X]
m : PolynomialModule R M
⊢ f • m = ((aeval (Finsupp.lmapDomain M R Nat.succ)) f) m

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp, norm_cast] lemma coe_eq_zero : (r : ℝ) = 0 ↔ r = 0

Proof state:
r : ℝ≥0
⊢ ↑r = 0 ↔ r = 0

Tactic:
rw [← coe_zero, coe_inj]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
lemma isMax_of_not_succ_mem [SuccOrder α] {a : s} (h : succ ↑a ∉ s) : IsMax a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ (if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = a

Tactic:
split_ifs <;> trivial

Result:
no goals

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ succ a = a

Tactic:
change dite .. = _

Result:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ (if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ IsMax a

Tactic:
rw [← succ_eq_iff_isMax]

Result:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ succ a = a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∉ s
⊢ IsMax a

Tactic:
classical
rw [← succ_eq_iff_isMax]
change dite .. = _
split_ifs <;> trivial

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₁_yonedaEquivFst {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G)
    (p : YonedaCollection F X) :
    (YonedaCollection.map₁ η p).yonedaEquivFst = p.yonedaEquivFst

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).yonedaEquivFst = p.yonedaEquivFst

Tactic:
simp only [YonedaCollection.yonedaEquivFst_eq, map₁_fst]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem aeval_eq_sum_range [Algebra R S] {p : R[X]} (x : S) :
    aeval x p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range (p.natDegree + 1), (algebraMap R S) (p.coeff x_1) * x ^ x_1

Tactic:
exact eval₂_eq_sum_range (algebraMap R S) x

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ (aeval x) p = ∑ i ∈ range (p.natDegree + 1), p.coeff i • x ^ i

Tactic:
simp_rw [Algebra.smul_def]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
x : S
⊢ (aeval x) p = ∑ x_1 ∈ range (p.natDegree + 1), (algebraMap R S) (p.coeff x_1) * x ^ x_1