harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Filter.tendsto_nhds_max_left {l : Filter β} {a : α} (h : Tendsto f l (𝓝[>] a)) :
    Tendsto (fun i => max (f i) a) l (𝓝[>] a)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i => f i ⊔ a) l (𝓝[>] a)

Tactic:
simp_rw [max_comm _ a]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝[>] a)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝[>] a)
⊢ Tendsto (fun i => a ⊔ f i) l (𝓝[>] a)

Tactic:
exact Filter.tendsto_nhds_max_right h

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem mem_comm (nH : H.Normal) {a b : G} (h : a * b ∈ H) : b * a ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H

Tactic:
simpa

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
⊢ b * a ∈ H

Tactic:
have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
nH : H.Normal
a b : G
h : a * b ∈ H
this : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H
⊢ b * a ∈ H
-- Mathlib/ModelTheory/Basic.lean
theorem injective_toEmbedding : Function.Injective (toEmbedding : (M ≃[L] N) → M ↪[L] N)

Proof state:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ (fun f => ⇑f) a₁✝ = (fun f => ⇑f) a₂✝

Tactic:
exact congr_arg (DFunLike.coe ∘ Embedding.toHom) h

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective toEmbedding

Tactic:
intro _ _ h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ a₁✝ = a₂✝

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ a₁✝ = a₂✝

Tactic:
apply DFunLike.coe_injective

Result:
case a
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
a₁✝ a₂✝ : M ≃[L] N
h : a₁✝.toEmbedding = a₂✝.toEmbedding
⊢ (fun f => ⇑f) a₁✝ = (fun f => ⇑f) a₂✝
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_pos : (0 : K) < q ↔ 0 < q

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
q : ℚ≥0
⊢ 0 < ↑q ↔ 0 < q

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biInter_inter {ι α : Type*} {s : Set ι} (hs : s.Nonempty) (f : ι → Set α) (t : Set α) :
    ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Proof state:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
simp [biInter_eq_iInter, ← iInter_inter]

Result:
no goals

Proof state:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t

Tactic:
haveI : Nonempty s := hs.to_subtype

Result:
ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ ⋂ i ∈ s, f i ∩ t = (⋂ i ∈ s, f i) ∩ t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem limplies_delete [Clause α β] [Entails α σ] [Formula α β σ] {f : σ} {arr : Array Nat} :
    Limplies α f (delete f arr)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
⊢ Limplies α f (delete f arr)

Tactic:
intro p

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ p ⊨ f → p ⊨ delete f arr

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ p ⊨ f → p ⊨ delete f arr

Tactic:
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ (∀ (x : β), x ∈ toList f → p ⊨ x) → ∀ (x : β), x ∈ toList (delete f arr) → p ⊨ x

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : c ∈ toList f
⊢ p ⊨ c

Tactic:
exact h c del_f_subset

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
⊢ (∀ (x : β), x ∈ toList f → p ⊨ x) → ∀ (x : β), x ∈ toList (delete f arr) → p ⊨ x

Tactic:
intro h c c_in_f_del

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
⊢ p ⊨ c

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : ∀ (c : β), c ∈ toList (delete f arr) → c ∈ toList f
⊢ p ⊨ c

Tactic:
specialize del_f_subset c c_in_f_del

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : c ∈ toList f
⊢ p ⊨ c

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
⊢ p ⊨ c

Tactic:
have del_f_subset := delete_subset f arr

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
arr : Array Nat
p : α → Bool
h : ∀ (x : β), x ∈ toList f → p ⊨ x
c : β
c_in_f_del : c ∈ toList (delete f arr)
del_f_subset : ∀ (c : β), c ∈ toList (delete f arr) → c ∈ toList f
⊢ p ⊨ c
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
a : α
⊢ ¬a ∈ m → m.get? a = none

Tactic:
simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
@[simp] lemma piAntidiag_empty_of_ne_zero (hn : n ≠ 0) : piAntidiag (∅ : Finset ι) n = ∅ :=
  eq_empty_of_forall_not_mem (by simp [@eq_comm _ 0, hn.symm])

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n : μ
hn : n ≠ 0
⊢ ∀ (x : ι → μ), x ∉ ∅.piAntidiag n

