harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Basic.lean
theorem one_div_mul_one_div : 1 / a * (1 / b) = 1 / (a * b)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ 1 / a * (1 / b) = 1 / (a * b)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.smul (hs : StrictConvex 𝕜 s) (c : 𝕝) : StrictConvex 𝕜 (c • s)

Proof state:
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (0 • s)

Tactic:
exact (subsingleton_zero_smul_set _).strictConvex

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)

Tactic:
exact hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
⊢ StrictConvex 𝕜 (c • s)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (0 • s)

case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coroot_eq_coreflection_of_root_eq
    {i j k : ι} (hk : P.root k = P.reflection i (P.root j)) :
    P.coroot k = P.coreflection i (P.coroot j)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hk : P.root k = (P.reflection i) (P.root j)
⊢ P.coroot k = (P.coreflection i) (P.coroot j)

Tactic:
rw [← P.root_reflection_perm, EmbeddingLike.apply_eq_iff_eq] at hk

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hk : k = (P.reflection_perm i) j
⊢ P.coroot k = (P.coreflection i) (P.coroot j)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hk : k = (P.reflection_perm i) j
⊢ P.coroot k = (P.coreflection i) (P.coroot j)

Tactic:
rw [← P.coroot_reflection_perm, hk]

Result:
no goals
-- Mathlib/Algebra/IsPrimePow.lean
theorem isPrimePow_nat_iff_bounded (n : ℕ) :
    IsPrimePow n ↔ ∃ p : ℕ, p ≤ n ∧ ∃ k : ℕ, k ≤ n ∧ p.Prime ∧ 0 < k ∧ p ^ k = n

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ 1 ≤ p ^ k

Tactic:
exact Nat.pow_le_pow_right hp.one_lt.le hk

Result:
no goals

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃ p_1 ≤ p ^ k, ∃ k_1 ≤ p ^ k, Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k

Tactic:
refine ⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩

Result:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ≤ p ^ k

Proof state:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
refine Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩

Result:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
n : ℕ
⊢ IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rw [isPrimePow_nat_iff]

Result:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
rintro ⟨p, k, hp, hk, rfl⟩

Result:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ ∃ p_1 ≤ p ^ k, ∃ k_1 ≤ p ^ k, Nat.Prime p_1 ∧ 0 < k_1 ∧ p_1 ^ k_1 = p ^ k

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ≤ p ^ k

Tactic:
conv => { lhs; rw [← (pow_one p)] }

Result:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ 1 ≤ p ^ k
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem parallelogram_law {x y : E} : ⟪x + y, x + y⟫ + ⟪x - y, x - y⟫ = 2 * (⟪x, x⟫ + ⟪y, y⟫)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜 + (⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜) = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)

