harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma condCDF_eq_stieltjesOfMeasurableRat_unit_prod (ρ : Measure (α × ℝ)) (a : α) :
    condCDF ρ a = stieltjesOfMeasurableRat (fun (p : Unit × α) r ↦ (preCDF ρ r p.2).toReal)
      (measurable_preCDF'.comp measurable_snd) ((), a)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ condCDF ρ a = stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), a)

Tactic:
ext x

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ ↑(condCDF ρ a) x = ↑(stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), a)) x

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ ↑(condCDF ρ a) x = ↑(stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), a)) x

Tactic:
rw [condCDF, ← stieltjesOfMeasurableRat_unit_prod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem signExtend_eq (x : BitVec w) : x.signExtend w = x

Proof state:
w : Nat
x : BitVec w
⊢ signExtend w x = x

Tactic:
rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_intCast_iff_of_nonneg {z : ℤ} (hz : 0 ≤ z) :
    Irrational (√z) ↔ ¬IsSquare z

Proof state:
z : ℤ
hz : 0 ≤ z
⊢ Irrational √↑z ↔ ¬IsSquare z

Tactic:
rw [← Rat.isSquare_intCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg (mod_cast hz),
  Rat.cast_intCast]

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_choose {p n k b : ℕ} (hp : p.Prime) (hkn : k ≤ n) (hnb : log p n < b) :
    emultiplicity p (choose n k) = #{i ∈ Ico 1 b | p ^ i ≤ k % p ^ i + (n - k) % p ^ i}

Proof state:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b

Tactic:
exact this.symm ▸ hnb

Result:
no goals

Proof state:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
⊢ emultiplicity p (n.choose k) = ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))

Tactic:
have := Nat.sub_add_cancel hkn

Result:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ emultiplicity p (n.choose k) = ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))

Proof state:
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ emultiplicity p (n.choose k) = ↑(#(filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)))

Tactic:
convert @emultiplicity_choose' p (n - k) k b hp _

Result:
case h.e'_2.h.e'_4.h.e'_1
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k

p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ log p (n - k + k) < b

Proof state:
case h.e'_2.h.e'_4.h.e'_1
p n k b : ℕ
hp : Prime p
hkn : k ≤ n
hnb : log p n < b
this : n - k + k = n
⊢ n = n - k + k

Tactic:
rw [this]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem exists_nhds_split_inv {s : Set G} (hs : s ∈ 𝓝 (1 : G)) :
    ∃ V ∈ 𝓝 (1 : G), ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
⊢ s ∈ 𝓝 ((fun x => x.1 * x.2⁻¹) (1, 1))

Tactic:
simpa

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Tactic:
have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) :=
  continuousAt_fst.mul continuousAt_snd.inv (by simpa)

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
this : (fun p => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
this : (fun p => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Tactic:
simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using
  this

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem monic (hx : IsIntegral A x) : Monic (minpoly A x)

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic

Tactic:
exact (degree_lt_wf.min_mem _ hx).1

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).Monic

Tactic:
rw [dif_pos hx]

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic

Proof state:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (minpoly A x).Monic

Tactic:
delta minpoly

Result:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : Ring B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).Monic
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.setLIntegral_kernel_prod_right {f : α → β → ℝ≥0∞}
    (hf : Measurable (uncurry f)) {s : Set β} (hs : MeasurableSet s) :
    Measurable fun a => ∫⁻ b in s, f a b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β) in s, f a b ∂κ a

Tactic:
simp_rw [← lintegral_restrict κ hs]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂(κ.restrict hs) a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂(κ.restrict hs) a

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem snoc_comp_nat_add {n m : ℕ} {α : Sort*} (f : Fin (m + n) → α) (a : α) :
    (snoc f a : Fin _ → α) ∘ (natAdd m : Fin (n + 1) → Fin (m + n + 1)) =
      snoc (f ∘ natAdd m) a

Proof state:
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
⊢ snoc f a ∘ natAdd m = snoc (f ∘ natAdd m) a

Tactic:
ext i

Result:
case h
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) i = snoc (f ∘ natAdd m) a i

Proof state:
case h
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) i = snoc (f ∘ natAdd m) a i

Tactic:
refine Fin.lastCases ?_ (fun i ↦ ?_) i

