harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem parallelepiped_single [DecidableEq ι] (a : ι → ℝ) :
    (parallelepiped fun i => Pi.single i (a i)) = Set.uIcc 0 a

Proof state:
case h.mp.intro.intro
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
ht : ∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1
i : ι
⊢ 0 ⊓ a i ≤ (t • a) i ∧ (t • a) i ≤ 0 ⊔ a i

Tactic:
specialize ht i

Result:
case h.mp.intro.intro
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
⊢ 0 ⊓ a i ≤ (t • a) i ∧ (t • a) i ≤ 0 ⊔ a i

Proof state:
case h.mpr.refine_2.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 = x i
hai : a i = 0
⊢ x i = x i / a i * a i

Tactic:
rw [hai, ← h, zero_div, zero_mul]

Result:
no goals

Proof state:
case h.mpr.refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
i : ι
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1

Tactic:
specialize h i

Result:
case h.mpr.refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1

Proof state:
case h.mp.intro.intro.inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
⊢ a i ≤ t i * a i ∧ t i * a i ≤ 0

Tactic:
exact ⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩

Result:
no goals

Proof state:
case h.mpr.refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
⊢ x i = ((fun i => x i / a i) • a) i

Tactic:
simp only [smul_eq_mul, Pi.mul_apply]

Result:
case h.mpr.refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
⊢ x i = x i / a i * a i

Proof state:
case h.mp.intro.intro.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
⊢ 0 ≤ t i * a i ∧ t i * a i ≤ a i

Tactic:
exact ⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩

Result:
no goals