Tactic:
simp only [inner_add_add_self, inner_sub_sub_self]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫_𝕜 + ⟪x, y⟫_𝕜 + ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜 + (⟪x, x⟫_𝕜 - ⟪x, y⟫_𝕜 - ⟪y, x⟫_𝕜 + ⟪y, y⟫_𝕜) = 2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜)
-- Mathlib/Topology/Constructions.lean
theorem Filter.Tendsto.finSnoc
    {f : Y → ∀ j : Fin n, π j.castSucc} {g : Y → π (Fin.last _)}
    {l : Filter Y} {x : ∀ j, π (Fin.castSucc j)} {y : π (Fin.last _)}
    (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
    Tendsto (fun a => Fin.snoc (f a) (g a)) l (𝓝 <| Fin.snoc x y) :=
  tendsto_pi_nhds.2 fun j => Fin.lastCases (by simpa) (by simpa using tendsto_pi_nhds.1 hf) j

Proof state:
Y : Type v
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
f : Y → (j : Fin n) → π j.castSucc
g : Y → π (Fin.last n)
l : Filter Y
x : (j : Fin n) → π j.castSucc
y : π (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ Tendsto (fun i => Fin.snoc (f i) (g i) (Fin.last n)) l (𝓝 (Fin.snoc x y (Fin.last n)))

Tactic:
simpa

Result:
no goals

Proof state:
Y : Type v
n : ℕ
π : Fin (n + 1) → Type u_8
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (π i)
f : Y → (j : Fin n) → π j.castSucc
g : Y → π (Fin.last n)
l : Filter Y
x : (j : Fin n) → π j.castSucc
y : π (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 => Fin.snoc (f i_1) (g i_1) i.castSucc) l (𝓝 (Fin.snoc x y i.castSucc))

Tactic:
simpa using tendsto_pi_nhds.1 hf

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
@[simp] lemma norm_smul_const {R β : Type*} [NormedAddCommGroup β] [NormedDivisionRing R]
    [Module R β] [BoundedSMul R β] (f : C(α, R)) (b : β) :
    ‖f • const α b‖ = ‖f‖ * ‖b‖

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CompactSpace α
R : Type u_4
β : Type u_5
inst✝³ : NormedAddCommGroup β
inst✝² : NormedDivisionRing R
inst✝¹ : Module R β
inst✝ : BoundedSMul R β
f : C(α, R)
b : β
⊢ ‖f • const α b‖ = ‖f‖ * ‖b‖

Tactic:
simp only [← coe_nnnorm, NNReal.coe_mul, nnnorm_smul_const]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
lemma rieszContent_ne_top {K : Compacts X} : rieszContent Λ K ≠ ⊤

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
⊢ (rieszContent Λ) K ≠ ⊤

Tactic:
simp [rieszContent, ne_eq, ENNReal.coe_ne_top, not_false_eq_true]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem add_right_cancel (h₁ : c ≡ d [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :
    a ≡ b [ZMOD n]

Proof state:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ d + b [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
exact h₁.add_left_cancel h₂

Result:
no goals

Proof state:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : a + c ≡ b + d [ZMOD n]
⊢ a ≡ b [ZMOD n]

Tactic:
rw [add_comm a, add_comm b] at h₂

Result:
n a b c d : ℤ
h₁ : c ≡ d [ZMOD n]
h₂ : c + a ≡ d + b [ZMOD n]
⊢ a ≡ b [ZMOD n]
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_zero (μ : Measure α) : μ.prod (0 : Measure β) = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
⊢ μ.prod 0 = 0

Tactic:
simp [Measure.prod]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc]
lemma XIsoOfEq_inv_naturality {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') :
    φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n n' : ι
h : n = n'
⊢ φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).inv = (K.XIsoOfEq ⋯).inv ≫ φ.f n

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
n : ι
⊢ φ.f n ≫ (L.XIsoOfEq ⋯).inv = (K.XIsoOfEq ⋯).inv ≫ φ.f n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_mul {f g : K[X]} (hf : Splits i f) (hg : Splits i g) : Splits i (f * g) :=
  letI := Classical.decEq L
  if h : (f * g).map i = 0 then Or.inl h
  else
    Or.inr @fun p hp hpf =>
      ((irreducible_iff_prime.1 hp).2.2 _ _
            (show p ∣ map i f * map i g by convert hpf; rw [Polynomial.map_mul])).elim
        (hf.resolve_left (fun hf => by simp [hf] at h) hp)
        (hg.resolve_left (fun hg => by simp [hg] at h) hp)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g : K[X]
hf✝ : Splits i f
hg : Splits i g
this : DecidableEq L := Classical.decEq L
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
hf : map i f = 0
⊢ False

Tactic:
simp [hf] at h

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g : K[X]
hf : Splits i f
hg : Splits i g
this : DecidableEq L := Classical.decEq L
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
⊢ p ∣ map i f * map i g

Tactic:
convert hpf

Result:
case h.e'_4
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g : K[X]
hf : Splits i f
hg : Splits i g
this : DecidableEq L := Classical.decEq L
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
⊢ map i f * map i g = map i (f * g)

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g : K[X]
hf : Splits i f
hg✝ : Splits i g
this : DecidableEq L := Classical.decEq L
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
hg : map i g = 0
⊢ False

Tactic:
simp [hg] at h

Result:
no goals

Proof state:
case h.e'_4
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f g : K[X]
hf : Splits i f
hg : Splits i g
this : DecidableEq L := Classical.decEq L
h : ¬map i (f * g) = 0
p : L[X]
hp : Irreducible p
hpf : p ∣ map i (f * g)
⊢ map i f * map i g = map i (f * g)

Tactic:
rw [Polynomial.map_mul]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem lift_nhds_left {x : α} {g : Set α → Filter β} (hg : Monotone g) :
    (𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g (ball x s)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun s => g (ball x s)

Tactic:
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]

Result:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun s => g (ball x s)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun s => g (ball x s)

Tactic:
simp_rw [ball, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_congr {as bs : Array α}
    (w : as = bs) (h : start = start') (h' : stop = stop') :
    as.extract start stop = bs.extract start' stop'

Proof state:
α : Type u_1
start start' stop stop' : Nat
as bs : Array α
w : as = bs
h : start = start'
h' : stop = stop'
⊢ as.extract start stop = bs.extract start' stop'

Tactic:
subst w h h'

Result:
α : Type u_1
start stop : Nat
as : Array α
⊢ as.extract start stop = as.extract start stop

Proof state:
α : Type u_1
start stop : Nat
as : Array α
⊢ as.extract start stop = as.extract start stop

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_eq_false_iff : ∀ {x y : Bool}, (x || y) = false ↔ x = false ∧ y = false

Proof state:
⊢ ∀ {x y : Bool}, (x || y) = false ↔ x = false ∧ y = false

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem snd_comp_prodComm :
    (LinearMap.snd R M₂ M).comp (prodComm R M M₂).toLinearMap = (LinearMap.fst R M M₂)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ LinearMap.snd R M₂ M ∘ₗ ↑(prodComm R M M₂) = LinearMap.fst R M M₂

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem HasBasis.limsup_eq_iInf_iSup {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α}
    (h : f.HasBasis p s) : limsup u f = ⨅ (i) (_ : p i), ⨆ a ∈ s i, u a :=
  (h.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, id]

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : f.HasBasis p s
⊢ ⨅ i, ⨅ (_ : p i), sSup (u '' s i) = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a

Tactic:
simp only [sSup_image, id]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_idem (a : α) : a ⊔ a = a

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a : α
⊢ a ⊔ a = a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem natCast_mul (m n : ℕ) :
    (m * n : ℕ) = (m : EReal) * (n : EReal)

Proof state:
m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem C_mul_dvd (ha : a ≠ 0) : C a * p ∣ q ↔ p ∣ q :=
  ⟨fun h => dvd_trans (dvd_mul_left _ _) h, fun ⟨r, hr⟩ =>
    ⟨C a⁻¹ * r, by
      rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
        one_mul, hr]⟩⟩

Proof state:
R : Type u
a : R
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = C a * p * (C a⁻¹ * r)

Tactic:
rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, mul_inv_cancel₀ ha, C.map_one,
  one_mul, hr]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem erase_eq_self_iff_forall_bne [BEq α] (a : α) (xs : List α) :
    xs.erase a = xs ↔ ∀ (x : α), x ∈ xs → ¬x == a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
xs : List α
⊢ xs.erase a = xs ↔ ∀ (x : α), x ∈ xs → ¬(x == a) = true

Tactic:
rw [erase_eq_eraseP', eraseP_eq_self_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_unique_of_dist_ne_zero {α β} {F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β]
    [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : dist x y ≠ 0)
    (hr : dist (f x) (f y) = r * dist x y) : r = ratio f :=
  ratio_unique_of_nndist_ne_zero (NNReal.coe_ne_zero.1 hxy) <|
    NNReal.eq <| by rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]

Proof state:
α : Type u_6
β : Type u_7
F : Type u_5
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (f x) (f y) = ↑r * dist x y
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)

Tactic:
rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem measure_condCDF_Iic (ρ : Measure (α × ℝ)) (a : α) (x : ℝ) :
    (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (condCDF ρ a x)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x - 0)

Tactic:
exact (condCDF ρ a).measure_Iic (tendsto_condCDF_atBot ρ a) _

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x)

Tactic:
rw [← sub_zero (condCDF ρ a x)]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (condCDF ρ a).measure (Iic x) = ENNReal.ofReal (↑(condCDF ρ a) x - 0)
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem w {A B : CostructuredArrow S T} (f : A ⟶ B) : S.map f.left ≫ B.hom = A.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
A B : CostructuredArrow S T
f : A ⟶ B
⊢ S.map f.left ≫ B.hom = A.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem image_top {s : Set α} (h : Set.Nonempty s) :
    (⊤ : Rel α β).image s = Set.univ :=
  Set.eq_univ_of_forall fun _ ↦ ⟨h.some, by simp [h.some_mem, Top.top]⟩

Proof state:
α : Type u_1
β : Type u_2
s : Set α
h : s.Nonempty
x✝ : β
⊢ h.some ∈ s ∧ ⊤ h.some x✝

Tactic:
simp [h.some_mem, Top.top]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem finrank_comap (f : L →ₐ[F] E) : finrank (A.comap f) L = relfinrank A f.fieldRange

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A : IntermediateField F E
f : L →ₐ[F] E
⊢ finrank (↥(comap f A)) L = A.relfinrank f.fieldRange

Tactic:
simpa using congr(toNat $(lift_rank_comap A f))

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem norm_dvd_iff {x : S} (hx : Prime (Algebra.norm ℤ x)) {y : ℤ} :
    Algebra.norm ℤ x ∣ y ↔ x ∣ y

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ (Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y

Tactic:
rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ S), ← Ideal.mem_comap,
  ← Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton,
  Int.natAbs_dvd]

Result:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
x : S
hx : Prime ((Algebra.norm ℤ) x)
y : ℤ
⊢ Nat.Prime (absNorm (span {x}))

Tactic:
rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]

