harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
@[simp]
lemma localizationAway_jacobiMatrix :
    (localizationAway S r).jacobiMatrix = Matrix.diagonal (fun () ↦ MvPolynomial.C r)

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
h : (pderiv ()) (C r * X () - 1) = C r
⊢ (localizationAway S r).jacobiMatrix = Matrix.diagonal fun x => C r

Tactic:
ext (i : Unit) (j : Unit) : 1

Result:
case a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
h : (pderiv ()) (C r * X () - 1) = C r
i j : Unit
⊢ (localizationAway S r).jacobiMatrix i j = Matrix.diagonal (fun x => C r) i j

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (localizationAway S r).jacobiMatrix = Matrix.diagonal fun x => C r

Tactic:
have h : (pderiv ()) (C r * X () - 1) = C r := by simp

Result:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
h : (pderiv ()) (C r * X () - 1) = C r
⊢ (localizationAway S r).jacobiMatrix = Matrix.diagonal fun x => C r

Proof state:
case a
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
h : (pderiv ()) (C r * X () - 1) = C r
i j : Unit
⊢ (localizationAway S r).jacobiMatrix i j = Matrix.diagonal (fun x => C r) i j

Tactic:
rwa [jacobiMatrix_apply]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ (pderiv ()) (C r * X () - 1) = C r

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_or_distrib_right : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c