Result:
case h.refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) (last n) = snoc (f ∘ natAdd m) a (last n)

case h.refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ natAdd m) i.castSucc = snoc (f ∘ natAdd m) a i.castSucc

Proof state:
case h.refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = snoc (f ∘ natAdd m) a (last n)

Tactic:
rw [snoc_last, natAdd_last, snoc_last]

Result:
no goals

Proof state:
case h.refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ (snoc f a ∘ natAdd m) i.castSucc = snoc (f ∘ natAdd m) a i.castSucc

Tactic:
simp only [comp_apply, snoc_castSucc]

Result:
case h.refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (natAdd m i.castSucc) = f (natAdd m i)

Proof state:
case h.refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ (snoc f a ∘ natAdd m) (last n) = snoc (f ∘ natAdd m) a (last n)

Tactic:
simp only [Function.comp_apply]

Result:
case h.refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = snoc (f ∘ natAdd m) a (last n)

Proof state:
case h.refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (natAdd m i.castSucc) = f (natAdd m i)

Tactic:
rw [natAdd_castSucc, snoc_castSucc]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
lemma nilpotencyClass_eq_succ_iff {k : ℕ} :
    nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Proof state:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
s : Set ℕ := {k | x ^ k = 0}
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Tactic:
have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁

Result:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
s : Set ℕ := {k | x ^ k = 0}
this : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Proof state:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Tactic:
let s : Set ℕ := {k | x ^ k = 0}