Tactic:
simp [@eq_comm _ 0, hn.symm]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_vadd_const_iff {x y z : V} (p : P) :
    Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z

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 : V
p : P
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_vadd_const_iff, (vadd_right_injective p).ne_iff,
  (vadd_right_injective p).ne_iff]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_empty : 𝓝ˢ (∅ : Set X) = ⊥

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝ˢ ∅ = ⊥

Tactic:
rw [isOpen_empty.nhdsSet_eq, principal_empty]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem le_enum_succ {o : Ordinal} (a : (succ o).toType) :
    a ≤ enum (α := (succ o).toType) (· < ·) ⟨o, (type_toType _ ▸ lt_succ o)⟩

Proof state:
o : Ordinal.{u_1}
a : (succ o).toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding a < succ o

Tactic:
apply typein_lt_self

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem foldr_map (g : β → γ) (f : γ → α → α) (a : α) (l : t β) :
    foldr f a (g <$> l) = foldr (f ∘ g) a l

Proof state:
α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : γ → α → α
a : α
l : t β
⊢ foldr f a (g <$> l) = foldr (f ∘ g) a l

Tactic:
simp only [foldr, foldMap_map, Function.comp_def, flip]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_Iic_of_hasDerivAt_of_tendsto (hcont : ContinuousWithinAt f (Iic a) a)
    (hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Iic a))
    (hf : Tendsto f atBot (𝓝 m)) : ∫ x in Iic a, f' x = f a - m

Proof state:
case h
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont✝ : ContinuousWithinAt f (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ IntegrableOn f' (Ioc x a) volume

Tactic:
exact f'int.mono (fun y hy => hy.2) le_rfl

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem rightRel_apply {x y : α} : rightRel s x y ↔ y * x⁻¹ ∈ s :=
  calc
    (∃ a : s, (a : α) * y = x) ↔ ∃ a : s, y * x⁻¹ = a⁻¹

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹

Tactic:
simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ s

Tactic:
simp [exists_inv_mem_iff_exists_mem]

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_add (m n : ℤ) : bodd (m + n) = xor (bodd m) (bodd n)

Proof state:
case negSucc.negSucc
m n : ℕ
⊢ ((m + n).succ + 1).bodd = (m + 1 + (n + 1)).bodd

Tactic:
rw [← Nat.succ_add, add_assoc]

Result:
no goals

Proof state:
m n : ℤ
⊢ (m + n).bodd = (m.bodd ^^ n.bodd)

Tactic:
rcases m with m | m <;>
rcases n with n | n <;>
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat,
           negSucc_add_negSucc, bodd_subNatNat] <;>
simp only [negSucc_coe, bodd_neg, bodd_coe, ← Nat.bodd_add, Bool.xor_comm, ← Nat.cast_add]

Result:
case negSucc.negSucc
m n : ℕ
⊢ ((m + n).succ + 1).bodd = (m + 1 + (n + 1)).bodd
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem prodIsoProd_hom_fst (X Y : TopCat.{u}) :
    (prodIsoProd X Y).hom ≫ prodFst = Limits.prod.fst

Proof state:
X Y : TopCat
⊢ (X.prodIsoProd Y).hom ≫ prodFst = prod.fst

Tactic:
simp [← Iso.eq_inv_comp, prodIsoProd]

Result:
X Y : TopCat
⊢ prodFst = (X.prodBinaryFan Y).fst