Proof state:
case h.mpr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
⊢ ∃ t, (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a

Tactic:
refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩

Result:
case h.mpr.refine_1
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
i : ι
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1

case h.mpr.refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
i : ι
⊢ x i = ((fun i => x i / a i) • a) i

Proof state:
case h.mpr.refine_2.inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
hai : a i ≠ 0
⊢ x i = x i / a i * a i

Tactic:
rw [div_mul_cancel₀ _ hai]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma desc_var (s : relations.Solution N) (g : relations.G) :
    h.desc s (solution.var g) = s.var g

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
g : relations.G
⊢ s.fromQuotient (h.linearEquiv.symm (solution.var g)) = s.var g

Tactic:
simp only [linearEquiv_symm_var, fromQuotient_toQuotient, π_single]

Result:
no goals

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
g : relations.G
⊢ (h.desc s) (solution.var g) = s.var g

Tactic:
dsimp [desc]

Result:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
g : relations.G
⊢ s.fromQuotient (h.linearEquiv.symm (solution.var g)) = s.var g
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
theorem comp_deterministic_eq_comap (κ : Kernel α β) (hg : Measurable g) :
    κ ∘ₖ deterministic g hg = comap κ g hg

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((κ ∘ₖ deterministic g hg) a) s = ((κ.comap g hg) a) s

Tactic:
simp_rw [comap_apply' _ _ _ s, comp_apply' _ _ _ hs, deterministic_apply hg a,
  lintegral_dirac' _ (Kernel.measurable_coe κ hs)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
⊢ κ ∘ₖ deterministic g hg = κ.comap g hg

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((κ ∘ₖ deterministic g hg) a) s = ((κ.comap g hg) a) s
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.preimage_isClosed_of_isClosed {t : Set β}
    (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ f ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
⊢ IsClosed (s ∩ f ⁻¹' t)

Tactic:
rcases continuousOn_iff_isClosed.1 hf t ht with ⟨u, hu⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
u : Set α
hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed (s ∩ f ⁻¹' t)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
u : Set α
hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed (u ∩ s)

Tactic:
apply IsClosed.inter hu.1 hs

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
u : Set α
hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed (s ∩ f ⁻¹' t)

Tactic:
rw [inter_comm, hu.2]

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
hf : ContinuousOn f s
hs : IsClosed s
ht : IsClosed t
u : Set α
hu : IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
⊢ IsClosed (u ∩ s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem modify_toArray (f : α → α) (l : List α) :
    l.toArray.modify i f = (l.modify f i).toArray

Proof state:
case h
α : Type u_1
i : Nat
f : α → α
l : List α
⊢ (l.toArray.modify i f).toList = (modify f i l).toArray.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
i : Nat
f : α → α
l : List α
⊢ l.toArray.modify i f = (modify f i l).toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
i : Nat
f : α → α
l : List α
⊢ (l.toArray.modify i f).toList = (modify f i l).toArray.toList
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem closure_setOf_lt_im (a : ℝ) : closure { z : ℂ | a < z.im } = { z | a ≤ z.im }

Proof state:
a : ℝ
⊢ closure {z | a < z.im} = {z | a ≤ z.im}

Tactic:
simpa only [closure_Ioi] using closure_preimage_im (Ioi a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_map_toArray (l : List (List α)) :
    (l.toArray.map List.toArray).flatten = l.flatten.toArray

Proof state:
case h
α : Type u_1
l : List (List α)
⊢ (map List.toArray l.toArray).flatten.toList = l.flatten.toArray.toList

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
l : List (List α)
⊢ (map List.toArray l.toArray).flatten = l.flatten.toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List (List α)
⊢ (map List.toArray l.toArray).flatten.toList = l.flatten.toArray.toList
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_mul (I J : Ideal S) : spanNorm R (I * J) = spanNorm R I * spanNorm R J

Proof state:
case neg
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this : IsDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Tactic:
have : IsDedekindDomain Sₚ := IsLocalization.isDedekindDomain S h _

Result:
case neg
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
P : Ideal R
hP : P.IsMaximal
hP0 : ¬P = ⊥
P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl
Rₚ : Type u_1 := Localization.AtPrime P
Sₚ : Type u_3 := Localization P'
x✝ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
this✝¹ : IsScalarTower R Rₚ Sₚ
h : P' ≤ S⁰
this✝ : IsDomain Sₚ
this : IsDedekindDomain Sₚ
⊢ map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) =
    map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)

Proof state:
case pos.eq_bot_or_top
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
⊢ ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤

Tactic:
intro I

Result:
case pos.eq_bot_or_top
R : Type u_1
inst✝¹² : CommRing R
inst✝¹¹ : IsDomain R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : IsDomain S
inst✝⁸ : IsIntegrallyClosed R
inst✝⁷ : IsIntegrallyClosed S
inst✝⁶ : Algebra R S
inst✝⁵ : Module.Finite R S
inst✝⁴ : NoZeroSMulDivisors R S
inst✝³ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
inst✝² : IsDedekindDomain R
inst✝¹ : IsDedekindDomain S
I✝ J : Ideal S
inst✝ : Nontrivial R
h✝ : Nontrivial S
hP : ⊥.IsMaximal
I : Ideal R
⊢ I = ⊥ ∨ I = ⊤
-- Mathlib/Order/Defs/LinearOrder.lean
lemma compare_eq_iff_eq : compare a b = .eq ↔ a = b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ False ↔ a = b

Tactic:
rw [false_iff]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ¬a = b

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b

Tactic:
case _ _ h => rwa [true_iff]

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : a = b
⊢ True ↔ a = b

Tactic:
rwa [true_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b

Tactic:
split_ifs <;> try simp only [reduceCtorEq]

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b

case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ¬a = b

Tactic:
exact ne_iff_lt_or_gt.2 <| .inl h

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq ↔ a = b

Tactic:
simp only [reduceCtorEq]

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : ¬a < b
h : ¬a = b
⊢ False ↔ a = b

Tactic:
rwa [false_iff]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝ : a < b
⊢ False ↔ a = b

case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b

Tactic:
case _ h   => rw [false_iff]; exact ne_iff_lt_or_gt.2 <| .inl h

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : a = b
⊢ True ↔ a = b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.eq ↔ a = b

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False ↔ a = b

Tactic:
case _ _ h => rwa [false_iff]

Result:
no goals
-- Mathlib/CategoryTheory/DiscreteCategory.lean
theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) :
    (Discrete.functor F).map f = 𝟙 (F i.as)

Proof state:
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
i : Discrete I
f : i ⟶ i
⊢ (functor F).map f = 𝟙 (F i.as)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.linear_image (hs : StarConvex 𝕜 x s) (f : E →ₗ[𝕜] F) :
    StarConvex 𝕜 (f x) (f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Tactic:
rintro _ ⟨y, hy, rfl⟩ a b ha hb hab

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ ⇑f '' s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ ⇑f '' s

Tactic:
exact ⟨a • x + b • y, hs hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/CauSeqFilter.lean
theorem CauSeq.cauchySeq (f : CauSeq β norm) : CauchySeq f

Proof state:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ (a, b) ∈ s

Tactic:
rw [← ha'2, ← hb'2]

Result:
case intro.intro.intro.right.mk.intro.intro.intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
a b : β
a' : ℕ
ha'1 : a' ≥ N
ha'2 : ↑f a' = a
b' : ℕ
hb'1 : b' ≥ N
hb'2 : ↑f b' = b
⊢ (↑f a', ↑f b') ∈ s

Proof state:
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s

Tactic:
rcases mem_uniformity_dist.1 hs with ⟨ε, ⟨hε, hεs⟩⟩

Result:
case intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
⊢ ∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s

Proof state:
case intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
⊢ ∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s

Tactic:
obtain ⟨N, hN⟩ := CauSeq.cauchy₂ f hε

Result:
case intro.intro.intro
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
ε : ℝ
hε : ε > 0
hεs : ∀ ⦃a b : β⦄, dist a b < ε → (a, b) ∈ s
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, ‖↑f j - ↑f k‖ < ε
⊢ ∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s

Proof state:
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
⊢ CauchySeq ↑f

Tactic:
refine cauchy_iff.2 ⟨by infer_instance, fun s hs => ?_⟩

Result:
β : Type v
inst✝ : NormedField β
f : CauSeq β norm
s : Set (β × β)
hs : s ∈ uniformity β
⊢ ∃ t ∈ map (↑f) atTop, t ×ˢ t ⊆ s
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_three_mul : cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2
⊢ cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) =
    2 * cos x * cos x * cos x + 2 * cos x * (1 - sin x ^ 2) - 3 * cos x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2
⊢ cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
rw [h2, cos_sq']

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2
⊢ cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) =
    2 * cos x * cos x * cos x + 2 * cos x * (1 - sin x ^ 2) - 3 * cos x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
have h1 : x + 2 * x = 3 * x := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos x * cos (2 * x) - sin x * sin (2 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
simp only [cos_two_mul, sin_two_mul, mul_add, mul_sub, mul_one, sq]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 4 * cos x ^ 3 - 3 * cos x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
have h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2 := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2
⊢ cos x * (2 * (cos x * cos x)) - cos x - sin x * (2 * sin x * cos x) = 4 * cos x ^ 3 - 3 * cos x

Proof state:
x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x

Tactic:
rw [← h1, cos_add x (2 * x)]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cos x * cos (2 * x) - sin x * sin (2 * x) = 4 * cos x ^ 3 - 3 * cos x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldr_attach (l : Array α) (f : α → β → β) (b : β) :
    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
⊢ List.foldr f b (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = List.foldr f b l

Tactic:
congr

Result:
case mk.e_a
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
⊢ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = l

Proof state:
case mk.e_a
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
⊢ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = l

Tactic:
ext

Result:
case mk.e_a.h.a
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
i✝ : Nat
a✝ : α
⊢ a✝ ∈ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach[i✝]? ↔ a✝ ∈ l[i✝]?

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

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
⊢ foldr (fun t acc => f t.val acc) b { toList := l }.attach = foldr f b { toList := l }

Proof state:
case mk.e_a.h.a
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
i✝ : Nat
a✝ : α
⊢ a✝ ∈ (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach[i✝]? ↔ a✝ ∈ l[i✝]?

Tactic:
simpa using fun a => List.mem_of_getElem? a

Result:
no goals

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

Tactic:
simp only [List.attach_toArray, List.attachWith_mem_toArray, List.map_attach, size_toArray,
  List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
⊢ List.foldr f b (List.pmap (fun a h => ⟨a, ⋯⟩) l ⋯).unattach = List.foldr f b l