Result:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
s : Set ℕ := {k | x ^ k = 0}
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Proof state:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
k : ℕ
s : Set ℕ := {k | x ^ k = 0}
this : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Tactic:
simp [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem IsPrimePow.minFac_pow_factorization_eq {n : ℕ} (hn : IsPrimePow n) :
    n.minFac ^ n.factorization n.minFac = n

Proof state:
n : ℕ
hn : IsPrimePow n
⊢ n.minFac ^ n.factorization n.minFac = n

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := hn

Result:
case intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k

Tactic:
rw [hp.pow_minFac hk.ne', hp.factorization_pow, Finsupp.single_eq_same]

Result:
no goals

Proof state:
case intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k

Tactic:
rw [← Nat.prime_iff] at hp

Result:
case intro.intro.intro.intro
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
@[ext] lemma ext {f g : StieltjesFunction} (h : ∀ x, f x = g x) : f = g

Proof state:
f g : StieltjesFunction
h : ∀ (x : ℝ), ↑f x = ↑g x
⊢ f = g

Tactic:
exact (StieltjesFunction.mk.injEq ..).mpr (funext h)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma inv_pow_sub₀ (ha : a ≠ 0) (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n

Tactic:
rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_eq_empty_iff {l : Array α} {n : Nat} : l.zipIdx n = #[] ↔ l = #[]

Proof state:
α : Type u_1
l : Array α
n : Nat
⊢ l.zipIdx n = #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ { toList := toList✝ }.zipIdx n = #[] ↔ { toList := toList✝ } = #[]

Proof state:
case mk
α : Type u_1
n : Nat
toList✝ : List α
⊢ { toList := toList✝ }.zipIdx n = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closedBall_subset_cthickening {α : Type*} [PseudoMetricSpace α] {x : α} {E : Set α}
    (hx : x ∈ E) (δ : ℝ) : closedBall x δ ⊆ cthickening δ E

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ E

Tactic:
refine (closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ ?_)

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ {x} ⊆ E

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ {x} ⊆ E

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma associator_hom_snd_fst (X Y Z : C) :
    (α_ X Y Z).hom ≫ snd _ _ ≫ fst _ _ = fst _ _ ≫ snd _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.fst (product (product X Y).cone.pt Z).cone ≫ Limits.BinaryFan.snd (product X Y).cone =
    fst (X ⊗ Y) Z ≫ snd X Y

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ snd X (Y ⊗ Z) ≫ fst Y Z = fst (X ⊗ Y) Z ≫ snd X Y

Tactic:
erw [lift_snd_assoc, lift_fst]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z : C
⊢ Limits.BinaryFan.fst (product (product X Y).cone.pt Z).cone ≫ Limits.BinaryFan.snd (product X Y).cone =
    fst (X ⊗ Y) Z ≫ snd X Y
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem L1.SimpleFunc.integrable (f : α →₁ₛ[μ] E) :
    Integrable (Lp.simpleFunc.toSimpleFunc f) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
⊢ MemLp (⇑(Lp.simpleFunc.toSimpleFunc f)) 1 μ

Tactic:
exact Lp.simpleFunc.memLp f

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
⊢ Integrable (⇑(Lp.simpleFunc.toSimpleFunc f)) μ

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f : ↥(Lp.simpleFunc E 1 μ)
⊢ MemLp (⇑(Lp.simpleFunc.toSimpleFunc f)) 1 μ
-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfp_mem_range_lfpApprox : f.lfp ∈ Set.range (lfpApprox f ⊥)

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ∈ Set.range (lfpApprox f ⊥)

Tactic:
use ord <| succ #α

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = lfp f

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = lfp f

Tactic:
exact lfpApprox_ord_eq_lfp f

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalComp_nil_cons (α : f ≅ g) (β : g ≅ h) (η : h ⟶ i) (ηs : i ⟶ j) :
    α.hom ≫ (β.hom ≫ η ≫ ηs) = (α ≪≫ β).hom ≫ η ≫ ηs

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h i j : a ⟶ b
α : f ≅ g
β : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
⊢ α.hom ≫ β.hom ≫ η ≫ ηs = (α ≪≫ β).hom ≫ η ≫ ηs

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
@[to_additive]
lemma fn_max_mul_fn_min (f : α → β) (a b : α) : f (max a b) * f (min a b) = f a * f b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommSemigroup β
f : α → β
a b : α
⊢ f (a ⊔ b) * f (a ⊓ b) = f a * f b

Tactic:
obtain h | h := le_total a b <;> simp [h, mul_comm]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_range {α : Type*} [Small.{u} α] (f : α → ZFSet.{u}) :
    rank (range f) = ⨆ i, succ (rank (f i))

Proof state:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank = ⨆ i, succ (f i).rank

Tactic:
apply (Ordinal.iSup_le _).antisymm'

Result:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ i, succ (f i).rank

α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Proof state:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ i, succ (f i).rank

Tactic:
simpa [rank_le_iff, ← succ_le_iff] using Ordinal.le_iSup _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Tactic:
simp [rank_lt_of_mem]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem comap_uniformity_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
    (hf : Pairwise fun x y => (f x, f y) ∉ s) : comap (Prod.map f f) (𝓤 β) = 𝓟 idRel

Proof state:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓟 idRel

Tactic:
calc
  comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
  _ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
  _ ≤ 𝓟 idRel := principal_mono.2 ?_

Result:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ Prod.map f f ⁻¹' s ⊆ idRel

Proof state:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 idRel

Tactic:
refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))

Result:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓟 idRel

Proof state:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ Prod.map f f ⁻¹' s ⊆ idRel

Tactic:
rintro ⟨x, y⟩

Result:
case mk
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
x y : α
⊢ (x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ idRel

Proof state:
case mk
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
x y : α
⊢ (x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ idRel

Tactic:
simpa [not_imp_not] using @hf x y

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem findP?_insert [@TransCmp α cmp] (t : RBSet α cmp) (v cut) [IsStrictCut cmp cut] :
    (t.insert v).findP? cut = if cut v = .eq then some v else t.findP? cut

Proof state:
α : Type u_1
cmp : α → α → Ordering
inst✝¹ : TransCmp cmp
t : RBSet α cmp
v : α
cut : α → Ordering
inst✝ : IsStrictCut cmp cut
⊢ (t.insert v).findP? cut = if cut v = Ordering.eq then some v else t.findP? cut

Tactic:
split <;> [exact findP?_insert_of_eq t ‹_›; exact findP?_insert_of_ne t ‹_›]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem zero_or (x : Nat) : 0 ||| x = x

Proof state:
x : Nat
⊢ 0 ||| x = x

Tactic:
simp only [HOr.hOr, OrOp.or, lor]

Result:
x : Nat
⊢ bitwise or 0 x = x

Proof state:
x : Nat
⊢ bitwise or 0 x = x

Tactic:
unfold bitwise

Result:
x : Nat
⊢ (if 0 = 0 then if (false || true) = true then x else 0
    else
      if x = 0 then if (true || false) = true then 0 else 0
      else
        let n' := 0 / 2;
        let m' := x / 2;
        let b₁ := 0 % 2 = 1;
        let b₂ := x % 2 = 1;
        let r := bitwise or n' m';
        if (decide b₁ || decide b₂) = true then r + r + 1 else r + r) =
    x

Proof state:
x : Nat
⊢ (if 0 = 0 then if (false || true) = true then x else 0
    else
      if x = 0 then if (true || false) = true then 0 else 0
      else
        let n' := 0 / 2;
        let m' := x / 2;
        let b₁ := 0 % 2 = 1;
        let b₂ := x % 2 = 1;
        let r := bitwise or n' m';
        if (decide b₁ || decide b₂) = true then r + r + 1 else r + r) =
    x

Tactic:
simp [@eq_comm _ 0]

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem measure_eq_zero_or_one_or_top_of_indepSet_self {t : Set Ω}
    (h_indep : IndepSet t t μ) : μ t = 0 ∨ μ t = 1 ∨ μ t = ∞

Proof state:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
t : Set Ω
h_indep : IndepSet t t μ
⊢ μ t = 0 ∨ μ t = 1 ∨ μ t = ⊤

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
  using Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self h_indep

Result:
no goals
-- Mathlib/Data/Pi/Interval.lean
theorem card_Ioo : #(Ioo a b) = ∏ i, #(Icc (a i) (b i)) - 2

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioo a b) = ∏ i : ι, #(Icc (a i) (b i)) - 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
lemma comp (g h : L ≃+* L) : χ₀ n (g * h) =
    χ₀ n g * χ₀ n h

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ (g * h) ↑↑ζ = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)

Tactic:
change g (h (ζ : Lˣ)) = _

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ g (h ↑↑ζ) = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ g (h ↑↑ζ) = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)