Proof state:
X Y : TopCat
⊢ prodFst = (X.prodBinaryFan Y).fst

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_rightUnitor (X : C) : (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom

Tactic:
rw [← whiskerLeft_iff, MonoidalCategory.whiskerLeft_comp, braiding_rightUnitor_aux₂]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure {K : Set E} (hK : IsCompact K)
    (hKmeas : MeasurableSet K) (f g : C(E, ℝ)) {δ : ℝ} (hε : 0 < ε)
    (hfg : ∀ x ∈ K, |g x - f x| < δ) :
    |∫ x in K, mulExpNegMulSq ε (g x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P|
      ≤ δ * (P K).toReal

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (a : E) in K, ε.mulExpNegMulSq (g a) - ε.mulExpNegMulSq (f a) ∂P| ≤ δ * (P K).toReal

Tactic:
apply norm_setIntegral_le_of_norm_le_const hK.measure_lt_top
  (fun x hxK => le_trans (dist_mulExpNegMulSq_le_dist hε) (hfg x hxK).le)
  (StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
  (Continuous.sub g.continuous.mulExpNegMulSq f.continuous.mulExpNegMulSq)))

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| ≤ δ * (P K).toReal

Tactic:
rw [← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
    (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f))]

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |g x - f x| < δ
⊢ |∫ (a : E) in K, ε.mulExpNegMulSq (g a) - ε.mulExpNegMulSq (f a) ∂P| ≤ δ * (P K).toReal
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma inv_nonpos : a⁻¹ ≤ 0 ↔ a ≤ 0

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulMono G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀)

Result:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
simp only [← not_lt, inv_pos]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem comap_map_mk' (N H : Subgroup G) [N.Normal] :
    Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H

Proof state:
G : Type u
inst✝¹ : Group G
N H : Subgroup G
inst✝ : N.Normal
⊢ Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H

