harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of a Dirichlet character `χ` and of the twist of `μ` by `χ` are multiplicative
inverses. -/
lemma LSeries.mul_mu_eq_one {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ}
    (hs : 1 < s.re) : L ↗χ s * L (↗χ * ↗μ) s = 1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L (fun n => χ ↑n) s * L ((fun n => χ ↑n) * fun n => ↑(μ n)) s = 1

Tactic:
rw [← LSeries_convolution' (LSeriesSummable_of_one_lt_re χ hs) <|
        LSeriesSummable_mul χ <| ArithmeticFunction.LSeriesSummable_moebius_iff.mpr hs,
  convolution_mul_moebius, LSeries_delta, Pi.one_apply]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem zero_update : update 0 a b = single a b

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
a✝ : α
⊢ (update 0 a b) a✝ = (single a b) a✝

Tactic:
rw [single_eq_update, coe_update, coe_zero]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ update 0 a b = single a b

Tactic:
classical
  ext
  rw [single_eq_update, coe_update, coe_zero]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ update 0 a b = single a b

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
a✝ : α
⊢ (update 0 a b) a✝ = (single a b) a✝
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousOn_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} :
    ContinuousOn f s ↔ ∀ b, ContinuousOn (f ⟨·, b⟩) {a | (a, b) ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) {a | (a, b) ∈ s}

Tactic:
simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x => f (x, b)) {a | (a, b) ∈ s} a) ↔
    ∀ (b : β), ∀ x ∈ {a | (a, b) ∈ s}, ContinuousWithinAt (fun x => f (x, b)) {a | (a, b) ∈ s} x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
⊢ (∀ (a : α) (b : β), (a, b) ∈ s → ContinuousWithinAt (fun x => f (x, b)) {a | (a, b) ∈ s} a) ↔
    ∀ (b : β), ∀ x ∈ {a | (a, b) ∈ s}, ContinuousWithinAt (fun x => f (x, b)) {a | (a, b) ∈ s} x

Tactic:
apply forall_swap

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_add_Iio : (fun x => a + x) '' Iio b = Iio (a + b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => a + x) '' Iio b = Iio (a + b)

Tactic:
simp [add_comm]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem congr_equiv {p : SeminormFamily 𝕜 E ι} [t : TopologicalSpace E]
    (hp : WithSeminorms p) (e : ι' ≃ ι) : WithSeminorms (p ∘ e)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
ι' : Type u_9
inst✝⁴ : Nonempty ι
inst✝³ : Nonempty ι'
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
t : TopologicalSpace E
hp : WithSeminorms p
e : ι' ≃ ι
⊢ WithSeminorms (p ∘ ⇑e)

Tactic:
refine hp.congr ?_ ?_ <;>
intro i <;>
[use {e i}, 1; use {e.symm i}, 1] <;>
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.post_post {E : Type u''} [Category.{v''} E] (H : D ⥤ E)
    -- H G (colimit F) ⟶ H (colimit (F ⋙ G)) ⟶ colimit ((F ⋙ G) ⋙ H) equals
    -- H G (colimit F) ⟶ colimit (F ⋙ (G ⋙ H))
    [h : HasColimit ((F ⋙ G) ⋙ H)] : haveI : HasColimit (F ⋙ G ⋙ H) := h
    colimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
haveI : HasColimit (F ⋙ G ⋙ H) := h

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
this : HasColimit (F ⋙ G ⋙ H)
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
⊢ post (F ⋙ G) H ≫ H.map (post F G) = post F (G ⋙ H)

Tactic:
ext j

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ ι ((F ⋙ G) ⋙ H) j ≫ post (F ⋙ G) H ≫ H.map (post F G) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
this : HasColimit (F ⋙ G ⋙ H)
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
exact (colimit.ι_post F (G ⋙ H) j).symm

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem terminal.hom_ext [HasTerminal C] {P : C} (f g : P ⟶ ⊤_ C) : f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P : C
f g : P ⟶ ⊤_ C
⊢ f = g

Tactic:
ext ⟨⟨⟩⟩

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem neg_mem_ball_zero {r : ℝ} {x : E} : -x ∈ ball p 0 r ↔ x ∈ ball p 0 r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -x ∈ p.ball 0 r ↔ x ∈ p.ball 0 r

Tactic:
simp only [mem_ball_zero, map_neg_eq_map]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_lt_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} :
    ∀ᵐ x ∂(η a), rnDeriv κ η a x < ∞

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂η a, κ.rnDeriv η a x < ⊤

Tactic:
filter_upwards [κ.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_ne_top _]
  with x heq htop using heq ▸ htop.lt_top

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β → β
a : α
l : List α
ih : ∀ (b : β), foldr (fun t acc => f t.val acc) b l.attach = foldr f b l
b : β
⊢ foldr (fun t acc => f t.val acc) b (a :: l).attach = foldr f b (a :: l)

