harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Sups.lean
theorem upperClosure_sups [SemilatticeSup α] (s t : Set α) :
    upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t

Proof state:
case a.h
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
constructor

Result:
case a.h.mp
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a

case a.h.mpr
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ ((∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a) → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_2) ∧ a_2 ≤ a

Proof state:
case a.h.mp
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) → (∃ a_2 ∈ s, a_2 ≤ a) ∧ ∃ a_2 ∈ t, a_2 ≤ a

Tactic:
rintro ⟨_, ⟨b, hb, c, hc, rfl⟩, ha⟩

Result:
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Proof state:
case a.h.mpr
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ ((∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a) → ∃ a_2, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_2) ∧ a_2 ≤ a

Tactic:
rintro ⟨⟨b, hb, hab⟩, c, hc, hac⟩

Result:
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
⊢ upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t

Tactic:
ext a

Result:
case a.h
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)

Proof state:
case a.h.mp.intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
c : α
hc : c ∈ t
ha : b ⊔ c ≤ a
⊢ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a

Tactic:
exact ⟨⟨b, hb, le_sup_left.trans ha⟩, c, hc, le_sup_right.trans ha⟩

Result:
no goals

Proof state:
case a.h.mpr.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a b : α
hb : b ∈ s
hab : b ≤ a
c : α
hc : c ∈ t
hac : c ≤ a
⊢ ∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a

Tactic:
exact ⟨_, ⟨b, hb, c, hc, rfl⟩, sup_le hab hac⟩

Result:
no goals

Proof state:
case a.h
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ a ∈ ↑(upperClosure (s ⊻ t)) ↔ a ∈ ↑(upperClosure s ⊔ upperClosure t)

Tactic:
simp only [SetLike.mem_coe, mem_upperClosure, Set.mem_sups, exists_and_left, exists_prop,
  UpperSet.coe_sup, Set.mem_inter_iff]

Result:
case a.h
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ (∃ a_1, (∃ a ∈ s, ∃ b ∈ t, a ⊔ b = a_1) ∧ a_1 ≤ a) ↔ (∃ a_1 ∈ s, a_1 ≤ a) ∧ ∃ a_1 ∈ t, a_1 ≤ a
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem mem_source_at : (⟨b, a⟩ : Z.TotalSpace) ∈ (Z.localTrivAt b).source

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
⊢ { proj := b, snd := a } ∈ (Z.localTrivAt b).source

Tactic:
rw [localTrivAt, mem_localTriv_source]

Result:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
⊢ { proj := b, snd := a }.proj ∈ Z.baseSet (Z.indexAt b)

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
⊢ { proj := b, snd := a }.proj ∈ Z.baseSet (Z.indexAt b)

Tactic:
exact Z.mem_baseSet_at b

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem isBasis_restrict_iff' : (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X)

Tactic:
intro hXR

Result:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R

Tactic:
exact fun h ↦ h.subset.trans hXR

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I (X ∩ M.E) ∧ X ⊆ R

Tactic:
rw [isBasis_iff_isBasis'_subset_ground, isBasis'_restrict_iff, restrict_ground_eq,
  and_congr_left_iff, ← isBasis'_iff_isBasis_inter_ground]

Result:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X)

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X

Tactic:
rw [inter_eq_self_of_subset_left hXR, and_iff_left_iff_imp]

Result:
α : Type u_1
M : Matroid α
R I X : Set α
hXR : X ⊆ R
⊢ M.IsBasis' I X → I ⊆ R
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_union {f : α → E} {s t : Set α} (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ)
    (hsμ : μ s ≠ ∞) (htμ : μ t ≠ ∞) (hfs : IntegrableOn f s μ) (hft : IntegrableOn f t μ) :
    ⨍ x in s ∪ t, f x ∂μ =
      ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ x in s, f x ∂μ +
        ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ x in t, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this✝ : Fact (μ s < ⊤)
this : Fact (μ t < ⊤)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ +
      ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
