harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Restriction.lean
@[simp]
lemma updateFinset_frestrictLe (a : α) (x : Π a, π a) : updateFinset x _ (frestrictLe a x) = x

Proof state:
α : Type u_1
inst✝² : Preorder α
π : α → Type u_2
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
a : α
x : (a : α) → π a
⊢ updateFinset x (Iic a) (frestrictLe a x) = x

Tactic:
simp [frestrictLe]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
/-- A functor preserving larger filtered colimits also preserves smaller filtered colimits. -/
lemma preservesFilteredColimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
    [UnivLE.{w₂, w₂'}] [PreservesFilteredColimitsOfSize.{w', w₂'} F] :
      PreservesFilteredColimitsOfSize.{w, w₂} F where
  preserves_filtered_colimits J _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ PreservesColimitsOfShape J F

Tactic:
haveI := IsFiltered.of_equivalence e.symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsFiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesColimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsFiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv e F

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
⊢ PreservesColimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesFilteredColimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ PreservesColimitsOfShape J F
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_mul_cos_add_sin_mul_I_eq_toIocMod {r : ℝ} (hr : 0 < r) (θ : ℝ) :
    arg (r * (cos θ + sin θ * I)) = toIocMod Real.two_pi_pos (-π) θ

Proof state:
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
convert arg_mul_cos_add_sin_mul_I hr hi using 3

Result:
case h.e'_2.h.e'_1.h.e'_6
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π
⊢ cos ↑θ + sin ↑θ * I = cos ↑(toIocMod Real.two_pi_pos (-π) θ) + sin ↑(toIocMod Real.two_pi_pos (-π) θ) * I

Proof state:
case h.e'_2.h.e'_1.h.e'_6
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π
⊢ cos ↑θ + sin ↑θ * I = cos ↑(toIocMod Real.two_pi_pos (-π) θ) + sin ↑(toIocMod Real.two_pi_pos (-π) θ) * I

Tactic:
simp [toIocMod, cos_sub_int_mul_two_pi, sin_sub_int_mul_two_pi]

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π

Tactic:
convert toIocMod_mem_Ioc _ _ θ

Result:
case h.e'_4.h.e'_4
r : ℝ
hr : 0 < r
θ : ℝ
⊢ π = -π + 2 * π

Proof state:
case h.e'_4.h.e'_4
r : ℝ
hr : 0 < r
θ : ℝ
⊢ π = -π + 2 * π

Tactic:
ring

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ

Tactic:
have hi : toIocMod Real.two_pi_pos (-π) θ ∈ Set.Ioc (-π) π := by
  convert toIocMod_mem_Ioc _ _ θ
  ring

Result:
r : ℝ
hr : 0 < r
θ : ℝ
hi : toIocMod Real.two_pi_pos (-π) θ ∈ Ioc (-π) π
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg = toIocMod Real.two_pi_pos (-π) θ
-- Mathlib/Data/NNReal/Defs.lean
@[simp, norm_cast] lemma one_le_coe : 1 ≤ (r : ℝ) ↔ 1 ≤ r

Proof state:
r : ℝ≥0
⊢ 1 ≤ ↑r ↔ 1 ≤ r

Tactic:
rw [← coe_le_coe, coe_one]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem rel_mem (hr : BiUnique R) : (R ⇒ Forall₂ R ⇒ Iff) (· ∈ ·) (· ∈ ·)
  | a, b, _, [], [], Forall₂.nil => by simp only [not_mem_nil]
  | a, b, h, a' :: as, b' :: bs, Forall₂.cons h₁ h₂ => by
    simp only [mem_cons]
    exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun x1 x2 => x1 ∈ x2) a (a' :: as) ↔ (fun x1 x2 => x1 ∈ x2) b (b' :: bs)

Tactic:
simp only [mem_cons]

Result:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
x✝ : R a b
⊢ (fun x1 x2 => x1 ∈ x2) a [] ↔ (fun x1 x2 => x1 ∈ x2) b []

Tactic:
simp only [not_mem_nil]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ a = a' ∨ a ∈ as ↔ b = b' ∨ b ∈ bs

Tactic:
exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_one_of_mul_left (h : a * b = 1) : b = 1 :=
  congr_arg Units.inv <| Subsingleton.elim (Units.mk _ _ h <| by rwa [mul_comm]) 1

Proof state:
α : Type u
inst✝¹ : CommMonoid α
inst✝ : Subsingleton αˣ
a b : α
h : a * b = 1
⊢ b * a = 1

Tactic:
rwa [mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem tmul_apply (a : ι → M) (b : ι₂ → M) :
    tmul ((⨂ₜ[R] i, a i) ⊗ₜ[R] ⨂ₜ[R] i, b i) = ⨂ₜ[R] i, Sum.elim a b i

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : ι → M
b : ι₂ → M
⊢ PiTensorProduct.tmul (((tprod R) fun i => a i) ⊗ₜ[R] (tprod R) fun i => b i) = (tprod R) fun i => Sum.elim a b i

Tactic:
erw [TensorProduct.lift.tmul, PiTensorProduct.lift.tprod, PiTensorProduct.lift.tprod]

Result:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : ι → M
b : ι₂ → M
⊢ ((((currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R)) fun i => a i) fun i => b i) =
    (tprod R) fun i => Sum.elim a b i

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : ι → M
b : ι₂ → M
⊢ ((((currySumEquiv R ι (⨂[R] (i : ι ⊕ ι₂), M) M ι₂) (tprod R)) fun i => a i) fun i => b i) =
    (tprod R) fun i => Sum.elim a b i

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Fib/Zeckendorf.lean
@[simp]
lemma IsZeckendorfRep_nil : IsZeckendorfRep []

Proof state:
⊢ [].IsZeckendorfRep

Tactic:
simp [IsZeckendorfRep]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem zero_smul_subset (t : Set β) : (0 : Set α) • t ⊆ 0

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
t : Set β
⊢ 0 • t ⊆ 0

Tactic:
simp [subset_def, mem_smul]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem coe_fin_one (a : Fin 1) : (a : ℕ) = 0

Proof state:
a : Fin 1
⊢ ↑a = 0

Tactic:
simp [Subsingleton.elim a 0]

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousAt.finset_inf' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
    ContinuousAt (s.inf' hne f) x

Proof state:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeInf L
inst✝ : ContinuousInf L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.inf' hne f) x

Tactic:
simpa only [← Finset.inf'_apply] using finset_inf'_apply hne hs

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
/-- A map from a compact space to a T2 space is a homeomorphism iff it is continuous and
  bijective. -/
lemma isHomeomorph_iff_continuous_bijective [CompactSpace X] [T2Space Y] :
    IsHomeomorph f ↔ Continuous f ∧ Bijective f

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous f
⊢ IsClosedMap f ∧ Bijective f ↔ Bijective f

Tactic:
rw [eq_true hf.isClosedMap, true_and]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ Continuous f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous f ∧ Bijective f

Tactic:
refine and_congr_right fun hf ↦ ?_

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous f
⊢ IsClosedMap f ∧ Bijective f ↔ Bijective f

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ IsHomeomorph f ↔ Continuous f ∧ Bijective f

Tactic:
rw [isHomeomorph_iff_continuous_isClosedMap_bijective]

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ Continuous f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous f ∧ Bijective f
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_zero_measure : AEMeasurable f (0 : Measure α)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
a✝ : Nontrivial α
⊢ AEMeasurable f 0

Tactic:
inhabit α

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f 0

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f 0

Tactic:
exact ⟨fun _ => f default, measurable_const, rfl⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
⊢ AEMeasurable f 0

Tactic:
nontriviality α

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
a✝ : Nontrivial α
⊢ AEMeasurable f 0
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_extend_bot {e : ι → β} (he : Injective e) (f : ι → α) :
    ⨆ j, extend e f ⊥ j = ⨆ i, f i

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ i, ⨆ (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ i, ⨆ (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i = ⨆ i, f i

Tactic:
simp +contextual [he.extend_apply, extend_apply', @iSup_comm _ β ι]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ ⨆ j, extend e f ⊥ j = ⨆ i, f i

Tactic:
rw [iSup_split _ fun j => ∃ i, e i = j]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ (⨆ i, ⨆ (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ i, ⨆ (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i = ⨆ i, f i
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_div_int_iff : Irrational (x / m) ↔ m ≠ 0 ∧ Irrational x

Proof state:
m : ℤ
x : ℝ
⊢ Irrational (x / ↑m) ↔ m ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_intCast, irrational_div_rat_iff, Int.cast_ne_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem range_mkQ_comp (f : M →ₛₗ[τ₁₂] M₂) : f.range.mkQ.comp f = 0 :=
  LinearMap.ext fun x => by simp

Proof state:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
x : M
⊢ ((range f).mkQ.comp f) x = 0 x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma ball_eq_or_disjoint :
    ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
⊢ ball x r = ball y r

Tactic:
have h₁ := ball_eq_of_mem <| Set.inter_subset_left h.some_mem

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
h₁ : ball x r = ball h.some r
⊢ ball x r = ball y r

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
h₁ : ball x r = ball h.some r
⊢ ball x r = ball y r

Tactic:
have h₂ := ball_eq_of_mem <| Set.inter_subset_right h.some_mem

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
h₁ : ball x r = ball h.some r
h₂ : ball y r = ball h.some r
⊢ ball x r = ball y r

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
⊢ ball x r = ball y r ∨ Disjoint (ball x r) (ball y r)

Tactic:
refine Set.disjoint_or_nonempty_inter (ball x r) (ball y r) |>.symm.imp (fun h ↦ ?_) id

Result:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
⊢ ball x r = ball y r

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
h : (ball x r ∩ ball y r).Nonempty
h₁ : ball x r = ball h.some r
h₂ : ball y r = ball h.some r
⊢ ball x r = ball y r

Tactic:
exact h₁.trans h₂.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_max_distrib_right (a b c : Nat) :
    min (max a b) c = max (min a c) (min b c)

Proof state:
a b c : Nat
⊢ min c (max a b) = max (min c a) (min c b)

Tactic:
exact Nat.min_max_distrib_left ..

Result:
no goals

Proof state:
a b c : Nat
⊢ min c (max a b) = max (min c a) (min b c)

Tactic:
rw [Nat.min_comm _ c]

Result:
a b c : Nat
⊢ min c (max a b) = max (min c a) (min c b)

Proof state:
a b c : Nat
⊢ min (max a b) c = max (min a c) (min b c)

Tactic:
repeat rw [Nat.min_comm _ c]

Result:
a b c : Nat
⊢ min c (max a b) = max (min c a) (min c b)
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma floorRoot_pow_self (hn : n ≠ 0) (a : ℕ) : floorRoot n (a ^ n) = a

Proof state:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 => x1 ^ x2) = a

Tactic:
split_ifs <;> simp [*]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ n.floorRoot (a ^ n) = a

Tactic:
simp [floorRoot_def, pos_iff_ne_zero.2, hn]

Result:
n : ℕ
hn : n ≠ 0
a : ℕ
⊢ (if a = 0 then 0 else a.factorization.prod fun x1 x2 => x1 ^ x2) = a
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive] lemma pair_mul (a b : α) (s : Set α) : {a, b} * s = a • s ∪ b • s

Proof state:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ {a, b} * s = a • s ∪ b • s

Tactic:
rw [insert_eq, union_mul, singleton_mul, singleton_mul]

Result:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x => a * x) '' s ∪ (fun x => b * x) '' s = a • s ∪ b • s

Proof state:
α : Type u_2
inst✝ : Mul α
a b : α
s : Set α
⊢ (fun x => a * x) '' s ∪ (fun x => b * x) '' s = a • s ∪ b • s

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem primeFactors_pow (a : M) {n : ℕ} (hn : 0 < n) : primeFactors (a ^ n) = primeFactors a

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
hn : 0 < n
⊢ primeFactors (a ^ n) = primeFactors a

Tactic:
simp_rw [primeFactors, normalizedFactors_pow, Multiset.toFinset_nsmul _ _ hn.ne']

Result:
no goals
-- Mathlib/Order/Filter/EventuallyConst.lean
lemma eventuallyConst_atTop [SemilatticeSup α] [Nonempty α] :
    EventuallyConst f atTop ↔ (∃ i, ∀ j, i ≤ j → f j = f i) :=
  (atTop_basis.eventuallyConst_iff' fun _ _ ↦ left_mem_Ici).trans <| by
    simp only [true_and, mem_Ici]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
⊢ (∃ i, True ∧ ∀ y ∈ Ici i, f y = f i) ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i

Tactic:
simp only [true_and, mem_Ici]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_Iic_atTop [Preorder α] [(atTop : Filter α).IsCountablyGenerated]
    (μ : Measure α) : Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ))

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ univ))

Tactic:
rw [← iUnion_Iic]

Result:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ (⋃ a, Iic a)))

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝¹ : Preorder α
inst✝ : atTop.IsCountablyGenerated
μ : Measure α
⊢ Tendsto (fun x => μ (Iic x)) atTop (𝓝 (μ (⋃ a, Iic a)))

Tactic:
exact tendsto_measure_iUnion_atTop monotone_Iic

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_assoc_comm_cons {l : List α} {a₁ a₂} : ((a₁ :: l) <*> a₂) = a₁ ⋆ l <*> a₂

Proof state:
α : Type u
op : α → α → α
ha : Std.Associative op
hc : Std.Commutative op
l : List α
a₁ a₂ : α
⊢ ((a₁ :: l) <*> a₂) = op a₁ (l <*> a₂)

Tactic:
rw [foldl_cons, hc.comm, foldl_assoc]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem to_nhds_mono {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) (a : α) :
    @nhds _ (@UniformSpace.toTopologicalSpace _ u₁) a ≤
      @nhds _ (@UniformSpace.toTopologicalSpace _ u₂) a

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)

Tactic:
exact lift'_mono h le_rfl

Result:
no goals

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]

Result:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem continuous_coordChange (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈ e₁.baseSet)
    (h₂ : b ∈ e₂.baseSet) : Continuous (e₁.coordChange e₂ b)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous (e₁.coordChange e₂ b)

Tactic:
refine continuous_snd.comp (e₂.toPartialHomeomorph.continuousOn.comp_continuous
  (e₁.toPartialHomeomorph.continuousOn_symm.comp_continuous ?_ ?_) ?_)

Result:
case refine_1
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous (Prod.mk b)

case refine_2
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target

case refine_3
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), ↑e₁.symm (b, x) ∈ e₂.source

