harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_insertEntryIfNew' [BEq α] [PartialEquivBEq α]
    {l : List ((a : α) × β a)} {k a : α} {v : β k} (h₁ : containsKey a (insertEntryIfNew k v l))
    (h₂ : ¬((k == a) ∧ containsKey k l = false)) : containsKey a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : (k == a) = false ∨ containsKey k l = true
⊢ containsKey a l = true

Tactic:
rcases h₂ with h₂|h₂

Result:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : (k == a) = false
⊢ containsKey a l = true

case inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : containsKey k l = true
⊢ containsKey a l = true

Proof state:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : (k == a) = false
⊢ containsKey a l = true

Tactic:
rwa [containsKey_insertEntryIfNew, h₂, Bool.false_or] at h₁

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : ¬((k == a) = true ∧ containsKey k l = false)
⊢ containsKey a l = true

Tactic:
rw [Decidable.not_and_iff_or_not, Bool.not_eq_true, Bool.not_eq_false] at h₂

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : (k == a) = false ∨ containsKey k l = true
⊢ containsKey a l = true

Proof state:
case inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (insertEntryIfNew k v l) = true
h₂ : containsKey k l = true
⊢ containsKey a l = true

Tactic:
rwa [insertEntryIfNew_of_containsKey h₂] at h₁

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem integral_pos : 0 < ∫ x, f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ 0 < μ (ball c f.rOut)

Tactic:
exact measure_ball_pos μ c f.rOut_pos

Result:
no goals

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ 0 < μ (support ↑f)

Tactic:
rw [f.support_eq]

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ 0 < μ (ball c f.rOut)

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ 0 < ∫ (x : E), ↑f x ∂μ

Tactic:
refine (integral_pos_iff_support_of_nonneg f.nonneg' f.integrable).mpr ?_

Result:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ 0 < μ (support ↑f)
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem sigmaFinite_of_countable {S : Set (Set α)} (hc : S.Countable) (hμ : ∀ s ∈ S, μ s < ∞)
    (hU : ⋃₀ S = univ) : SigmaFinite μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ : ∀ s ∈ S, μ s < ⊤
hU : ⋃₀ S = univ
⊢ SigmaFinite μ

Tactic:
obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → Set α, (∀ n, μ (s n) < ∞) ∧ ⋃ n, s n = univ :=
  (@exists_seq_cover_iff_countable _ (fun x => μ x < ∞) ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ✝ : ∀ s ∈ S, μ s < ⊤
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), μ (s n) < ⊤
hs : ⋃ n, s n = univ
⊢ SigmaFinite μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ : ∀ s ∈ S, μ s < ⊤
hU : ⋃₀ S = univ
⊢ (fun x => μ x < ⊤) ∅

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ✝ : ∀ s ∈ S, μ s < ⊤
hU : ⋃₀ S = univ
s : ℕ → Set α
hμ : ∀ (n : ℕ), μ (s n) < ⊤
hs : ⋃ n, s n = univ
⊢ SigmaFinite μ

Tactic:
exact ⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean
theorem FarFromTriangleFree.nonpos (h₀ : G.FarFromTriangleFree ε) (h₁ : G.CliqueFree 3) :
    ε ≤ 0

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H => H.CliqueFree 3) G → ε * ↑(Fintype.card α ^ 2) ≤ 0
⊢ ε ≤ 0

Tactic:
exact nonpos_of_mul_nonpos_left (this h₁) (cast_pos.2 <| sq_pos_of_pos Fintype.card_pos)

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
⊢ ε ≤ 0