Tactic:
rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β → β
b : β
⊢ foldr (fun t acc => f t.val acc) b l.attach = foldr f b l

Tactic:
induction l generalizing b with
| nil => simp
| cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β → β
b : β
⊢ foldr (fun t acc => f t.val acc) b [].attach = foldr f b []

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_modify_self (h : m.1.WF) {k : α} {f : β → β} {hc : (Const.modify m k f).contains k} :
    haveI h' : m.contains k

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : LawfulBEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : β → β
hc : (modify m k f).contains k = true
⊢ m.contains k = true

Tactic:
rwa [contains_modify _ h] at hc

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : β → β
hc : (modify m k f).contains k = true
⊢ get (modify m k f) k hc = f (get m k ⋯)

Tactic:
simp_to_model [Const.modify] using List.Const.getValue_modifyKey_self

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_singleton_inter (a : α) (s : Set α) : ({a} ∩ s).ncard ≤ 1

Proof state:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).ncard ≤ 1

Tactic:
rw [← Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one]

Result:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1

Proof state:
α : Type u_1
a : α
s : Set α
⊢ ({a} ∩ s).encard ≤ 1

Tactic:
apply encard_singleton_inter

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tight.lean
protected lemma union (hS : IsTightMeasureSet S) (hT : IsTightMeasureSet T) :
    IsTightMeasureSet (S ∪ T)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S T : Set (Measure α)
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ Tendsto ((⨆ x ∈ S, ⇑x) ⊔ ⨆ x ∈ T, ⇑x) (cocompact α).smallSets (𝓝 0)

Tactic:
convert Tendsto.sup_nhds hS hT

Result:
case h.e'_5.h.e'_3
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S T : Set (Measure α)
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ 0 = 0 ⊔ 0

Proof state:
case h.e'_5.h.e'_3
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S T : Set (Measure α)
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ 0 = 0 ⊔ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S T : Set (Measure α)
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ IsTightMeasureSet (S ∪ T)

Tactic:
rw [IsTightMeasureSet, iSup_union]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
mα : MeasurableSpace α
S T : Set (Measure α)
hS : IsTightMeasureSet S
hT : IsTightMeasureSet T
⊢ Tendsto ((⨆ x ∈ S, ⇑x) ⊔ ⨆ x ∈ T, ⇑x) (cocompact α).smallSets (𝓝 0)
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
theorem commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right
    {i₁ : ZMod 2} (hm₁ : m₁ ∈ evenOdd Q₁ i₁) (hm₂ : m₂ ∈ evenOdd Q₂ 0) :
    Commute (map f₁ m₁) (map f₂ m₂) :=
  (map_mul_map_of_isOrtho_of_mem_evenOdd _ _ hf _ _ hm₁ hm₂).trans <| by simp

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
i₁ : ZMod 2
hm₁ : m₁ ∈ evenOdd Q₁ i₁
hm₂ : m₂ ∈ evenOdd Q₂ 0
⊢ (-1) ^ (0 * i₁) • ((map f₂) m₂ * (map f₁) m₁) = (map f₂) m₂ * (map f₁) m₁

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_unitClosedBall_of_nonneg {r : ℝ} (hr : 0 ≤ r) :
    r • closedBall (0 : E) 1 = closedBall (0 : E) r

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
⊢ r • closedBall 0 1 = closedBall 0 r

