harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.disjoint_openCell_of_ne [RelCWComplex C D] {n m : ℕ} {i : cell C n}
    {j : cell C m} (ne : (⟨n, i⟩ : Σ n, cell C n) ≠ ⟨m, j⟩) : openCell n i ∩ openCell m j = ∅

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ
i : cell C n
j : cell C m
ne : ⟨n, i⟩ ≠ ⟨m, j⟩
this : univ.PairwiseDisjoint fun ni => openCell ni.fst ni.snd
⊢ openCell n i ∩ openCell m j = ∅

Tactic:
simp only [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_iff_inter_eq_empty] at this

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ
i : cell C n
j : cell C m
ne : ⟨n, i⟩ ≠ ⟨m, j⟩
this :
  ∀ ⦃x : (n : ℕ) × cell C n⦄,
    x ∈ univ → ∀ ⦃y : (n : ℕ) × cell C n⦄, y ∈ univ → x ≠ y → openCell x.fst x.snd ∩ openCell y.fst y.snd = ∅
⊢ openCell n i ∩ openCell m j = ∅

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ
i : cell C n
j : cell C m
ne : ⟨n, i⟩ ≠ ⟨m, j⟩
⊢ openCell n i ∩ openCell m j = ∅

Tactic:
have := pairwiseDisjoint (C := C) (D := D)

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ
i : cell C n
j : cell C m
ne : ⟨n, i⟩ ≠ ⟨m, j⟩
this : univ.PairwiseDisjoint fun ni => openCell ni.fst ni.snd
⊢ openCell n i ∩ openCell m j = ∅

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n m : ℕ
i : cell C n
j : cell C m
ne : ⟨n, i⟩ ≠ ⟨m, j⟩
this :
  ∀ ⦃x : (n : ℕ) × cell C n⦄,
    x ∈ univ → ∀ ⦃y : (n : ℕ) × cell C n⦄, y ∈ univ → x ≠ y → openCell x.fst x.snd ∩ openCell y.fst y.snd = ∅
⊢ openCell n i ∩ openCell m j = ∅

Tactic:
exact this (mem_univ _) (mem_univ _) ne

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Hom.lean
theorem comp_id_id (B : BilinForm R M) : B.comp LinearMap.id LinearMap.id = B

Proof state:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.comp id id) x✝) y✝ = (B x✝) y✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.comp id id = B

Tactic:
ext

Result:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ y✝ : M
⊢ ((B.comp id id) x✝) y✝ = (B x✝) y✝
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coe_monomial (n : ℕ) (a : R) :
    (monomial n a : PowerSeries R) = PowerSeries.monomial R n a

Proof state:
case h
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) ↑((monomial n) a) = (PowerSeries.coeff R n✝) ((PowerSeries.monomial R n) a)

