harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem support_hsum_subset {s : SummableFamily Γ R α} : s.hsum.support ⊆ ⋃ a : α, (s a).support :=
  fun g hg => by
  rw [mem_support, coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)] at hg
  obtain ⟨a, _, h2⟩ := exists_ne_zero_of_sum_ne_zero hg
  rw [Set.mem_iUnion]
  exact ⟨a, h2⟩

Proof state:
case intro.intro
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0
a : α
left✝ : a ∈ ⋯.toFinset
h2 : (s a).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Tactic:
rw [Set.mem_iUnion]

Result:
case intro.intro
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0
a : α
left✝ : a ∈ ⋯.toFinset
h2 : (s a).coeff g ≠ 0
⊢ ∃ i, g ∈ (s i).support

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Tactic:
obtain ⟨a, _, h2⟩ := exists_ne_zero_of_sum_ne_zero hg

Result:
case intro.intro
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0
a : α
left✝ : a ∈ ⋯.toFinset
h2 : (s a).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : g ∈ s.hsum.support
⊢ g ∈ ⋃ a, (s a).support

Tactic:
rw [mem_support, coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)] at hg

Result:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0
⊢ g ∈ ⋃ a, (s a).support

Proof state:
case intro.intro
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : ∑ i ∈ ⋯.toFinset, (s i).coeff g ≠ 0
a : α
left✝ : a ∈ ⋯.toFinset
h2 : (s a).coeff g ≠ 0
⊢ ∃ i, g ∈ (s i).support

Tactic:
exact ⟨a, h2⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem ofReal_cpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : ((x ^ y : ℝ) : ℂ) = (x : ℂ) ^ (y : ℂ)

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(x ^ y) = ↑x ^ ↑y

Tactic:
simp only [Real.rpow_def_of_nonneg hx, Complex.cpow_def, ofReal_eq_zero]

Result:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log ↑x * ↑y)

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ ↑(if x = 0 then if y = 0 then 1 else 0 else rexp (Real.log x * y)) =
    if x = 0 then if y = 0 then 1 else 0 else cexp (log ↑x * ↑y)

Tactic:
split_ifs <;>
simp [Complex.ofReal_log hx]

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem eq_of_hammingDist_eq_zero {x y : ∀ i, β i} : hammingDist x y = 0 → x = y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y = 0 → x = y

Tactic:
simp_rw [hammingDist, card_eq_zero, filter_eq_empty_iff, Classical.not_not, funext_iff, mem_univ,
  forall_true_left, imp_self]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma pairwiseDisjoint_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    PairwiseDisjoint (hC.disjointOfDiff hs ht : Set (Set α)) id

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
simp only [disjointOfDiff, coe_sdiff, coe_singleton]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑⋯.choose \ {∅}).PairwiseDisjoint id

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id

Tactic:
classical
simp only [disjointOfDiff, coe_sdiff, coe_singleton]
exact Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1
    diff_subset

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑⋯.choose \ {∅}).PairwiseDisjoint id

Tactic:
exact Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1
    diff_subset

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem H1LequivOfIsTrivial_comp_H1π [A.IsTrivial] :
    (H1LequivOfIsTrivial A).comp (H1π A).hom = oneCocyclesLequivOfIsTrivial A