Tactic:
simp [Subgroup.comap_map_eq, sup_comm]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem toPiLocalization_injective : Function.Injective (toPiLocalization R) := fun r r' eq ↦ by
  rw [← one_mul r, ← one_mul r']
  by_contra ne
  have ⟨I, mI, hI⟩ := (Module.eqIdeal R r r').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
  have ⟨s, hs⟩ := (IsLocalization.eq_iff_exists I.primeCompl _).mp (congr_fun eq ⟨I, mI⟩)
  exact s.2 (hI hs)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
s : ↥I.primeCompl
hs : ↑s * r = ↑s * r'
⊢ False

Tactic:
exact s.2 (hI hs)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
⊢ False

Tactic:
have ⟨I, mI, hI⟩ := (Module.eqIdeal R r r').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)

Result:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
⊢ False

Tactic:
have ⟨s, hs⟩ := (IsLocalization.eq_iff_exists I.primeCompl _).mp (congr_fun eq ⟨I, mI⟩)

Result:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
s : ↥I.primeCompl
hs : ↑s * r = ↑s * r'
⊢ False

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
⊢ r = r'

Tactic:
rw [← one_mul r, ← one_mul r']

Result:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
⊢ 1 * r = 1 * r'

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
⊢ 1 * r = 1 * r'

Tactic:
by_contra ne

Result:
R : Type u_1
inst✝ : CommSemiring R
r r' : R
eq : (toPiLocalization R) r = (toPiLocalization R) r'
ne : ¬1 * r = 1 * r'
⊢ False
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesSummable.sum (hf : ∀ i ∈ S, LSeriesSummable (f i) s) :
    LSeriesSummable (∑ i ∈ S, f i) s

Proof state:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeriesSummable (∑ i ∈ S, f i) s

Tactic:
simpa [LSeriesSummable, ← term_sum_apply] using summable_sum hf

Result:
no goals
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem comp_map {α β γ : Type _} (f : α → β) (g : β → γ) (x : F α) :
    (g ∘ f) <$> x = g <$> f <$> x

Proof state:
case mk
F : Type u → Type u
q : QPF F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : (P F).B a → α
⊢ abs ((P F).map (g ∘ f✝) ⟨a, f⟩) = abs ((P F).map g ((P F).map f✝ ⟨a, f⟩))

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs (repr x) = g <$> f <$> abs (repr x)

Tactic:
obtain ⟨a, f⟩ := repr x

Result:
case mk
F : Type u → Type u
q : QPF F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : (P F).B a → α
⊢ (g ∘ f✝) <$> abs ⟨a, f⟩ = g <$> f✝ <$> abs ⟨a, f⟩

Proof state:
case mk
F : Type u → Type u
q : QPF F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : (P F).B a → α
⊢ (g ∘ f✝) <$> abs ⟨a, f⟩ = g <$> f✝ <$> abs ⟨a, f⟩

Tactic:
rw [← abs_map, ← abs_map, ← abs_map]

Result:
case mk
F : Type u → Type u
q : QPF F
α β γ : Type u
f✝ : α → β
g : β → γ
x : F α
a : (P F).A
f : (P F).B a → α
⊢ abs ((P F).map (g ∘ f✝) ⟨a, f⟩) = abs ((P F).map g ((P F).map f✝ ⟨a, f⟩))

Proof state:
F : Type u → Type u
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> x = g <$> f <$> x

Tactic:
rw [← abs_repr x]

Result:
F : Type u → Type u
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> abs (repr x) = g <$> f <$> abs (repr x)
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.tsum_inner_products_le (hv : Orthonormal 𝕜 v) :
    ∑' i, ‖⟪v i, x⟫‖ ^ 2 ≤ ‖x‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ 0 ≤ ‖x‖ ^ 2

Tactic:
simp only [norm_nonneg, pow_nonneg]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∑' (i : ι), ‖inner (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Tactic:
refine tsum_le_of_sum_le' ?_ fun s => hv.sum_inner_products_le x

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
hv : Orthonormal 𝕜 v
⊢ 0 ≤ ‖x‖ ^ 2
-- Mathlib/Data/Multiset/Powerset.lean
theorem nodup_powerset {s : Multiset α} : Nodup (powerset s) ↔ Nodup s :=
  ⟨fun h => (nodup_of_le (map_single_le_powerset _) h).of_map _,
    Quotient.inductionOn s fun l h => by
      simp only [quot_mk_to_coe, powerset_coe', coe_nodup]
      refine (nodup_sublists'.2 h).map_on ?_
      exact fun x sx y sy e =>
        (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)⟩

Proof state:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (List.map ofList l.sublists').Nodup

Tactic:
refine (nodup_sublists'.2 h).map_on ?_

Result:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ ∀ x ∈ l.sublists', ∀ y ∈ l.sublists', ↑x = ↑y → x = y

Proof state:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (powerset ⟦l⟧).Nodup

Tactic:
simp only [quot_mk_to_coe, powerset_coe', coe_nodup]

Result:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ (List.map ofList l.sublists').Nodup

Proof state:
α : Type u_1
s : Multiset α
l : List α
h : Nodup ⟦l⟧
⊢ ∀ x ∈ l.sublists', ∀ y ∈ l.sublists', ↑x = ↑y → x = y

Tactic:
exact fun x sx y sy e =>
  (h.perm_iff_eq_of_sublist (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1 (Quotient.exact e)

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem apply_update₂ {ι : Sort*} [DecidableEq ι] {α β γ : ι → Sort*} (f : ∀ i, α i → β i → γ i)
    (g : ∀ i, α i) (h : ∀ i, β i) (i : ι) (v : α i) (w : β i) (j : ι) :
    f j (update g i v j) (update h i w j) = update (fun k ↦ f k (g k) (h k)) i (f i v w) j

Proof state:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
⊢ f i (update g i v i) (update h i w i) = update (fun k => f k (g k) (h k)) i (f i v w) i

Tactic:
simp

Result:
no goals

Proof state:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j

Tactic:
subst j

Result:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
⊢ f i (update g i v i) (update h i w i) = update (fun k => f k (g k) (h k)) i (f i v w) i

Proof state:
case neg
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : ¬j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update g i v j) (update h i w j) = update (fun k => f k (g k) (h k)) i (f i v w) j

Tactic:
by_cases h : j = i

Result:
case pos
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j

case neg
ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h✝ : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
h : ¬j = i
⊢ f j (update g i v j) (update h✝ i w j) = update (fun k => f k (g k) (h✝ k)) i (f i v w) j