Result:
no goals
-- Mathlib/Data/Finsupp/Ext.lean
theorem addHom_ext [AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄
    (H : ∀ x y, f (single x y) = g (single x y)) : f = g

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
⊢ f = g

Tactic:
refine AddMonoidHom.eq_of_eqOn_denseM add_closure_setOf_eq_single ?_

Result:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
⊢ Set.EqOn ⇑f ⇑g {f | ∃ a b, f = single a b}

Proof state:
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
⊢ Set.EqOn ⇑f ⇑g {f | ∃ a b, f = single a b}

Tactic:
rintro _ ⟨x, y, rfl⟩

Result:
case intro.intro
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
x : α
y : M
⊢ f (single x y) = g (single x y)

Proof state:
case intro.intro
α : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f g : (α →₀ M) →+ N
H : ∀ (x : α) (y : M), f (single x y) = g (single x y)
x : α
y : M
⊢ f (single x y) = g (single x y)

Tactic:
apply H

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem comap_dist_left_atTop (c : α) : comap (dist c) atTop = cobounded α

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
⊢ comap (dist c) atTop = cobounded α

Tactic:
simpa only [dist_comm _ c] using comap_dist_right_atTop c

Result:
no goals
-- Mathlib/Order/Circular.lean
theorem compl_cIoo {a b : α} : (cIoo a b)ᶜ = cIcc b a

Proof state:
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ x✝ ∈ cIcc b a

Tactic:
rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : CircularOrder α
a b x✝ : α
⊢ x✝ ∈ (cIoo a b)ᶜ ↔ x✝ ∈ cIcc b a
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum fun e a => f a * x ^ e

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = p.sum fun e a => f a * x ^ e

Tactic:
rw [eval₂_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_extractLsb' (start len : Nat) (x : BitVec n) (i : Nat) :
    (extractLsb' start len x).getLsbD i = (i < len && x.getLsbD (start+i))

Proof state:
n start len : Nat
x : BitVec n
i : Nat
⊢ (extractLsb' start len x).getLsbD i = (decide (i < len) && x.getLsbD (start + i))

Tactic:
simp [getLsbD, Nat.lt_succ]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem map_div_right_eq_self (μ : Measure G) [IsMulRightInvariant μ] (g : G) :
    map (· / g) μ = μ

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : DivInvMonoid G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
g : G
⊢ Measure.map (fun x => x / g) μ = μ

Tactic:
simp_rw [div_eq_mul_inv, map_mul_right_eq_self μ g⁻¹]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_ge_eq_Iic [DecidablePred (· ≤ a)] : ({x | x ≤ a} : Finset _) = Iic a

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
⊢ filter (fun x => x ≤ a) univ = Iic a

Tactic:
ext

Result:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
a✝ : α
⊢ a✝ ∈ filter (fun x => x ≤ a) univ ↔ a✝ ∈ Iic a

Proof state:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => x ≤ a
a✝ : α
⊢ a✝ ∈ filter (fun x => x ≤ a) univ ↔ a✝ ∈ Iic a

Tactic:
simp

Result:
no goals