Tactic:
simp [coeff_coe, PowerSeries.coeff_monomial, Polynomial.coeff_monomial, eq_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
⊢ ↑((monomial n) a) = (PowerSeries.monomial R n) a

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
a : R
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) ↑((monomial n) a) = (PowerSeries.coeff R n✝) ((PowerSeries.monomial R n) a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_replace_of_ne [LawfulBEq α] {l : List α} {i : Nat} {h : i < l.length} (h' : l[i] ≠ a) :
    (l.replace a b)[i]'(by simpa) = l[i]'(h)

Proof state:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
h' : l[i] ≠ a
⊢ (l.replace a b)[i] = l[i]

Tactic:
rw [getElem_replace h]

Result:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
h' : l[i] ≠ a
⊢ (if (l[i] == a) = true then if a ∈ take i l then a else b else l[i]) = l[i]

Proof state:
α : Type ?u.366943
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
h' : l[i] ≠ a
⊢ i < (l.replace a b).length

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : i < l.length
h' : l[i] ≠ a
⊢ (if (l[i] == a) = true then if a ∈ take i l then a else b else l[i]) = l[i]

Tactic:
simp [h']

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem IsHenstock.disjUnion (h₁ : IsHenstock π₁) (h₂ : IsHenstock π₂)
    (h : Disjoint π₁.iUnion π₂.iUnion) : IsHenstock (π₁.disjUnion π₂ h)

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
⊢ (π₁.disjUnion π₂ h).IsHenstock

Tactic:
refine fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => ?_) fun hJ => ?_

Result:
case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

Proof state:
case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

Tactic:
rw [disjUnion_tag_of_mem_left _ hJ]

Result:
case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ π₁.tag J ∈ Box.Icc J

Proof state:
case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ π₂.tag J ∈ Box.Icc J

Tactic:
exact h₂ _ hJ

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₁.boxes
⊢ π₁.tag J ∈ Box.Icc J

Tactic:
exact h₁ _ hJ

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ (π₁.disjUnion π₂ h).tag J ∈ Box.Icc J

Tactic:
rw [disjUnion_tag_of_mem_right _ hJ]

Result:
case refine_2
ι : Type u_1
I : Box ι
π₁ π₂ : TaggedPrepartition I
h₁ : π₁.IsHenstock
h₂ : π₂.IsHenstock
h : Disjoint π₁.iUnion π₂.iUnion
J : Box ι
hJ✝ : J ∈ π₁.disjUnion π₂ h
hJ : J ∈ π₂.boxes
⊢ π₂.tag J ∈ Box.Icc J
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma neg_root_mem :
    - P.root i ∈ range P.root :=
  ⟨P.reflection_perm i i, by simp⟩

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ P.root ((P.reflection_perm i) i) = -P.root i

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/ReesAlgebra.lean
theorem mem_reesAlgebra_iff_support (f : R[X]) :
    f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i

Tactic:
apply forall_congr'

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ∀ (a : ℕ), f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Tactic:
rw [mem_support_iff, Iff.comm, Classical.imp_iff_right_iff, Ne, ← imp_iff_not_or]

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a = 0 → f.coeff a ∈ I ^ a

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ∀ (a : ℕ), f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Tactic:
intro a

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
a : ℕ
⊢ f.coeff a = 0 → f.coeff a ∈ I ^ a

Tactic:
exact fun e => e.symm ▸ (I ^ a).zero_mem

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
lemma opensMeasurableSpace_iff_forall_measurableSet
    [TopologicalSpace α] [MeasurableSpace α] :
    OpensMeasurableSpace α ↔  (∀ (s : Set α), IsOpen s → MeasurableSet s)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
h : OpensMeasurableSpace α
s : Set α
hs : IsOpen s
⊢ MeasurableSet s

Tactic:
exact OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
⊢ OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen s → MeasurableSet s

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
h : OpensMeasurableSpace α
s : Set α
hs : IsOpen s
⊢ MeasurableSet s
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Proof state:
x y : ℝ
⊢ sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Tactic:
simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformContinuous_eval (x : α) :
    UniformContinuous (Function.eval x ∘ toFun : (α →ᵤ β) → β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆ (fun x_1 => ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'

Tactic:
exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous (Function.eval x ∘ ⇑toFun)

Tactic:
change _ ≤ _

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 => ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 => ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β

Tactic:
rw [map_le_iff_le_comap,
  (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ ∀ i' ∈ 𝓤 β,
    ∃ i ∈ 𝓤 β,
      UniformFun.gen α β i ⊆ (fun x_1 => ((Function.eval x ∘ ⇑toFun) x_1.1, (Function.eval x ∘ ⇑toFun) x_1.2)) ⁻¹' id i'
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem support_eq : Function.support f = Metric.ball c f.rOut

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) = ball c f.rOut

Tactic:
ext x

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ x ∈ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) ↔ x ∈ ball c f.rOut

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ support ↑f = ball c f.rOut

Tactic:
simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) = ball c f.rOut

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
⊢ x ∈ (fun x => f.rIn⁻¹ • (x - c)) ⁻¹' ball 0 (f.rOut / f.rIn) ↔ x ∈ ball c f.rOut

Tactic:
simp only [mem_ball_iff_norm, sub_zero, norm_smul, mem_preimage, Real.norm_eq_abs, abs_inv,
  abs_of_pos f.rIn_pos, ← div_eq_inv_mul, div_lt_div_iff_of_pos_right f.rIn_pos]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_principal {a : Set α} {p : α → Prop} : (∃ᶠ x in 𝓟 a, p x) ↔ ∃ x ∈ a, p x

Proof state:
α : Type u
a : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ x ∈ a, p x

Tactic:
simp [Filter.Frequently, not_forall]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedCoreAux_subset (s : Set E) : balancedCoreAux 𝕜 s ⊆ s := fun x hx => by
  simpa only [one_smul] using mem_balancedCoreAux_iff.1 hx 1 norm_one.ge

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ balancedCoreAux 𝕜 s
⊢ x ∈ s

Tactic:
simpa only [one_smul] using mem_balancedCoreAux_iff.1 hx 1 norm_one.ge

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma sUnion_disjointOfDiffUnion_subset (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) : ⋃₀ (hC.disjointOfDiffUnion hs hI : Set (Set α)) ⊆ s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ s

Tactic:
rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ s \ ⋃₀ ↑I ⊆ s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ s \ ⋃₀ ↑I ⊆ s

Tactic:
exact diff_subset

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpTo_top_iff (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpTo N f p ↔ ∀ n : ℕ, HasFTaylorSeriesUpTo n f p

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
N : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hN : ∞ ≤ N
⊢ HasFTaylorSeriesUpTo N f p ↔ ∀ (n : ℕ), HasFTaylorSeriesUpTo (↑n) f p

Tactic:
simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff hN]

Result:
no goals
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem scottContinuous_of_continuous {α β} [OmegaCompletePartialOrder α]
    [OmegaCompletePartialOrder β] (f : Scott α → Scott β) (hf : _root_.Continuous f) :
    OmegaCompletePartialOrder.ωScottContinuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })
⊢ f (ωSup c) ≤ z ↔ ωSup (c.map { toFun := f, monotone' := h }) ≤ z

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf'' : IsOpen (f ⁻¹' notBelow z)
hf' : (¬f (ωSup c) ≤ z) = ωSup (c.map { toFun := fun x => ¬f x ≤ z, monotone' := ⋯ })
⊢ ¬f (ωSup c) ≤ z ↔ ¬ωSup (c.map { toFun := f, monotone' := h }) ≤ z
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions monovary iff the rearrangement inequality holds. -/
lemma monovary_iff_mul_rearrangement :
    Monovary f g ↔ ∀ i j, f i * g j + f j * g i ≤ f i * g i + f j * g j

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : LinearOrderedRing α
f g : ι → α
⊢ Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j

Tactic:
simp only [smul_eq_mul, monovary_iff_smul_rearrangement]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma opcyclesMap'_g' : opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃

Tactic:
simp only [← cancel_epi h₁.p, assoc, φ.comm₂₃, p_opcyclesMap'_assoc,
  RightHomologyData.p_g'_assoc, RightHomologyData.p_g']

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
lemma Ideal.isPrime_map_of_isLocalizationAtPrime {p : Ideal R} [p.IsPrime] (hpq : p ≤ q) :
    (p.map (algebraMap R S)).IsPrime

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ Disjoint ↑q.primeCompl ↑p

Tactic:
simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Result:
no goals

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ p.IsPrime

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
⊢ (map (algebraMap R S) p).IsPrime

Tactic:
have disj : Disjoint (q.primeCompl : Set R) p := by
  simp [Ideal.primeCompl, ← le_compl_iff_disjoint_left, hpq]

Result:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ (map (algebraMap R S) p).IsPrime

Proof state:
R : Type u_4
inst✝⁵ : CommRing R
q : Ideal R
inst✝⁴ : q.IsPrime
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization.AtPrime S q
p : Ideal R
inst✝ : p.IsPrime
hpq : p ≤ q
disj : Disjoint ↑q.primeCompl ↑p
⊢ (map (algebraMap R S) p).IsPrime

Tactic:
apply IsLocalization.isPrime_of_isPrime_disjoint q.primeCompl _ p (by simpa) disj

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem finrank_eq_one_iff [Nontrivial E] [Module.Free F S] : finrank F S = 1 ↔ S = ⊥

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ finrank F ↥S = 1 ↔ Module.rank F ↥S = 1

Tactic:
exact toNat_eq_iff one_ne_zero

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ finrank F ↥S = 1 ↔ S = ⊥

Tactic:
rw [← Subalgebra.rank_eq_one_iff]

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ finrank F ↥S = 1 ↔ Module.rank F ↥S = 1
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
/-- In a unital C⋆-algebra, if `0 ≤ a ≤ b` and `a` and `b` are units, then `b⁻¹ ≤ a⁻¹`. -/
protected lemma inv_le_inv {a b : Aˣ} (ha : 0 ≤ (a : A))
    (hab : (a : A) ≤ b) : (↑b⁻¹ : A) ≤ a⁻¹

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
rw [le_iff_norm_sqrt_mul_sqrt_inv ha hb, ← sq_le_one_iff₀ (norm_nonneg _), sq,
  ← CStarRing.norm_star_mul_self] at hab

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
have hb := ha.trans hab

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
hb : 0 ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
have ha_inv : (0 : A) ≤ a⁻¹ := inv_nonneg_of_nonneg a ha

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * star (sqrt ↑b⁻¹ * sqrt ↑a)‖ ≤ 1

Tactic:
rwa [star_mul, IsSelfAdjoint.of_nonneg sqrt_nonneg,
  IsSelfAdjoint.of_nonneg sqrt_nonneg] at hab ⊢

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
rw [le_iff_norm_sqrt_mul_sqrt_inv hb_inv ha_inv, inv_inv, ← sq_le_one_iff₀ (norm_nonneg _), sq,
  ← CStarRing.norm_self_mul_star]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ‖star (sqrt ↑a * sqrt ↑b⁻¹) * (sqrt ↑a * sqrt ↑b⁻¹)‖ ≤ 1
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
ha_inv : 0 ≤ ↑a⁻¹
⊢ ‖sqrt ↑b⁻¹ * sqrt ↑a * star (sqrt ↑b⁻¹ * sqrt ↑a)‖ ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
hb : 0 ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
have hb_inv : (0 : A) ≤ b⁻¹ := inv_nonneg_of_nonneg b hb

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
hb : 0 ≤ ↑b
hb_inv : 0 ≤ ↑b⁻¹
⊢ ↑b⁻¹ ≤ ↑a⁻¹
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem dotProduct_star : v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/Algebra/Ring/CompTypeclasses.lean
theorem comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] :
    RingHomSurjective σ₁₃ :=
  { is_surjective

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective (⇑σ₂₃ ∘ ⇑σ₁₂)
⊢ Function.Surjective ⇑σ₁₃

Tactic:
rwa [← RingHom.coe_comp, RingHomCompTriple.comp_eq] at this

Result:
no goals

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
⊢ Function.Surjective ⇑σ₁₃

Tactic:
have := σ₂₃.surjective.comp σ₁₂.surjective

Result:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective (⇑σ₂₃ ∘ ⇑σ₁₂)
⊢ Function.Surjective ⇑σ₁₃
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_negAddY (P Q : Fin 3 → A) :
    (W'.baseChange B).toProjective.negAddY (f ∘ P) (f ∘ Q) =
      f ((W'.baseChange A).toProjective.negAddY P Q)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toProjective.negAddY (⇑f ∘ P) (⇑f ∘ Q) = f ((baseChange W' A).toProjective.negAddY P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

Result:
no goals