harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_ne_zero [Countable G] [SMulInvariantMeasure G α μ]
    (hμ : μ ≠ 0) (h : IsFundamentalDomain G s μ) : μ s ≠ 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ ∑' (i : G), μ (i • s) ≤ 0

Tactic:
simp_rw [measure_smul, hc, tsum_zero, le_refl]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ μ univ ≤ 0

Tactic:
rw [← measure_congr h.iUnion_smul_ae_eq]

Result:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ μ (⋃ g, g • s) ≤ 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : 0 < μ univ
⊢ μ s ≠ 0

Tactic:
contrapose! hc

Result:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ μ univ ≤ 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ μ (⋃ g, g • s) ≤ 0

Tactic:
refine le_trans (measure_iUnion_le _) ?_

Result:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ ∑' (i : G), μ (i • s) ≤ 0

Proof state:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
⊢ μ s ≠ 0

Tactic:
have hc := measure_univ_pos.mpr hμ

Result:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : 0 < μ univ
⊢ μ s ≠ 0
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@[to_additive]
lemma isCyclic_iff_exists_orderOf_eq_natCard [Finite α] :
    IsCyclic α ↔ ∃ g : α, orderOf g = Nat.card α

Proof state:
α : Type u_1
inst✝¹ : Group α
inst✝ : Finite α
⊢ IsCyclic α ↔ ∃ g, orderOf g = Nat.card α

Tactic:
simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_int_add (x : α) (y : ℤ) : round ((y : α) + x) = y + round x

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (↑y + x) = y + round x

Tactic:
rw [add_comm, round_add_int, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem join_map_eq_map_join {f : α → β} {x : Option (Option α)} :
    (x.map (Option.map f)).join = x.join.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x : Option (Option α)
⊢ (Option.map (Option.map f) x).join = Option.map f x.join

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem radius_leftInv_pos_of_radius_pos
    {p : FormalMultilinearSeries 𝕜 E F} {i : E ≃L[𝕜] F} {x : E}
    (hp : 0 < p.radius) (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    0 < (p.leftInv i x).radius

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ 0 < (p.rightInv i x).radius

Tactic:
exact radius_rightInv_pos_of_radius_pos hp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ 0 < (p.leftInv i x).radius

Tactic:
rw [leftInv_eq_rightInv _ _ _ h]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ 0 < (p.rightInv i x).radius
-- Mathlib/Analysis/Convex/Segment.lean
theorem Icc_subset_segment : Icc x y ⊆ [x -[𝕜] y]

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y : 𝕜
⊢ Icc x y ⊆ [x-[𝕜]y]

Tactic:
rintro z ⟨hxz, hyz⟩

Result:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x-[𝕜]y]

Proof state:
case intro.inr.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z

Tactic:
rw [smul_eq_mul, smul_eq_mul, ← mul_div_right_comm, ← mul_div_right_comm, ← add_div,
  div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub]

Result:
no goals

Proof state:
case intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : x < y
⊢ z ∈ [x-[𝕜]y]

Tactic:
rw [← sub_pos] at h

Result:
case intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ z ∈ [x-[𝕜]y]

Proof state:
case intro
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
⊢ z ∈ [x-[𝕜]y]

Tactic:
obtain rfl | h := (hxz.trans hyz).eq_or_lt

Result:
case intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x-[𝕜]x]

case intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x-[𝕜]y]

Proof state:
case intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ {x}

Tactic:
exact hyz.antisymm hxz

Result:
no goals

Proof state:
case intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ [x-[𝕜]x]

Tactic:
rw [segment_same]

Result:
case intro.inl
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x z : 𝕜
hxz : x ≤ z
hyz : z ≤ x
⊢ z ∈ {x}

Proof state:
case intro.inr.refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1