rw [restrict_union₀ hd ht, average_add_measure hfs hft, restrict_apply_univ, restrict_apply_univ]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this : Fact (μ s < ⊤)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ +
      ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
haveI := Fact.mk htμ.lt_top

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this✝ : Fact (μ s < ⊤)
this : Fact (μ t < ⊤)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ +
      ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ +
      ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ

Tactic:
haveI := Fact.mk hsμ.lt_top

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ⊤
htμ : μ t ≠ ⊤
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this : Fact (μ s < ⊤)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    ((μ s).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in s, f x ∂μ +
      ((μ t).toReal / ((μ s).toReal + (μ t).toReal)) • ⨍ (x : α) in t, f x ∂μ
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_eq_zero_iff {θ : Angle} : θ.toReal = 0 ↔ θ = 0

Proof state:
θ : Angle
⊢ θ.toReal = 0 ↔ θ = 0

Tactic:
nth_rw 1 [← toReal_zero]

Result:
θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0

Proof state:
θ : Angle
⊢ θ.toReal = toReal 0 ↔ θ = 0

Tactic:
exact toReal_inj

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_singleton {f : β → α} {b : β} : ⨆ x ∈ (singleton b : Set β), f x = f b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
b : β
⊢ ⨆ x ∈ {b}, f x = f b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem map_aeval {B : Type*} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) :
    φ (aeval g p) = eval₂Hom (φ.comp (algebraMap R S₁)) (fun i => φ (g i)) p

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (eval₂Hom (φ.comp (algebraMap R S₁)) fun i => φ (g i)) p

Tactic:
rw [← comp_eval₂Hom]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (φ.comp (eval₂Hom (algebraMap R S₁) g)) p

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (φ.comp (eval₂Hom (algebraMap R S₁) g)) p

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Cocardinal.lean
@[simp] lemma cocardinal_aleph0_eq_cofinite :
    cocardinal (α := α) isRegular_aleph0 = cofinite

Proof state:
α : Type u
⊢ cocardinal α isRegular_aleph0 = cofinite

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : log b r = 0

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ log b r = 0

Tactic:
rw [log_of_one_le_right _ h, Nat.log_of_left_le_one hb, Int.ofNat_zero]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0

Tactic:
rw [log_of_right_le_one _ h, Nat.clog_of_left_le_one hb, Int.ofNat_zero, neg_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ log b r = 0

Tactic:
rcases le_total 1 r with h | h

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : 1 ≤ r
⊢ log b r = 0

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
h : r ≤ 1
⊢ log b r = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_rotateRight {x : BitVec w} {r i : Nat} (h : i < w) :
    (x.rotateRight r)[i] = if h' : i < w - (r % w) then x[(r % w) + i] else x[(i - (w - (r % w)))]

Proof state:
w : Nat
x : BitVec w
r i : Nat
h : i < w
⊢ (x.rotateRight r).getLsbD i = if h : i < w - r % w then x.getLsbD (r % w + i) else x.getLsbD (i - (w - r % w))

Tactic:
simp [getLsbD_rotateRight, h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
h : i < w
⊢ (x.rotateRight r)[i] = if h' : i < w - r % w then x[r % w + i] else x[i - (w - r % w)]

Tactic:
simp only [← BitVec.getLsbD_eq_getElem]

Result:
w : Nat
x : BitVec w
r i : Nat
h : i < w
⊢ (x.rotateRight r).getLsbD i = if h : i < w - r % w then x.getLsbD (r % w + i) else x.getLsbD (i - (w - r % w))
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- We have that `𝓞 K ⧸ Ideal.span {ζ - 1}` has cardinality equal to the norm of `ζ - 1`.

See the results below to compute this norm in various cases. -/
lemma card_quotient_toInteger_sub_one [NumberField K] {k : ℕ+} (hk : 1 < k)
    (hζ : IsPrimitiveRoot ζ k) :
    Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) =
      (Algebra.norm ℤ (hζ.toInteger - 1)).natAbs

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
⊢ Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs

Tactic:
have := hζ.finite_quotient_toInteger_sub_one hk

Result:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
this : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
⊢ Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
this : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
⊢ Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs

Tactic:
let _ := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})