Proof state:
a b c : Prop
⊢ (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c

Tactic:
rw [or_or_or_comm, or_self]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma nnreal_iff [Algebra ℝ A] {a : A} :
    SpectrumRestricts a ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Proof state:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ 0 ≤ x

Tactic:
obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx

Result:
case refine_1.intro.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
hx : (algebraMap ℝ≥0 ℝ) x ∈ spectrum ℝ a
⊢ 0 ≤ (algebraMap ℝ≥0 ℝ) x

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ spectrum ℝ a, 0 ≤ x

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ 0 ≤ x

case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

Proof state:
case refine_1.intro.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
x : ℝ≥0
hx : (algebraMap ℝ≥0 ℝ) x ∈ spectrum ℝ a
⊢ 0 ≤ (algebraMap ℝ≥0 ℝ) x

Tactic:
exact coe_nonneg x

Result:
no goals

Proof state:
case refine_2
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal

Tactic:
exact .of_subset_range_algebraMap (fun _ ↦ Real.toNNReal_coe) fun x hx ↦ ⟨⟨x, h x hx⟩, rfl⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/RationalRoot.lean
theorem num_isRoot_scaleRoots_of_aeval_eq_zero [UniqueFactorizationMonoid A] {p : A[X]} {x : K}
    (hr : aeval x p = 0) : IsRoot (scaleRoots p (den A x)) (num A x)

Proof state:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ eval₂ (algebraMap A K) ((algebraMap A K) (num A x)) (p.scaleRoots ↑(den A x)) = 0

Tactic:
refine scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero ?_

Result:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (aeval (mk' K (num A x) (den A x))) p = 0

Proof state:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (aeval x) p = 0

Tactic:
exact hr

Result:
no goals

Proof state:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (aeval (mk' K (num A x) (den A x))) p = 0

Tactic:
rw [mk'_num_den]

Result:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (aeval x) p = 0

Proof state:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ (p.scaleRoots ↑(den A x)).IsRoot (num A x)

Tactic:
apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)

Result:
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : UniqueFactorizationMonoid A
p : A[X]
x : K
hr : (aeval x) p = 0
⊢ eval₂ (algebraMap A K) ((algebraMap A K) (num A x)) (p.scaleRoots ↑(den A x)) = 0
-- Mathlib/Algebra/Category/Grp/Basic.lean
theorem asHom_injective {G : AddCommGrp.{0}} : Function.Injective (@asHom G) := fun h k w => by
  simpa using CategoryTheory.congr_fun w 1

Proof state:
G : AddCommGrp
h k : ↑G
w : asHom h = asHom k
⊢ h = k

Tactic:
simpa using CategoryTheory.congr_fun w 1

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_closure_pos_iff_not_mem_closure {x : α} {E : Set α} :
    0 < infEdist x (closure E) ↔ x ∉ closure E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
⊢ 0 < infEdist x (closure E) ↔ x ∉ closure E

Tactic:
rw [infEdist_closure, infEdist_pos_iff_not_mem_closure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List  (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany m l).1.getKey? k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany m l).val.getKey? k' = some k

Tactic:
simp_to_model [Const.insertMany] using List.getKey?_insertListConst_of_mem

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_comp (s : Rel β γ) (t : Set γ) :
    preimage (r • s) t = preimage r (preimage s t)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
⊢ (r • s).preimage t = r.preimage (s.preimage t)

Tactic:
simp only [preimage, inv_comp, image_comp]

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem map_sup (hf : LeftOrdContinuous f) (x y : α) : f (x ⊔ y) = f x ⊔ f y :=
  (hf isLUB_pair).unique <| by simp only [image_pair, isLUB_pair]

Proof state:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
x y : α
⊢ IsLUB (f '' {x, y}) (f x ⊔ f y)

Tactic:
simp only [image_pair, isLUB_pair]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem subsingleton_of_subsingleton_span_eq_top {s : Set P} (h₁ : s.Subsingleton)
    (h₂ : affineSpan k s = ⊤) : Subsingleton P

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
⊢ Subsingleton P

Tactic:
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ Subsingleton P

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ Subsingleton P

Tactic:
have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ {p} ⊆ s

Tactic:
simp [hp]

Result:
no goals

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton,
  AffineSubspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
p : P
h₂ : univ.Subsingleton
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
p : P
h₂ : univ.Subsingleton
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
exact subsingleton_of_univ_subsingleton h₂

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem IsComplement'.isCompl (h : IsComplement' H K) : IsCompl H K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K

Tactic:
obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g

Result:
case intro.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h✝ : H.IsComplement' K
h : ↑↑H
k : ↑↑K
x✝ : (fun x => ↑x.1 * ↑x.2) (h, k) ∈ ⊤
⊢ (fun x => ↑x.1 * ↑x.2) (h, k) ∈ H ⊔ K

Proof state:
case intro.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h✝ : H.IsComplement' K
h : ↑↑H
k : ↑↑K
x✝ : (fun x => ↑x.1 * ↑x.2) (h, k) ∈ ⊤
⊢ (fun x => ↑x.1 * ↑x.2) (h, k) ∈ H ⊔ K

Tactic:
exact Subgroup.mul_mem_sup h.2 k.2

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
⊢ IsCompl H K

Tactic:
refine
  ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
      let x : H × K := ⟨⟨g, p⟩, 1⟩
      let y : H × K := ⟨1, g, q⟩
      Subtype.ext_iff.mp
        (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
    codisjoint_iff_le_sup.mpr fun g _ => ?_⟩

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.IsComplement' K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma mul_mod_mod (a b c : ℕ) : (a * (b % c)) % c = a * b % c

Proof state:
a b c : ℕ
⊢ a * (b % c) % c = a * b % c

Tactic:
rw [mul_mod, mod_mod, ← mul_mod]

Result:
no goals
-- Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean
theorem adic_module_basis :
    I.ringFilterBasis.SubmodulesBasis fun n : ℕ => I ^ n • (⊤ : Submodule R M) :=
  { inter := fun i j =>
      ⟨max i j,
        le_inf_iff.mpr
          ⟨smul_mono_left <| pow_le_pow_right (le_max_left i j),
            smul_mono_left <| pow_le_pow_right (le_max_right i j)⟩⟩
    smul := fun m i =>
      ⟨(I ^ i • ⊤ : Ideal R), ⟨i, by simp⟩, fun a a_in => by
        replace a_in : a ∈ I ^ i

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
⊢ ↑(I ^ i • ⊤) = ↑((fun i => toAddSubgroup (I ^ i • ⊤)) i)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)

Tactic:
exact smul_mem_smul a_in mem_top

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)

Tactic:
replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ I ^ i
⊢ a ∈ (fun x => x • m) ⁻¹' ↑(I ^ i • ⊤)

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ I ^ i

Tactic:
simpa [(I ^ i).mul_top] using a_in

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
    (not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) :
    getKey! (insertManyIfNewUnit m l) k' = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k k' : α
k_beq : (k == k') = true
not_mem : ¬k ∈ m
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (insertManyIfNewUnit m l).getKey! k' = k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey! k' = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKey! k' = k

Tactic:
exact Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
  not_mem distinct mem

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem iSupIndep_of_dfinsupp_sumAddHom_injective (p : ι → AddSubmonoid N)
    (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
⊢ iSupIndep p

Tactic:
rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoid N ≃o _)]

Result:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
⊢ iSupIndep (⇑AddSubmonoid.toNatSubmodule ∘ p)

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid N
p : ι → AddSubmonoid N
h : Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
⊢ iSupIndep (⇑AddSubmonoid.toNatSubmodule ∘ p)

Tactic:
exact iSupIndep_of_dfinsupp_lsum_injective _ h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_ofReal_of_nonneg {x : ℝ} (hx : 0 ≤ x) : arg x = 0

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ (↑x).arg = 0

Tactic:
simp [arg, hx]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_lintegral_le_pos (hint : ∫⁻ a, f a ∂μ ≠ ∞) : 0 < μ {x | ∫⁻ a, f a ∂μ ≤ f x}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
⊢ 0 < μ {x | ∫⁻ (a : α), f a ∂μ ≤ f x}

Tactic:
simpa only [laverage_eq_lintegral] using
  measure_laverage_le_pos (IsProbabilityMeasure.ne_zero μ) hint

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_left_singleton : (a * ·) ⁻¹' {b} = {a⁻¹ * b}

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x => a * x) ⁻¹' {b} = {a⁻¹ * b}

Tactic:
rw [← image_mul_left', image_singleton]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma toNNReal_lt_one {r : ℝ} : r.toNNReal < 1 ↔ r < 1

Proof state:
r : ℝ
⊢ r.toNNReal < 1 ↔ r < 1

Tactic:
simp only [← not_le, one_le_toNNReal]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem injective_piecewise_iff {f g : α → β} :
    Injective (s.piecewise f g) ↔
      InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ Injective (s.piecewise f g) ↔ InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y

Tactic:
rw [injective_iff_injOn_univ, ← union_compl_self s, injOn_union (@disjoint_compl_right _ _ s),
  (piecewise_eqOn s f g).injOn_iff, (piecewise_eqOn_compl s f g).injOn_iff]

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∈ sᶜ, s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ s.piecewise f g x ≠ s.piecewise f g y ↔ f x ≠ g y

Tactic:
rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_not_mem s f g hy]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
⊢ (InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∈ sᶜ, s.piecewise f g x ≠ s.piecewise f g y) ↔
    InjOn f s ∧ InjOn g sᶜ ∧ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g y

Tactic:
refine and_congr Iff.rfl (and_congr Iff.rfl <| forall₄_congr fun x hx y hy => ?_)

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
x : α
hx : x ∈ s
y : α
hy : y ∈ sᶜ
⊢ s.piecewise f g x ≠ s.piecewise f g y ↔ f x ≠ g y
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformContinuous_monoidHom_of_continuous {hom : Type*} [UniformSpace β] [Group β]
    [UniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Continuous f) :
    UniformContinuous f :=
  uniformContinuous_of_tendsto_one <|
    suffices Tendsto f (𝓝 1) (𝓝 (f 1)) by rwa [map_one] at this
    h.tendsto 1

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : UniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : UniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Continuous ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 (f 1))
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
rwa [map_one] at this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_eq_some_iff {xs : List α} {a : α} : xs.head? = some a ↔ ∃ ys, xs = a :: ys

Proof state:
α : Type u_1
xs : List α
a : α
⊢ xs.head? = some a ↔ ∃ ys, xs = a :: ys

Tactic:
cases xs <;> simp_all

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
@[simp]
lemma bnot_isSome (a : Option α) : (! a.isSome) = a.isNone

Proof state:
α : Type u_1
a : Option α
⊢ (!a.isSome) = a.isNone

Tactic:
cases a <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem affineSpan_eq_top_iff_vectorSpan_eq_top_of_nontrivial {s : Set P} [Nontrivial P] :
    affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
s : Set P
inst✝ : Nontrivial P
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Result:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
s : Set P
inst✝ : Nontrivial P
hs : s = ∅
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
s : Set P
inst✝ : Nontrivial P
hs : s.Nonempty
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Proof state:
case inr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
s : Set P
inst✝ : Nontrivial P
hs : s.Nonempty
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
rw [affineSpan_eq_top_iff_vectorSpan_eq_top_of_nonempty k V P hs]

Result:
no goals

Proof state:
case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
s : Set P
inst✝ : Nontrivial P
hs : s = ∅
⊢ affineSpan k s = ⊤ ↔ vectorSpan k s = ⊤

Tactic:
simp [hs, subsingleton_iff_bot_eq_top, AddTorsor.subsingleton_iff V P, not_subsingleton]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem hasSum_mFourier_series_of_summable (h : Summable (mFourierCoeff f)) :
    HasSum (fun i ↦ mFourierCoeff f i • mFourier i) f

Proof state:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i => mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ Summable fun a => ‖mFourierCoeff (⇑f) a • mFourier a‖

Tactic:
simpa only [norm_smul, mFourier_norm, mul_one] using h.norm

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 :
  HasSum (fun i => mFourierCoeff (↑↑((ContinuousMap.toLp 2 volume ℂ) f)) i • mFourierLp 2 i)
    ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ HasSum (fun i => mFourierCoeff (⇑f) i • mFourier i) f

Tactic:
simp only [mFourierCoeff_toLp] at sum_L2

Result:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i => mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ HasSum (fun i => mFourierCoeff (⇑f) i • mFourier i) f

Proof state:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i => mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ HasSum (fun i => mFourierCoeff (⇑f) i • mFourier i) f

Tactic:
refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2

Result:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 : HasSum (fun i => mFourierCoeff (⇑f) i • mFourierLp 2 i) ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ Summable fun a => ‖mFourierCoeff (⇑f) a • mFourier a‖

Proof state:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
⊢ HasSum (fun i => mFourierCoeff (⇑f) i • mFourier i) f

Tactic:
have sum_L2 := hasSum_mFourier_series_L2 (ContinuousMap.toLp 2 volume ℂ f)

Result:
d : Type u_1
inst✝ : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (mFourierCoeff ⇑f)
sum_L2 :
  HasSum (fun i => mFourierCoeff (↑↑((ContinuousMap.toLp 2 volume ℂ) f)) i • mFourierLp 2 i)
    ((ContinuousMap.toLp 2 volume ℂ) f)
⊢ HasSum (fun i => mFourierCoeff (⇑f) i • mFourier i) f