Proof state:
case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : ↑(ModuleCat.of k ↥(oneCocycles A))
x✝ : Additive G
⊢ ((↑(H1LequivOfIsTrivial A) ∘ₗ ModuleCat.Hom.hom (H1π A)) x✝¹) x✝ = (↑(oneCocyclesLequivOfIsTrivial A) x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ ↑(H1LequivOfIsTrivial A) ∘ₗ ModuleCat.Hom.hom (H1π A) = ↑(oneCocyclesLequivOfIsTrivial A)

Tactic:
ext

Result:
case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : ↑(ModuleCat.of k ↥(oneCocycles A))
x✝ : Additive G
⊢ ((↑(H1LequivOfIsTrivial A) ∘ₗ ModuleCat.Hom.hom (H1π A)) x✝¹) x✝ = (↑(oneCocyclesLequivOfIsTrivial A) x✝¹) x✝
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma even_xor'_odd (n : ℤ) : Xor' (Even n) (Odd n)

Proof state:
n : ℤ
⊢ Xor' (Even n) (Odd n)

Tactic:
cases even_or_odd n with
| inl h => exact Or.inl ⟨h, not_odd_iff_even.2 h⟩
| inr h => exact Or.inr ⟨h, not_even_iff_odd.2 h⟩

Result:
no goals

Proof state:
case inl
n : ℤ
h : Even n
⊢ Xor' (Even n) (Odd n)

Tactic:
exact Or.inl ⟨h, not_odd_iff_even.2 h⟩

Result:
no goals

Proof state:
case inr
n : ℤ
h : Odd n
⊢ Xor' (Even n) (Odd n)

Tactic:
exact Or.inr ⟨h, not_even_iff_odd.2 h⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem mul_self_lt_top_iff {a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤

Proof state:
a : ℝ≥0∞
⊢ a = 0 → a < ⊤

Tactic:
rintro rfl

Result:
⊢ 0 < ⊤

Proof state:
a : ℝ≥0∞
⊢ a * a < ⊤ ↔ a < ⊤

Tactic:
rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]

Result:
a : ℝ≥0∞
⊢ a = 0 → a < ⊤

Proof state:
⊢ 0 < ⊤

Tactic:
exact zero_lt_top

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_inter_of_injOn [DecidableEq α] {f : α → β} (s t : Finset α)
    (hf : Set.InjOn f (s ∪ t)) : (s ∩ t).image f = s.image f ∩ t.image f :=
  coe_injective <| by
    push_cast
    exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ ↑(image f (s ∩ t)) = ↑(image f s ∩ image f t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f (↑s ∪ ↑t)
⊢ f '' (↑s ∩ ↑t) = f '' ↑s ∩ f '' ↑t

Tactic:
exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_le_iff' {m : ℕ+} {v : PrimeMultiset} :
    factorMultiset m ≤ v ↔ m ∣ v.prod

Proof state:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v.prod.factorMultiset ↔ m ∣ v.prod := factorMultiset_le_iff
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
rw [v.factorMultiset_prod] at h

Result:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v ↔ m ∣ v.prod
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Proof state:
m : ℕ+
v : PrimeMultiset
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
let h := @factorMultiset_le_iff m v.prod

Result:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v.prod.factorMultiset ↔ m ∣ v.prod := factorMultiset_le_iff
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Proof state:
m : ℕ+
v : PrimeMultiset
h : m.factorMultiset ≤ v ↔ m ∣ v.prod
⊢ m.factorMultiset ≤ v ↔ m ∣ v.prod

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fundamentalDomain_reindex {ι' : Type*} (e : ι ≃ ι') :
    fundamentalDomain (b.reindex e) = fundamentalDomain b

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ x✝ ∈ fundamentalDomain (b.reindex e) ↔ x✝ ∈ fundamentalDomain b

Tactic:
simp_rw [mem_fundamentalDomain, Basis.repr_reindex_apply]

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ (∀ (i : ι'), (b.repr x✝) (e.symm i) ∈ Set.Ico 0 1) ↔ ∀ (i : ι), (b.repr x✝) i ∈ Set.Ico 0 1

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ ∀ (b_1 : ι'), (b.repr x✝) (e.symm b_1) ∈ Set.Ico 0 1 ↔ (b.repr x✝) (e.symm b_1) ∈ Set.Ico 0 1

Tactic:
simp_rw [implies_true]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
⊢ fundamentalDomain (b.reindex e) = fundamentalDomain b

Tactic:
ext

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ x✝ ∈ fundamentalDomain (b.reindex e) ↔ x✝ ∈ fundamentalDomain b

Proof state:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ (∀ (i : ι'), (b.repr x✝) (e.symm i) ∈ Set.Ico 0 1) ↔ ∀ (i : ι), (b.repr x✝) i ∈ Set.Ico 0 1

Tactic:
rw [Equiv.forall_congr' e]

Result:
case h
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝² : NormedLinearOrderedField K
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace K E
b : Basis ι K E
ι' : Type u_4
e : ι ≃ ι'
x✝ : E
⊢ ∀ (b_1 : ι'), (b.repr x✝) (e.symm b_1) ∈ Set.Ico 0 1 ↔ (b.repr x✝) (e.symm b_1) ∈ Set.Ico 0 1
-- Mathlib/Data/ENNReal/Inv.lean
lemma isUnit_iff : IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Proof state:
case intro
u : ℝ≥0∞ˣ
hu : ↑u = ⊤
this : ↑u * ↑u⁻¹ = ⊤ * ↑u⁻¹
⊢ False

Tactic:
norm_cast at this

Result:
case intro
u : ℝ≥0∞ˣ
hu : ↑u = ⊤
this : ↑(u * u⁻¹) = ⊤ * ↑u⁻¹
⊢ False

Proof state:
case intro
u : ℝ≥0∞ˣ
hu : ↑u = ⊤
⊢ False

Tactic:
have := congr($hu * u⁻¹)

Result:
case intro
u : ℝ≥0∞ˣ
hu : ↑u = ⊤
this : ↑u * ↑u⁻¹ = ⊤ * ↑u⁻¹
⊢ False

Proof state:
case intro
u : ℝ≥0∞ˣ
⊢ ↑u ≠ ⊤

Tactic:
rintro hu

Result:
case intro
u : ℝ≥0∞ˣ
hu : ↑u = ⊤
⊢ False

Proof state:
case intro
u : ℝ≥0∞ˣ
hu : ↑u = ⊤
this : ↑(u * u⁻¹) = ⊤ * ↑u⁻¹
⊢ False

Tactic:
simp [mul_inv_cancel] at this

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ⊤

Tactic:
refine ⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
  fun ha ↦ ⟨⟨a, a⁻¹, ENNReal.mul_inv_cancel ha.1 ha.2, ENNReal.inv_mul_cancel ha.1 ha.2⟩, rfl⟩⟩

Result:
a : ℝ≥0∞
ha : IsUnit a
⊢ a ≠ ⊤

Proof state:
a : ℝ≥0∞
ha : IsUnit a
⊢ a ≠ ⊤

Tactic:
obtain ⟨u, rfl⟩ := ha

Result:
case intro
u : ℝ≥0∞ˣ
⊢ ↑u ≠ ⊤
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem Matrix.toBilin'_comp (M : Matrix n n R₁) (P Q : Matrix n o R₁) :
    M.toBilin'.comp (Matrix.toLin' P) (Matrix.toLin' Q) = Matrix.toBilin' (Pᵀ * M * Q) :=
  BilinForm.toMatrix'.injective
    (by simp only [BilinForm.toMatrix'_comp, BilinForm.toMatrix'_toBilin', toMatrix'_toLin'])

Proof state:
R₁ : Type u_1
inst✝⁴ : CommSemiring R₁
n : Type u_5
o : Type u_6
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : DecidableEq n
inst✝ : DecidableEq o
M : Matrix n n R₁
P Q : Matrix n o R₁
⊢ BilinForm.toMatrix' ((toBilin' M).comp (toLin' P) (toLin' Q)) = BilinForm.toMatrix' (toBilin' (Pᵀ * M * Q))

Tactic:
simp only [BilinForm.toMatrix'_comp, BilinForm.toMatrix'_toBilin', toMatrix'_toLin']

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem dite_eq_iff : dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Tactic:
by_cases P <;> simp [*, exists_prop_of_true, exists_prop_of_false]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma rnDeriv_eq_one_iff_eq [HaveLebesgueDecomposition μ ν] [SigmaFinite ν] (hμν : μ ≪ ν) :
    μ.rnDeriv ν =ᵐ[ν] 1 ↔ μ = ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1 ↔ μ = ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ ν.rnDeriv_self⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᶠ[ae ν] 1
⊢ μ = ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᶠ[ae ν] 1
⊢ μ = ν

Tactic:
rw [← withDensity_rnDeriv_eq _ _ hμν, withDensity_congr_ae h, withDensity_one]

Result:
no goals
-- Mathlib/Topology/Baire/Lemmas.lean
theorem Dense.inter_of_Gδ {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) (hsc : Dense s)
    (htc : Dense t) : Dense (s ∩ t)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ b, bif b then s else t)

Tactic:
apply dense_iInter_of_Gδ <;> simp [Bool.forall_bool, *]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (s ∩ t)

Tactic:
rw [inter_eq_iInter]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ b, bif b then s else t)
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma SMulPosMono.lift [SMulPosMono α γ]
    (hf : ∀ {b₁ b₂}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂)
    (smul : ∀ (a : α) b, f (a • b) = a • f b)
    (zero : f 0 = 0) : SMulPosMono α β where
  elim b hb a₁ a₂ ha

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b

Tactic:
exact smul_le_smul_of_nonneg_right ha hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 ≤ b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
simp only [← hf, zero, smul] at *

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : α → β → True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem suppPreservation_iff_isUniform : q.SuppPreservation ↔ q.IsUniform

Proof state:
case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ IsUniform → SuppPreservation

Tactic:
rintro h α ⟨a, f⟩

Result:
case mpr.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Proof state:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ f i '' univ = f' i '' univ

Tactic:
rw [← MvPFunctor.supp_eq, ← MvPFunctor.supp_eq, ← h, h', h]

Result:
no goals

Proof state:
case mpr.mk
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (abs ⟨a, f⟩) = supp ⟨a, f⟩

Tactic:
ext

Result:
case mpr.mk.h.h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ supp (abs ⟨a, f⟩) x✝¹ ↔ x✝ ∈ supp ⟨a, f⟩ x✝¹

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation ↔ IsUniform

Tactic:
constructor

Result:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation → IsUniform

case mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ IsUniform → SuppPreservation

Proof state:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ SuppPreservation → IsUniform

Tactic:
intro h α a a' f f' h' i

Result:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a a' : (P F).A
f : (P F).B a ⟹ α
f' : (P F).B a' ⟹ α
h' : abs ⟨a, f⟩ = abs ⟨a', f'⟩
i : Fin2 n
⊢ f i '' univ = f' i '' univ

Proof state:
case mpr.mk.h.h
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
x✝¹ : Fin2 n
x✝ : α x✝¹
⊢ x✝ ∈ supp (abs ⟨a, f⟩) x✝¹ ↔ x✝ ∈ supp ⟨a, f⟩ x✝¹

Tactic:
rwa [supp_eq_of_isUniform, MvPFunctor.supp_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem continuous_circleTransformDeriv {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z w : ℂ}
    (hf : ContinuousOn f (sphere z R)) (hw : w ∈ ball z R) :
    Continuous (circleTransformDeriv R z w f)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransformDeriv R z w f)

Tactic:
rw [circleTransformDeriv_eq]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ

Tactic:
exact (continuous_circleMap_inv hw).smul (continuous_circleTransform hR hf hw)

Result:
no goals
-- Mathlib/Topology/Constructible.lean
@[simp] lemma IsRetrocompact.empty : IsRetrocompact (∅ : Set X)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact ∅

Tactic:
simp [IsRetrocompact]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_not_self : ∀(b : Bool), (b = (!b)) ↔ False

Proof state:
⊢ ∀ (b : Bool), b = !b ↔ False

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sum_eq_of_lt {ι : Type*} {s : Finset ι} {f : ι → R} {j : ι}
    (hj : j ∈ s) (h0 : v (f j) ≠ 0) (hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)) :
    v (∑ i ∈ s, f i) = v (f j)

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
h0 : v (f j) ≠ 0
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
⊢ v (∑ i ∈ s, f i) = v (f j)

Tactic:
rw [Finset.sum_eq_add_sum_diff_singleton hj]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
h0 : v (f j) ≠ 0
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
⊢ v (f j + ∑ x ∈ s \ {j}, f x) = v (f j)

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
j : ι
hj : j ∈ s
h0 : v (f j) ≠ 0
hf : ∀ i ∈ s \ {j}, v (f i) < v (f j)
⊢ v (f j + ∑ x ∈ s \ {j}, f x) = v (f j)

Tactic:
exact map_add_eq_of_lt_left _ (map_sum_lt _ h0 hf)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToL1_le_norm_setToL1SCLM (hT : DominatedFinMeasAdditive μ T C) :
    ‖setToL1 hT‖ ≤ ‖setToL1SCLM α E μ hT‖ :=
  calc
    ‖setToL1 hT‖ ≤ (1 : ℝ≥0) * ‖setToL1SCLM α E μ hT‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ‖setToL1 hT‖ ≤ ↑1 * ‖setToL1SCLM α E μ hT‖

Tactic:
refine
  ContinuousLinearMap.opNorm_extend_le (setToL1SCLM α E μ hT) (coeToLp α E ℝ)
    (simpleFunc.denseRange one_ne_top) fun x => le_of_eq ?_

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
⊢ ‖x‖ = ↑1 * ‖(coeToLp α E ℝ) x‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
⊢ ‖x‖ = ‖(coeToLp α E ℝ) x‖

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
⊢ ‖x‖ = ↑1 * ‖(coeToLp α E ℝ) x‖

Tactic:
rw [NNReal.coe_one, one_mul]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(simpleFunc E 1 μ)
⊢ ‖x‖ = ‖(coeToLp α E ℝ) x‖

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ ↑1 * ‖setToL1SCLM α E μ hT‖ = ‖setToL1SCLM α E μ hT‖

Tactic:
rw [NNReal.coe_one, one_mul]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
@[simp]
lemma zeroLocus_diff_singleton_zero (s : Set R) : zeroLocus (s \ {0}) = zeroLocus s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus (insert 0 s)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (s \ {0}) = zeroLocus s

Tactic:
rw [← zeroLocus_insert_zero, ← zeroLocus_insert_zero (s := s)]

Result:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 (s \ {0})) = zeroLocus (insert 0 s)
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem _root_.Ordinal.lift_omega (o : Ordinal.{u}) :
    Ordinal.lift.{v} (ω_ o) = ω_ (Ordinal.lift.{v} o)

Proof state:
o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (ω_ o) = ω_ (Ordinal.lift.{v, u} o)

Tactic:
simp [omega_eq_preOmega]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem zero_rpow {x : ℝ} (h : x ≠ 0) : (0 : ℝ) ^ x = 0

Proof state:
x : ℝ
h : x ≠ 0
⊢ 0 ^ x = 0

Tactic:
simp [rpow_def, *]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_inter_Ioo : Iio a ∩ Ioo b c = Ioo b (min a c)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Iio a ∩ Ioo b c = Ioo b (a ⊓ c)

Tactic:
rw [Set.inter_comm, Set.Ioo_inter_Iio, min_comm]

Result:
no goals