Tactic:
rw [smul_unitClosedBall, Real.norm_of_nonneg hr]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_eq_one_iff_of_one_le [MulLeftMono α]
    [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
    a * b = 1 ↔ a = 1 ∧ b = 1 :=
  Iff.intro
    (fun hab : a * b = 1 =>
      have : a ≤ 1 := hab ▸ le_mul_of_le_of_one_le le_rfl hb
      have : a = 1 := le_antisymm this ha
      have : b ≤ 1 := hab ▸ le_mul_of_one_le_of_le ha le_rfl
      have : b = 1 := le_antisymm this hb
      And.intro ‹a = 1› ‹b = 1›)
    (by rintro ⟨rfl, rfl⟩; rw [mul_one])

Proof state:
case intro
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
ha hb : 1 ≤ 1
⊢ 1 * 1 = 1

Tactic:
rw [mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a = 1 ∧ b = 1 → a * b = 1

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
ha hb : 1 ≤ 1
⊢ 1 * 1 = 1
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem lcm_zero_left (x : R) : lcm 0 x = 0

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm 0 x = 0

Tactic:
rw [lcm, zero_mul, zero_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a

Proof state:
a b : Int
Ha : 0 ≤ a
this : a / b ≤ ↑a.natAbs
⊢ a / b ≤ a

Tactic:
rwa [natAbs_of_nonneg Ha] at this

Result:
no goals

Proof state:
a b : Int
Ha : 0 ≤ a
⊢ a / b ≤ a

Tactic:
have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_div_le_natAbs a b)

Result:
a b : Int
Ha : 0 ≤ a
this : a / b ≤ ↑a.natAbs
⊢ a / b ≤ a
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem div_ball_one : s / ball 1 δ = thickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s / ball 1 δ = thickening δ s

Tactic:
simp [div_eq_mul_inv, mul_ball_one]

Result:
no goals
-- Mathlib/Data/List/Palindrome.lean
theorem map (f : α → β) (p : Palindrome l) : Palindrome (map f l) :=
  of_reverse_eq <| by rw [← map_reverse, p.reverse_eq]

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p : l.Palindrome
⊢ (map f l).reverse = map f l

Tactic:
rw [← map_reverse, p.reverse_eq]

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem mem_inf (x : L) : x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
x : L
⊢ x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'

Tactic:
rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule,
  Submodule.mem_inf]

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem asModuleEquiv_symm_map_smul (r : k) (x : V) :
    ρ.asModuleEquiv.symm (r • x) = algebraMap k (MonoidAlgebra k G) r • ρ.asModuleEquiv.symm x

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
x : V
⊢ ρ.asModuleEquiv.symm (r • x) = (algebraMap k (MonoidAlgebra k G)) r • ρ.asModuleEquiv.symm x

Tactic:
apply_fun ρ.asModuleEquiv

Result:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
x : V
⊢ ρ.asModuleEquiv (ρ.asModuleEquiv.symm (r • x)) =
    ρ.asModuleEquiv ((algebraMap k (MonoidAlgebra k G)) r • ρ.asModuleEquiv.symm x)

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
x : V
⊢ ρ.asModuleEquiv (ρ.asModuleEquiv.symm (r • x)) =
    ρ.asModuleEquiv ((algebraMap k (MonoidAlgebra k G)) r • ρ.asModuleEquiv.symm x)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem ι_apply (x : ⨁ i, A i) :
  ⟨Quot.mk (Rel <| rel R A) (TensorAlgebra.ι R x)⟩ = ι' R A x

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
x : ⨁ (i : I), A i
⊢ { toQuot := Quot.mk (RingQuot.Rel (rel R A)) ((ι R) x) } = (ι' R A) x

Tactic:
aesop (add simp [ι', mkAlgHom, RingQuot.mkAlgHom, mkRingHom])

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem abs_arg_lt_pi_div_two_iff {z : ℂ} : |arg z| < π / 2 ↔ 0 < re z ∨ z = 0

Proof state:
case inl
z : ℂ
hz : z = 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
simp [hz]

Result:
no goals

Proof state:
z : ℂ
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
rcases eq_or_ne z 0 with hz | hz

Result:
case inl
z : ℂ
hz : z = 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Proof state:
case inr
z : ℂ
hz : z ≠ 0
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0

Tactic:
simp_rw [hz, or_false, ← not_lt, not_and_self_iff, or_false]

Result:
no goals

Proof state:
z : ℂ
⊢ |z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0

Tactic:
rw [abs_lt, arg_lt_pi_div_two_iff, neg_pi_div_two_lt_arg_iff, ← or_and_left]

Result:
z : ℂ
⊢ 0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
-- Mathlib/Tactic/NormNum/Pow.lean
theorem IsNatPowT.bit1 :
    IsNatPowT (Nat.pow a b = c) a (nat_lit 2 * b + nat_lit 1) (Nat.mul c (Nat.mul c a)) :=
  ⟨fun h1 => by simp [two_mul, pow_add, mul_assoc, ← h1]⟩

Proof state:
a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b + 1) = c.mul (c.mul a)

Tactic:
simp [two_mul, pow_add, mul_assoc, ← h1]

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem disjoint_ndinsert_right {a : α} {s t : Multiset α} :
    Disjoint s (ndinsert a t) ↔ a ∉ s ∧ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ _root_.Disjoint s (ndinsert a t) ↔ a ∉ s ∧ _root_.Disjoint s t

Tactic:
rw [_root_.disjoint_comm, disjoint_ndinsert_left]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ∉ s ∧ _root_.Disjoint t s ↔ a ∉ s ∧ _root_.Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ∉ s ∧ _root_.Disjoint t s ↔ a ∉ s ∧ _root_.Disjoint s t

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_neg (x y : R) (p : R[X][Y]) : (-p).evalEval x y = -p.evalEval x y

Proof state:
R : Type u_1
inst✝ : Ring R
x y : R
p : R[X][Y]
⊢ evalEval x y (-p) = -evalEval x y p

Tactic:
simp only [evalEval, eval_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem of_mem_zip {a b} {l₁ : Vector α n} {l₂ : Vector β n} : (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : Array α
l₂ : Vector β l₁.size
⊢ (a, b) ∈ { toArray := l₁, size_toArray := ⋯ }.zip l₂ → a ∈ { toArray := l₁, size_toArray := ⋯ } ∧ b ∈ l₂

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ (a, b) ∈ { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } →
    a ∈ { toArray := l₁, size_toArray := ⋯ } ∧ b ∈ { toArray := l₂, size_toArray := h }

Proof state:
α : Type u_1
n : Nat
β : Type u_2
a : α
b : β
l₁ : Vector α n
l₂ : Vector β n
⊢ (a, b) ∈ l₁.zip l₂ → a ∈ l₁ ∧ b ∈ l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : Array α
l₂ : Vector β l₁.size
⊢ (a, b) ∈ { toArray := l₁, size_toArray := ⋯ }.zip l₂ → a ∈ { toArray := l₁, size_toArray := ⋯ } ∧ b ∈ l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
a : α
b : β
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ (a, b) ∈ { toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h } →
    a ∈ { toArray := l₁, size_toArray := ⋯ } ∧ b ∈ { toArray := l₂, size_toArray := h }

Tactic:
simpa using Array.of_mem_zip

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_univ_two (a b : ℕ) :
    multinomial Finset.univ ![a, b] = (a + b)! / (a ! * b !)

Proof state:
a b : ℕ
⊢ multinomial univ ![a, b] = (a + b)! / (a ! * b !)

Tactic:
rw [multinomial, Fin.sum_univ_two, Fin.prod_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one,
  Matrix.head_cons]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P4_neg_right : P4 x₁ x₂ y ↔ P4 x₁ x₂ (-y)

Proof state:
x₁ x₂ y : PGame
⊢ P4 x₁ x₂ y ↔ P4 x₁ x₂ (-y)

Tactic:
rw [P4, P4, neg_neg, and_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Iic : ((↑) : ℤ → α) ⁻¹' Set.Iic a = Set.Iic ⌊a⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ Int.cast ⁻¹' Iic a = Iic ⌊a⌋

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Iic a ↔ x✝ ∈ Iic ⌊a⌋

Tactic:
simp [le_floor]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_lt_of_lt_div (h : a < b / c) : a * c < b

Proof state:
a b c : ℝ≥0∞
h : a < b / c
⊢ a * c < b

Tactic:
contrapose! h

Result:
a b c : ℝ≥0∞
h : b ≤ a * c
⊢ b / c ≤ a

Proof state:
a b c : ℝ≥0∞
h : b ≤ a * c
⊢ b / c ≤ a

Tactic:
exact ENNReal.div_le_of_le_mul h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_mul_le_iff₀` for a version with multiplication on the other side. -/
lemma inv_mul_le_iff₀' (hc : 0 < c) : c⁻¹ * b ≤ a ↔ b ≤ a * c

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b ≤ a ↔ b ≤ a * c

Tactic:
rw [inv_mul_le_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem support_uniformOfFinset : (uniformOfFinset s hs).support = s :=
  Set.ext
    (by
      let ⟨a, ha⟩ := hs
      simp [mem_support_iff, Finset.ne_empty_of_mem ha])

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ (uniformOfFinset s ⋯).support ↔ x ∈ ↑s

Tactic:
simp [mem_support_iff, Finset.ne_empty_of_mem ha]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ (x : α), x ∈ (uniformOfFinset s hs).support ↔ x ∈ ↑s

Tactic:
let ⟨a, ha⟩ := hs

Result:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ (uniformOfFinset s ⋯).support ↔ x ∈ ↑s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_sub_le (a b : Int) : natAbs (a - b) ≤ natAbs a + natAbs b

Proof state:
a b : Int
⊢ (a - b).natAbs ≤ a.natAbs + b.natAbs

Tactic:
rw [← Int.natAbs_neg b]

Result:
a b : Int
⊢ (a - b).natAbs ≤ a.natAbs + (-b).natAbs

Proof state:
a b : Int
⊢ (a - b).natAbs ≤ a.natAbs + (-b).natAbs

Tactic:
apply natAbs_add_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_const_fun (x : β) : map (Function.const α x) = (replicate ·.length x)

Proof state:
case h
β : Type u_1
α : Type u_2
x : β
l : List α
⊢ map (Function.const α x) l = replicate l.length x

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
x : β
⊢ map (Function.const α x) = fun x_1 => replicate x_1.length x

Tactic:
funext l

Result:
case h
β : Type u_1
α : Type u_2
x : β
l : List α
⊢ map (Function.const α x) l = replicate l.length x