Result:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
this : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
x✝ : Fintype (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
⊢ Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs

Proof state:
K : Type u
inst✝¹ : Field K
ζ : K
inst✝ : NumberField K
k : ℕ+
hk : 1 < k
hζ : IsPrimitiveRoot ζ ↑k
this : Finite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
x✝ : Fintype (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1})
⊢ Nat.card (𝓞 K ⧸ Ideal.span {hζ.toInteger - 1}) = ((Algebra.norm ℤ) (hζ.toInteger - 1)).natAbs

Tactic:
rw [← Submodule.cardQuot_apply, ← Ideal.absNorm_apply, Ideal.absNorm_span_singleton]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem subsemigroupMap_surjective (f : M →ₙ* N) (M' : Subsemigroup M) :
    Function.Surjective (f.subsemigroupMap M')

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
M' : Subsemigroup M
⊢ Function.Surjective ⇑(f.subsemigroupMap M')

Tactic:
rintro ⟨_, x, hx, rfl⟩

Result:
case mk.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
M' : Subsemigroup M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, (f.subsemigroupMap M') a = ⟨f x, ⋯⟩

Proof state:
case mk.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
M' : Subsemigroup M
x : M
hx : x ∈ ↑M'
⊢ ∃ a, (f.subsemigroupMap M') a = ⟨f x, ⋯⟩

Tactic:
exact ⟨⟨x, hx⟩, rfl⟩

Result:
no goals
-- Mathlib/Data/Multiset/Interval.lean
theorem card_Iic : (Finset.Iic s).card = ∏ i ∈ s.toFinset, (s.count i + 1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ #(Finset.Iic s) = ∏ i ∈ s.toFinset, (count i s + 1)

Tactic:
simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem eq_compl_comm : x = yᶜ ↔ y = xᶜ

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x = yᶜ ↔ y = xᶜ

Tactic:
rw [eq_comm, compl_eq_iff_isCompl, eq_compl_iff_isCompl]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem dual_isBase_iff (hB : B ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ (M✶.Indep B ∧ ∀ ⦃t : Set α⦄, M✶.Indep t → B ⊆ t → B = t) ↔
    (B ⊆ M.E ∧ ∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) → B ⊆ t → B = t

Tactic:
simp [dual_indep_iff_exists', hB]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B)

Tactic:
rw [isBase_compl_iff_maximal_disjoint_isBase, isBase_iff_maximal_indep, maximal_subset_iff,
  maximal_subset_iff]

Result:
α : Type u_1
M : Matroid α
B : Set α
hB : autoParam (B ⊆ M.E) _auto✝
⊢ (M✶.Indep B ∧ ∀ ⦃t : Set α⦄, M✶.Indep t → B ⊆ t → B = t) ↔
    (B ⊆ M.E ∧ ∃ B_1, M.IsBase B_1 ∧ Disjoint B B_1) ∧
      ∀ ⦃t : Set α⦄, (t ⊆ M.E ∧ ∃ B, M.IsBase B ∧ Disjoint t B) → B ⊆ t → B = t
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma lt_mul_left [MulPosStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < b * a

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a b : M₀
inst✝ : MulPosStrictMono M₀
ha : 0 < a
hb : 1 < b
⊢ a < b * a

Tactic:
simpa using mul_lt_mul_of_pos_right hb ha

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_antitoneOn_Ioi :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Ioi 0)

Proof state:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
⊢ AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)

Tactic:
convert sub_inv_antitoneOn_Ioi

Result:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
x✝ : α
⊢ x✝ = x✝ - 0
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem edist_mul_mul_le (a₁ a₂ b₁ b₂ : E) :
    edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

Tactic:
apply nndist_mul_mul_le

Result:
no goals

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ ↑(nndist (a₁ * a₂) (b₁ * b₂)) ≤ ↑(nndist a₁ b₁) + ↑(nndist a₂ b₂)

Tactic:
norm_cast

Result:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

Tactic:
simp only [edist_nndist]

Result:
E : Type u_2
inst✝ : SeminormedCommGroup E
a₁ a₂ b₁ b₂ : E
⊢ ↑(nndist (a₁ * a₂) (b₁ * b₂)) ≤ ↑(nndist a₁ b₁) + ↑(nndist a₂ b₂)
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.iSup_lintegral_eq_of_countably_generated [Nonempty ι] [l.NeBot]
    [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ) {f : α → ℝ≥0∞}
    (hfm : AEMeasurable f μ) : ⨆ i : ι, ∫⁻ x in φ i, f x ∂μ = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ

Tactic:
exact (this.eventually_const_lt hw).exists

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
⊢ ⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
have := hφ.lintegral_tendsto_of_countably_generated hfm

Result:
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ ⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Proof state:
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
⊢ ⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt
  (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => ?_

Result:
α : Type u_1
ι : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : Nonempty ι
inst✝¹ : l.NeBot
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
this : Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
w : ℝ≥0∞
hw : w < ∫⁻ (x : α), f x ∂μ
⊢ ∃ i, w < ∫⁻ (x : α) in φ i, f x ∂μ
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma lift_f (p q : ℤ) (hpq : p + 1 = q) :
    (lift φ α β eq).f p = α.1.v p q hpq ≫
      (inl φ).v q p (by omega) + β.v p p (add_zero p) ≫ (inr φ).f p

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ (lift φ α β eq).f p = (↑α).v p q hpq ≫ (inl φ).v q p ⋯ + β.v p p ⋯ ≫ (inr φ).f p

Tactic:
simp [ext_to_iff _ _ _ hpq]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.228384, u_1} C
inst✝³ : Category.{?u.228388, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
@[reassoc, simp]
lemma map₂_hom_inv {f g : a ⟶ b} (η : f ≅ g) :
    F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)

Tactic:
rw [← F.map₂_comp, Iso.hom_inv_id, F.map₂_id]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_apply (hs : MeasurableSet s) : count s = s.encard

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ count s = ↑s.encard

Tactic:
simp [count, hs, ← tsum_subtype, Set.encard]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
@[simp]
lemma algebraTensorAlgEquiv_symm_X (s : σ) :
    (algebraTensorAlgEquiv R A).symm (X s) = 1 ⊗ₜ X s

Proof state:
R : Type u
inst✝² : CommSemiring R
σ : Type u_1
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : σ
⊢ (algebraTensorAlgEquiv R A).symm (X s) = 1 ⊗ₜ[R] X s

Tactic:
simp [algebraTensorAlgEquiv]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f : R ⟶ Γ.obj (op X)}
    {β : X ⟶ Spec.locallyRingedSpaceObj R}
    (w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base)
    (h :
      ∀ r : R,
        f ≫ X.presheaf.map (homOfLE le_top : (Opens.map β.base).obj (basicOpen r) ⟶ _).op =
          toOpen R (basicOpen r) ≫ β.c.app (op (basicOpen r))) :
    X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        toOpen (↑(Γ.obj (op X))) ((Opens.comap (PrimeSpectrum.comap (CommRingCat.Hom.hom f))) U) ≫
          X.toΓSpec.c.app (op ((Opens.map (Spec.locallyRingedSpaceMap f).base).obj (unop (op U))))) ≫
      X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Tactic:
rw [Category.assoc]

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      (toOpen (↑(Γ.obj (op X))) ((Opens.comap (PrimeSpectrum.comap (CommRingCat.Hom.hom f))) U) ≫
          X.toΓSpec.c.app (op ((Opens.map (Spec.locallyRingedSpaceMap f).base).obj (unop (op U))))) ≫
        X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)