Tactic:
have := h₀ (empty_subset _)

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H => H.CliqueFree 3) (G.deleteEdges ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#∅)
⊢ ε ≤ 0

Proof state:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H => H.CliqueFree 3) (G.deleteEdges ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#∅)
⊢ ε ≤ 0

Tactic:
rw [coe_empty, Finset.card_empty, cast_zero, deleteEdges_empty] at this

Result:
α : Type u_1
𝕜 : Type u_3
inst✝³ : LinearOrderedField 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝² : Fintype α
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty α
h₀ : G.FarFromTriangleFree ε
h₁ : G.CliqueFree 3
this : (fun H => H.CliqueFree 3) G → ε * ↑(Fintype.card α ^ 2) ≤ 0
⊢ ε ≤ 0
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_le (a b c : α) : |a - c| ≤ |a - b| + |b - c| :=
  calc
    |a - c| = |a - b + (b - c)|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| = |a - b + (b - c)|

Tactic:
rw [sub_add_sub_cancel]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_eq_iSup_norm : ‖f‖ = ⨆ x : α, ‖f x‖

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ = ⨆ x, ‖f x‖

Tactic:
simp_rw [norm_def, dist_eq_iSup, coe_zero, Pi.zero_apply, dist_zero_right]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem Scheme.ι_image_homOfLE_le_ι_image {U V : X.Opens} (e : U ≤ V) (W : Opens V) :
    U.ι ''ᵁ (X.homOfLE e ⁻¹ᵁ W) ≤ V.ι ''ᵁ W

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
a✝ : ↑↑(↑U).toPresheafedSpace
h : a✝ ∈ ⇑(ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) ⁻¹' ↑W
⊢ a✝ ∈
    (fun a => (ConcreteCategory.hom (Hom.toLRSHom U.ι).base) a) ⁻¹'
      ((fun a => (ConcreteCategory.hom (Hom.toLRSHom V.ι).base) a) '' ↑W)

Tactic:
exact ⟨_, h, rfl⟩

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ U.ι ''ᵁ X.homOfLE e ⁻¹ᵁ W ≤ V.ι ''ᵁ W

Tactic:
simp only [← SetLike.coe_subset_coe, IsOpenMap.coe_functor_obj, Set.image_subset_iff,
  Scheme.homOfLE_base, Opens.map_coe, Opens.inclusion'_hom_apply]

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ ⇑(ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) ⁻¹' ↑W ⊆
    (fun a => (ConcreteCategory.hom (Hom.toLRSHom U.ι).base) a) ⁻¹'
      ((fun a => (ConcreteCategory.hom (Hom.toLRSHom V.ι).base) a) '' ↑W)

Proof state:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
⊢ ⇑(ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) ⁻¹' ↑W ⊆
    (fun a => (ConcreteCategory.hom (Hom.toLRSHom U.ι).base) a) ⁻¹'
      ((fun a => (ConcreteCategory.hom (Hom.toLRSHom V.ι).base) a) '' ↑W)

Tactic:
rintro _ h

Result:
X : Scheme
U V : X.Opens
e : U ≤ V
W : (↑V).Opens
a✝ : ↑↑(↑U).toPresheafedSpace
h : a✝ ∈ ⇑(ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) ⁻¹' ↑W
⊢ a✝ ∈
    (fun a => (ConcreteCategory.hom (Hom.toLRSHom U.ι).base) a) ⁻¹'
      ((fun a => (ConcreteCategory.hom (Hom.toLRSHom V.ι).base) a) '' ↑W)
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma setIntegral_compProd [SFinite μ] [IsSFiniteKernel κ] {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t)
    {f : α × β → E} (hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ))  :
    ∫ x in s ×ˢ t, f x ∂(μ ⊗ₘ κ) = ∫ a in s, ∫ b in t, f (a, b) ∂(κ a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
rw [compProd, ProbabilityTheory.setIntegral_compProd hs ht hf]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝³ : SFinite μ
inst✝² : IsSFiniteKernel κ
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set α
hs : MeasurableSet s
t : Set β
ht : MeasurableSet t
f : α × β → E
hf : IntegrableOn f (s ×ˢ t) (μ ⊗ₘ κ)
⊢ ∫ (x : α) in s, ∫ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () =
    ∫ (a : α) in s, ∫ (b : β) in t, f (a, b) ∂κ a ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
lemma basicOpen_eq_bot_iff_forall_evaluation_eq_zero (f : X.presheaf.obj (op U)) :
    X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : U), X.evaluation x f = 0

Proof state:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
f : ↑(X.presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (x : ↥U), (ConcreteCategory.hom (X.evaluation x)) f = 0

Tactic:
simp only [evaluation_eq_zero_iff_not_mem_basicOpen, Subtype.forall]

Result:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
f : ↑(X.presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ a ∈ U, a ∉ X.toRingedSpace.basicOpen f

Proof state:
X : LocallyRingedSpace
U : Opens ↑X.toTopCat
f : ↑(X.presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ a ∈ U, a ∉ X.toRingedSpace.basicOpen f

Tactic:
exact ⟨fun h ↦ h ▸ fun a _ hc ↦ hc,
  fun h ↦ eq_bot_iff.mpr <| fun a ha ↦ h a (X.toRingedSpace.basicOpen_le f ha) ha⟩

Result:
no goals
-- Mathlib/Condensed/Light/Epi.lean
lemma epi_iff_locallySurjective_on_lightProfinite : Epi f ↔
    ∀ (S : LightProfinite) (y : Y.val.obj ⟨S⟩),
      (∃ (S' : LightProfinite) (φ : S' ⟶ S) (_ : Function.Surjective φ) (x : X.val.obj ⟨S'⟩),
        f.val.app ⟨S'⟩ x = Y.val.map ⟨φ⟩ y)

Proof state:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ Epi f ↔
    ∀ (S : LightProfinite) (y : ↑(Y.val.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

Tactic:
rw [← isLocallySurjective_iff_epi']

Result:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ↑(Y.val.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

Proof state:
R : Type u
inst✝ : Ring R
X Y : LightCondMod R
f : X ⟶ Y
⊢ IsLocallySurjective f ↔
    ∀ (S : LightProfinite) (y : ↑(Y.val.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom φ)),
          ∃ x,
            (ConcreteCategory.hom (f.val.app (Opposite.op S'))) x = (ConcreteCategory.hom (Y.val.map (Opposite.op φ))) y

Tactic:
exact LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite _ f

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem not_mem_sdiff_of_mem_right (h : a ∈ t) : a ∉ s \ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ a ∉ s \ t

Tactic:
simp only [mem_sdiff, h, not_true, not_false_iff, and_false]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem toIntermediateField_toSubalgebra (S : IntermediateField K L) :
    (S.toSubalgebra.toIntermediateField fun _ => S.inv_mem) = S

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ S.toIntermediateField ⋯ ↔ x✝ ∈ S

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
⊢ S.toIntermediateField ⋯ = S

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
x✝ : L
⊢ x✝ ∈ S.toIntermediateField ⋯ ↔ x✝ ∈ S
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_symm_comp (α : R₁ ⟶ R₂) (β : R₂ ⟶ R₃) :
    (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α =
      (conjugateEquiv adj₁ adj₃).symm (α ≫ β)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β

Tactic:
simp only [Equiv.apply_symm_apply]

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₂ adj₃).symm β ≫ (conjugateEquiv adj₁ adj₂).symm α = (conjugateEquiv adj₁ adj₃).symm (α ≫ β)

Tactic:
rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]

Result:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : R₁ ⟶ R₂
β : R₂ ⟶ R₃
⊢ (conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α) ≫
      (conjugateEquiv adj₂ adj₃) ((conjugateEquiv adj₂ adj₃).symm β) =
    α ≫ β
-- Mathlib/Data/Set/Image.lean
theorem disjoint_image_image {f : β → α} {g : γ → α} {s : Set β} {t : Set γ}
    (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) : Disjoint (f '' s) (g '' t) :=
  disjoint_iff_inf_le.mpr <| by rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c
⊢ f '' s ⊓ g '' t ≤ ⊥

Tactic:
rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥

Tactic:
exact h b hb c hc eq

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_succ_right_eq_insert_Ico (h : a ≤ b) : Ico a (b + 1) = insert b (Ico a b)

Proof state:
a b : ℕ
h : a ≤ b
⊢ Ico a (b + 1) = insert b (Ico a b)

Tactic:
rw [Ico_succ_right, ← Ico_insert_right h]

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem one_mul (s : UpperSet α) : 1 * s = s :=
  SetLike.coe_injective <|
    (subset_mul_right _ left_mem_Ici).antisymm' <| by
      rw [← smul_eq_mul, ← Set.iUnion_smul_set]
      exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s : UpperSet α
⊢ ⋃ a ∈ Set.Ici 1, a • ↑s ⊆ ↑s

Tactic:
exact Set.iUnion₂_subset fun _ ↦ s.upper.smul_subset

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s : UpperSet α
⊢ Set.Ici 1 * ↑s ⊆ ↑s

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s : UpperSet α
⊢ ⋃ a ∈ Set.Ici 1, a • ↑s ⊆ ↑s
-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
theorem toOpen_germ (U : Opens (PrimeSpectrum.Top R)) (x) (hx : x ∈ U) :
    toOpen M U ≫ M.tildeInModuleCat.germ U x hx = toStalk M x

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ toOpen M ⊤ ≫ M.tildeInModuleCat.germ ⊤ x ⋯ = toStalk M x

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ toOpen M U ≫ M.tildeInModuleCat.germ U x hx = toStalk M x

Tactic:
rw [← toOpen_res M ⊤ U (homOfLE le_top : U ⟶ ⊤), Category.assoc, Presheaf.germ_res]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ toOpen M ⊤ ≫ M.tildeInModuleCat.germ ⊤ x ⋯ = toStalk M x
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem sup_mem_subalgebra_closure (A : Subalgebra ℝ C(X, ℝ)) (f g : A) :
    (f : C(X, ℝ)) ⊔ (g : C(X, ℝ)) ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ ↑f ⊔ ↑g ∈ A.topologicalClosure

Tactic:
rw [sup_eq_half_smul_add_add_abs_sub' ℝ]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g + |↑g - ↑f|) ∈ A.topologicalClosure

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |↑g - ↑f| ∈ A.topologicalClosure

Tactic:
exact mod_cast abs_mem_subalgebra_closure A _

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ 2⁻¹ • (↑f + ↑g + |↑g - ↑f|) ∈ A.topologicalClosure

Tactic:
refine
  A.topologicalClosure.smul_mem
    (A.topologicalClosure.add_mem
      (A.topologicalClosure.add_mem (A.le_topologicalClosure f.property)
        (A.le_topologicalClosure g.property))
      ?_)
    _

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f g : ↥A
⊢ |↑g - ↑f| ∈ A.topologicalClosure
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalSemiring_injective :
    Function.Injective (@toNonUnitalSemiring R)

Proof state:
case mk.mk
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring✝ : NonUnitalSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalSemiring = toNonUnitalSemiring
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toNonUnitalSemiring✝¹ : NonUnitalSemiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toNonUnitalSemiring✝ : NonUnitalSemiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toNonUnitalSemiring = toNonUnitalSemiring
⊢ mk mul_comm✝¹ = mk mul_comm✝
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem HasProd.div (hf : HasProd f a₁) (hg : HasProd g a₂) :
    HasProd (fun b ↦ f b / g b) (a₁ / a₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁
hg : HasProd g a₂
⊢ HasProd (fun b => f b / g b) (a₁ / a₂)

Tactic:
simp only [div_eq_mul_inv]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁
hg : HasProd g a₂
⊢ HasProd (fun b => f b * (g b)⁻¹) (a₁ * a₂⁻¹)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁
hg : HasProd g a₂
⊢ HasProd (fun b => f b * (g b)⁻¹) (a₁ * a₂⁻¹)

Tactic:
exact hf.mul hg.inv

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem mul_inv (s s' : S) : ((s : R) /ₒ s') * ((s' : R) /ₒ s) = 1

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
s s' : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
s s' : ↥S
⊢ ↑s /ₒ s' * (↑s' /ₒ s) = 1

Tactic:
simp [oreDiv_mul_char (s : R) s' s' s 1 1 (by simp)]

Result:
no goals