Tactic:
rw [← add_div, sub_add_sub_cancel, div_self h.ne']

Result:
no goals

Proof state:
case intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ z ∈ [x-[𝕜]y]

Tactic:
refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩

Result:
case intro.inr.refine_1
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ (y - z) / (y - x) + (z - x) / (y - x) = 1

case intro.inr.refine_2
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : 0 < y - x
⊢ ((y - z) / (y - x)) • x + ((z - x) / (y - x)) • y = z

Proof state:
case intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : x ≤ z
hyz : z ≤ y
h : x < y
⊢ z ∈ [x-[𝕜]y]

Tactic:
rw [← sub_nonneg] at hxz hyz

Result:
case intro.inr
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x y z : 𝕜
hxz : 0 ≤ z - x
hyz : 0 ≤ y - z
h : x < y
⊢ z ∈ [x-[𝕜]y]
-- Mathlib/Data/Multiset/Fintype.lean
@[simp] lemma map_toEnumFinset_fst (m : Multiset α) : m.toEnumFinset.val.map Prod.fst = m

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
⊢ count a (map Prod.fst m.toEnumFinset.val) = count a m

Tactic:
simp [count_map, ← Finset.filter_val, eq_comm (a := a)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
⊢ map Prod.fst m.toEnumFinset.val = m

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
⊢ count a (map Prod.fst m.toEnumFinset.val) = count a m
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem srange_eq_top_iff_surjective {N} [Mul N] {f : M →ₙ* N} :
    f.srange = (⊤ : Subsemigroup N) ↔ Function.Surjective f :=
  SetLike.ext'_iff.trans <| Iff.trans (by rw [coe_srange, coe_top]) Set.range_eq_univ

Proof state:
M : Type u_1
inst✝¹ : Mul M
N : Type u_5
inst✝ : Mul N
f : M →ₙ* N
⊢ ↑f.srange = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
rw [coe_srange, coe_top]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma powerset_inter (s t : Finset α) : (s ∩ t).powerset = s.powerset ⊼ t.powerset

Proof state:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u

Tactic:
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩

Result:
case h.refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t
⊢ s ∩ u ∩ (t ∩ u) = u

case h.refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t

Proof state:
case h.refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∩ w ⊆ s ∩ t

Tactic:
exact inter_subset_inter hv hw

Result:
no goals

Proof state:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset

Tactic:
simp only [mem_infs, mem_powerset, le_eq_subset, inf_eq_inter]

Result:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ⊆ s ∩ t ↔ ∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).powerset = s.powerset ⊼ t.powerset

Tactic:
ext u

Result:
case h
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ u ∈ (s ∩ t).powerset ↔ u ∈ s.powerset ⊼ t.powerset

Proof state:
case h.refine_2
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
⊢ (∃ a ⊆ s, ∃ b ⊆ t, a ∩ b = u) → u ⊆ s ∩ t

Tactic:
rintro ⟨v, hv, w, hw, rfl⟩

Result:
case h.refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
s t v : Finset α
hv : v ⊆ s
w : Finset α
hw : w ⊆ t
⊢ v ∩ w ⊆ s ∩ t

Proof state:
case h.refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t
⊢ s ∩ u ∩ (t ∩ u) = u

Tactic:
rwa [← inter_inter_distrib_right, inter_eq_right]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_of_subset_zero (h : s ⊆ 0) : gauge s = 0

Proof state:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
h : ∅ ⊆ 0
⊢ gauge ∅ = 0

case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
h : {0} ⊆ 0
⊢ gauge {0} = 0

Tactic:
exacts [gauge_empty, gauge_zero']

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : s ⊆ 0
⊢ gauge s = 0

Tactic:
obtain rfl | rfl := subset_singleton_iff_eq.1 h

Result:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
h : ∅ ⊆ 0
⊢ gauge ∅ = 0

case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
h : {0} ⊆ 0
⊢ gauge {0} = 0
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma range_id : range (𝟙 F) = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
⊢ range (𝟙 F) = ⊤

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
@[simp]
lemma tsum_one : ∑' _ : α, (1 : ℝ≥0∞) = ENat.card α

Proof state:
α : Type u_1
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)

Tactic:
simpa [encard_univ] using tsum_set_one univ

Result:
no goals

Proof state:
α : Type u_1
⊢ ∑' (x : α), 1 = ↑(ENat.card α)

Tactic:
rw [← tsum_univ]

Result:
α : Type u_1
⊢ ∑' (x : ↑univ), 1 = ↑(ENat.card α)
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.mem_affineSpan {x y z : P} (h : Wbtw R x y z) : y ∈ line[R, x, z]

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
⊢ (lineMap x z) r ∈ affineSpan R {x, z}

Tactic:
exact lineMap_mem_affineSpan_pair _ _ _

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ y ∈ affineSpan R {x, z}

Tactic:
rcases h with ⟨r, ⟨-, rfl⟩⟩

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
r : R
⊢ (lineMap x z) r ∈ affineSpan R {x, z}
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_support (f : R[X]) : f.eraseLead.support = f.support.erase f.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.support = f.support.erase f.natDegree

Tactic:
simp only [eraseLead, support_erase]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem obj_η_app (n : M) (X : C) [F.Monoidal] :
    (F.obj n).map ((η F).app X) = (μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X ≫ (ε F).app X) =
    ((μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫ (F.obj n).map ((ε F).app X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X) = (μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X

Tactic:
rw [← cancel_mono ((F.obj n).map ((ε F).app X)), ← Functor.map_comp]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X ≫ (ε F).app X) =
    ((μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫ (F.obj n).map ((ε F).app X)
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upcrossingsBefore_bot [Preorder ι] [OrderBot ι] [InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
    {ω : Ω} : upcrossingsBefore a b f ⊥ ω = ⊥

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : OrderBot ι
inst✝ : InfSet ι
a b : ℝ
f : ι → Ω → ℝ
ω : Ω
⊢ upcrossingsBefore a b f ⊥ ω = ⊥

Tactic:
simp [upcrossingsBefore]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem inv_mul (χ : MulChar R R') : χ⁻¹ * χ = 1

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ 1 = 1 ↑x

Tactic:
rw [one_apply_coe]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ Ring.inverse (χ ↑x) * χ ↑x = 1 ↑x

Tactic:
simp only [Ring.inverse_mul_cancel _ (IsUnit.map χ x.isUnit)]

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ 1 = 1 ↑x

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ⁻¹ * χ = 1

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ (χ⁻¹ * χ) ↑x = 1 ↑x

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ (χ⁻¹ * χ) ↑x = 1 ↑x

Tactic:
rw [coeToFun_mul, Pi.mul_apply, inv_apply_eq_inv]

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ Ring.inverse (χ ↑x) * χ ↑x = 1 ↑x
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_eq_top_iff {I : Ideal S} : I.comap f = ⊤ ↔ I = ⊤ :=
  ⟨fun h => I.eq_top_iff_one.mpr (map_one f ▸ mem_comap.mp ((I.comap f).eq_top_iff_one.mp h)),
    fun h => by rw [h, comap_top]⟩

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
I : Ideal S
h : I = ⊤
⊢ comap f I = ⊤

Tactic:
rw [h, comap_top]

Result:
no goals
-- Mathlib/Data/Semiquot.lean
theorem ext_s {q₁ q₂ : Semiquot α} : q₁ = q₂ ↔ q₁.s = q₂.s

Proof state:
α : Type u_1
q₁ q₂ : Semiquot α
⊢ q₁ = q₂ ↔ q₁.s = q₂.s

Tactic:
refine ⟨congr_arg _, fun h => ?_⟩

Result:
α : Type u_1
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂

Proof state:
case mk'.mk'.h.e_3
α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ HEq v₁ v₂

Tactic:
exact Subsingleton.helim (congrArg Trunc (congrArg Set.Elem h)) v₁ v₂

Result:
no goals

Proof state:
case mk'
α : Type u_1
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂

Tactic:
obtain ⟨_, v₂⟩ := q₂

Result:
case mk'.mk'
α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }

Proof state:
α : Type u_1
q₁ q₂ : Semiquot α
h : q₁.s = q₂.s
⊢ q₁ = q₂

Tactic:
obtain ⟨_, v₁⟩ := q₁

Result:
case mk'
α : Type u_1
q₂ : Semiquot α
s✝ : Set α
v₁ : Trunc ↑s✝
h : { s := s✝, val := v₁ }.s = q₂.s
⊢ { s := s✝, val := v₁ } = q₂

Proof state:
case mk'.mk'
α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ { s := s✝¹, val := v₁ } = { s := s✝, val := v₂ }

Tactic:
congr

Result:
case mk'.mk'.h.e_3
α : Type u_1
s✝¹ : Set α
v₁ : Trunc ↑s✝¹
s✝ : Set α
v₂ : Trunc ↑s✝
h : { s := s✝¹, val := v₁ }.s = { s := s✝, val := v₂ }.s
⊢ HEq v₁ v₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = True) : (dite c t e) = t (of_eq_true h)

Proof state:
α : Sort u
c : Prop
x✝ : Decidable c
t : c → α
e : ¬c → α
h : c = True
⊢ dite c t e = t ⋯

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
lemma toNNReal_natCast_eq_toNNReal (n : ℕ) :
    (n : ℝ≥0∞).toNNReal = (n : ℝ).toNNReal

Proof state:
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
⊢ (↑n).toNNReal = (↑n).toNNReal

Tactic:
rw [Real.toNNReal_of_nonneg (by positivity), ENNReal.toNNReal_natCast, mk_natCast]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem sigmaFiniteTrim_mono {m m₂ m0 : MeasurableSpace α} {μ : Measure α} (hm : m ≤ m0)
    (hm₂ : m₂ ≤ m) [SigmaFinite (μ.trim (hm₂.trans hm))] : SigmaFinite (μ.trim hm)

Proof state:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ (μ.trim hm) (spanningSets (μ.trim ⋯) i) = ((μ.trim hm).trim hm₂) (spanningSets (μ.trim ⋯) i)

Tactic:
rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]

Result:
no goals

Proof state:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ (μ.trim hm) (spanningSets (μ.trim ⋯) i) < ⊤

Tactic:
calc
  (μ.trim hm) (spanningSets (μ.trim (hm₂.trans hm)) i) =
      ((μ.trim hm).trim hm₂) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
    rw [@trim_measurableSet_eq α m₂ m (μ.trim hm) _ hm₂ (measurableSet_spanningSets _ _)]
  _ = (μ.trim (hm₂.trans hm)) (spanningSets (μ.trim (hm₂.trans hm)) i) := by
    rw [@trim_trim _ _ μ _ _ hm₂ hm]
  _ < ∞ := measure_spanningSets_lt_top _ _

Result:
no goals

Proof state:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ (μ.trim hm).FiniteSpanningSetsIn Set.univ

Tactic:
refine
  { set := spanningSets (μ.trim (hm₂.trans hm))
    set_mem := fun _ => Set.mem_univ _
    finite := fun i => ?_
    spanning := iUnion_spanningSets _ }

Result:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ (μ.trim hm) (spanningSets (μ.trim ⋯) i) < ⊤

Proof state:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ SigmaFinite (μ.trim hm)

Tactic:
refine ⟨⟨?_⟩⟩

Result:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ (μ.trim hm).FiniteSpanningSetsIn Set.univ

Proof state:
α : Type u_1
m m₂ m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hm₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim ⋯)
i : ℕ
⊢ ((μ.trim hm).trim hm₂) (spanningSets (μ.trim ⋯) i) = (μ.trim ⋯) (spanningSets (μ.trim ⋯) i)

Tactic:
rw [@trim_trim _ _ μ _ _ hm₂ hm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Properties.lean
/-- A locally finite preconnected infinite graph has at least one end. -/
lemma nonempty_ends_of_infinite [LocallyFinite G] [Fact G.Preconnected] [Infinite V] :
    G.end.Nonempty

Proof state:
V : Type
G : SimpleGraph V
inst✝² : G.LocallyFinite
inst✝¹ : Fact G.Preconnected
inst✝ : Infinite V
⊢ G.end.Nonempty

Tactic:
classical
apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor

Result:
no goals

Proof state:
V : Type
G : SimpleGraph V
inst✝² : G.LocallyFinite
inst✝¹ : Fact G.Preconnected
inst✝ : Infinite V
⊢ G.end.Nonempty

Tactic:
apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor

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

Proof state:
w : Nat
x : BitVec w
⊢ x <<< 0 = x

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
⊢ (x <<< 0).toNat = x.toNat

Proof state:
case a
w : Nat
x : BitVec w
⊢ (x <<< 0).toNat = x.toNat

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem norm_embedding_eq (w : InfinitePlace K) (x : K) :
    ‖(embedding w) x‖ = w x

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = (mk w.embedding) x

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = w x

Tactic:
nth_rewrite 2 [← mk_embedding w]

Result:
K : Type u_2
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖w.embedding x‖ = (mk w.embedding) x
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernel.lift_zero {W : C} {h} : kernel.lift f (0 : W ⟶ X) h = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : 0 ≫ f = 0
⊢ lift f 0 h = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : 0 ≫ f = 0
⊢ lift f 0 h ≫ equalizer.ι f 0 = 0 ≫ equalizer.ι f 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : 0 ≫ f = 0
⊢ lift f 0 h ≫ equalizer.ι f 0 = 0 ≫ equalizer.ι f 0

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/Int.lean
lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n

Proof state:
n : ℕ
Hn : (Finset.range n).Nonempty
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
Hn : n ≠ 0
⊢ 0 < harmonic n

Tactic:
unfold harmonic

Result:
n : ℕ
Hn : n ≠ 0
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹

Proof state:
n : ℕ
Hn : n ≠ 0
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹

Tactic:
rw [← Finset.nonempty_range_iff] at Hn

Result:
n : ℕ
Hn : (Finset.range n).Nonempty
⊢ 0 < ∑ i ∈ Finset.range n, (↑(i + 1))⁻¹