Tactic:
rw [toFun_spec, ← Subgroup.coe_pow, toFun_spec, mul_comm, Subgroup.coe_pow, ← pow_mul,
  ← Subgroup.coe_pow]

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ↑↑(ζ ^ ((χ₀ n h).val * (χ₀ n g).val)) = ↑(↑ζ ^ (χ₀ n h * χ₀ n g).val)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ↑↑(ζ ^ ((χ₀ n h).val * (χ₀ n g).val)) = ↑(↑ζ ^ (χ₀ n h * χ₀ n g).val)

Tactic:
congr 2

Result:
case e_self
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ↑(ζ ^ ((χ₀ n h).val * (χ₀ n g).val)) = ↑ζ ^ (χ₀ n h * χ₀ n g).val

Proof state:
case e_self
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ζ ^ ((χ₀ n h).val * (χ₀ n g).val) = ζ ^ (χ₀ n h * χ₀ n g).val

Tactic:
simp only [pow_eq_pow_iff_modEq, ← ZMod.natCast_eq_natCast_iff, SubmonoidClass.coe_pow,
  ZMod.natCast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card]

Result:
no goals

Proof state:
case e_self
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ↑(ζ ^ ((χ₀ n h).val * (χ₀ n g).val)) = ↑ζ ^ (χ₀ n h * χ₀ n g).val

Tactic:
norm_cast

Result:
case e_self
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ ζ ^ ((χ₀ n h).val * (χ₀ n g).val) = ζ ^ (χ₀ n h * χ₀ n g).val

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
⊢ χ₀ n (g * h) = χ₀ n g * χ₀ n h

Tactic:
refine (toFun_unique n (g * h) _ <| fun ζ ↦ ?_).symm

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g h : L ≃+* L
ζ : ↥(rootsOfUnity n L)
⊢ (g * h) ↑↑ζ = ↑(↑ζ ^ (χ₀ n g * χ₀ n h).val)
-- Mathlib/MeasureTheory/Measure/Comap.lean
lemma map_symm {μ : Measure α} (e : β ≃ᵐ α) : μ.map e.symm = μ.comap e

Proof state:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
μ : Measure α
e : β ≃ᵐ α
⊢ Measure.map (⇑e.symm) μ = Measure.comap (⇑e) μ

Tactic:
rw [← comap_symm, symm_symm]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.encard_eq_encard_of_isBase (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) :
    B₁.encard = B₂.encard

Proof state:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
⊢ B₁.encard = B₂.encard

Tactic:
rw [M.isBase_exchange.encard_isBase_eq hB₁ hB₂]

Result:
no goals