Proof state:
case refine_3
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
intro x

Result:
case refine_3
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Proof state:
case refine_3
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]

Result:
no goals

Proof state:
case refine_1
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous (Prod.mk b)

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_2
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target

Tactic:
exact fun x => e₁.mem_target.2 h₁

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem wPathCasesOn_eta {α : TypeVec n} {a : P.A} {f : P.last.B a → P.last.W}
    (h : P.WPath ⟨a, f⟩ ⟹ α) : P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) = h

Tactic:
ext i x

Result:
case a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i x = h i x

Proof state:
case a.h
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i x = h i x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem of_int_sub (m : ℤ) (h : Irrational (m - x)) : Irrational x :=
  of_rat_sub m <| by rwa [Rat.cast_intCast]

Proof state:
x : ℝ
m : ℤ
h : Irrational (↑m - x)
⊢ Irrational (↑↑m - x)

Tactic:
rwa [Rat.cast_intCast]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem ofBaseChange_tmul_one (Q : QuadraticForm R V) (z : A) :
    ofBaseChange A Q (z ⊗ₜ 1) = algebraMap _ _ z

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
⊢ (ofBaseChange A Q) (z ⊗ₜ[R] 1) = (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z

Tactic:
show algebraMap _ _ z * ofBaseChangeAux A Q 1 = _

Result:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) 1 =
    (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) 1 =
    (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z

Tactic:
rw [map_one, mul_one]

Result:
no goals