harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PNat/Xgcd.lean
theorem gcdA'_coe : (gcdA' a b : ℕ) = gcdW a b + gcdX a b

Proof state:
a b : ℕ+
⊢ ↑(a.gcdA' b) = ↑(a.gcdW b) + a.gcdX b

Tactic:
dsimp [gcdA', gcdX, gcdW, XgcdType.w]

Result:
a b : ℕ+
⊢ (a.xgcd b).wp + (a.xgcd b).x + 1 = (a.xgcd b).wp + 1 + (a.xgcd b).x

Proof state:
a b : ℕ+
⊢ (a.xgcd b).wp + (a.xgcd b).x + 1 = (a.xgcd b).wp + 1 + (a.xgcd b).x

Tactic:
rw [add_right_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem integrable_approxOn_range [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    [SeparableSpace (range f ∪ {0} : Set E)] (hf : Integrable f μ) (n : ℕ) :
    Integrable (approxOn f fmeas (range f ∪ {0}) 0 (by simp) n) μ :=
  integrable_approxOn fmeas hf _ (integrable_zero _ _ _) n

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : Integrable f μ
n : ℕ
⊢ 0 ∈ Set.range f ∪ {0}

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsInfix.ne_nil {x y : List α} (h : x <:+: y) (hx : x ≠ []) : y ≠ []

Proof state:
α : Type u_1
x : List α
hx : x ≠ []
h : x <:+: []
⊢ False

Tactic:
exact hx <| List.infix_nil.mp h

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <:+: y
hx : x ≠ []
⊢ y ≠ []

Tactic:
rintro rfl

Result:
α : Type u_1
x : List α
hx : x ≠ []
h : x <:+: []
⊢ False
-- Mathlib/Data/Nat/ModEq.lean
theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n

Proof state:
case intro
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.Coprime n

Tactic:
rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]

Result:
case intro
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 1 ≡ 0 [MOD a.gcd n]

Proof state:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 0 * b = 0

Tactic:
rw [zero_mul]

Result:
no goals

Proof state:
b a n : ℕ
h : a * b ≡ 1 [MOD n]
⊢ a.Coprime n

Tactic:
obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n

Result:
case intro
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ a.Coprime n

Proof state:
case intro
b a n : ℕ
h : a * b ≡ 1 [MOD n]
g : ℕ
hh : n = a.gcd n * g
⊢ 1 ≡ 0 [MOD a.gcd n]

Tactic:
calc
  1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
  _ ≡ 0 * b [MOD a.gcd n] := (Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b
  _ = 0 := by rw [zero_mul]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem of_injective [MulOneClass G] [Nontrivial k] :
    Function.Injective (of k G) := fun a b h => by
  simpa using (single_eq_single_iff _ _ _ _).mp h

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Nontrivial k
a b : G
h : (of k G) a = (of k G) b
⊢ a = b

Tactic:
simpa using (single_eq_single_iff _ _ _ _).mp h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_const_cpow {a b : ℂ} (ha : a ≠ 0) : ContinuousAt (fun x : ℂ => a ^ x) b

Proof state:
case h
a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = cexp (Complex.log a * b)

Tactic:
rw [cpow_def_of_ne_zero ha]

Result:
no goals

Proof state:
a b : ℂ
ha : a ≠ 0
⊢ (fun x => a ^ x) = fun x => cexp (Complex.log a * x)

Tactic:
ext1 b

Result:
case h
a b✝ : ℂ
ha : a ≠ 0
b : ℂ
⊢ a ^ b = cexp (Complex.log a * b)

Proof state:
a b : ℂ
ha : a ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) := by
  ext1 b
  rw [cpow_def_of_ne_zero ha]

Result:
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => cexp (Complex.log a * x)
⊢ ContinuousAt (fun x => a ^ x) b

Proof state:
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => cexp (Complex.log a * x)
⊢ ContinuousAt (fun x => cexp (Complex.log a * x)) b

Tactic:
exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)

Result:
no goals

Proof state:
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => cexp (Complex.log a * x)
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
rw [cpow_eq]

Result:
a b : ℂ
ha : a ≠ 0
cpow_eq : (fun x => a ^ x) = fun x => cexp (Complex.log a * x)
⊢ ContinuousAt (fun x => cexp (Complex.log a * x)) b
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Mem_reverse [@OrientedCmp α cmp] {t : RBNode α} :
    Mem cmp x t.reverse ↔ Mem (flip cmp) x t

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ MemP (fun x_1 => (cmp x x_1).swap) t ↔ MemP (flip cmp x) t

Tactic:
apply Iff.of_eq

Result:
case h
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ MemP (fun x_1 => (cmp x x_1).swap) t = MemP (flip cmp x) t

Proof state:
case h.e_cut.h
α : Type u_1
cmp : α → α → Ordering
x✝ : α
inst✝ : OrientedCmp cmp
t : RBNode α
x : α
⊢ (cmp x✝ x).swap = flip cmp x✝ x

Tactic:
rw [OrientedCmp.symm]

Result:
case h.e_cut.h
α : Type u_1
cmp : α → α → Ordering
x✝ : α
inst✝ : OrientedCmp cmp
t : RBNode α
x : α
⊢ cmp x x✝ = flip cmp x✝ x

Proof state:
case h.e_cut
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ (fun x_1 => (cmp x x_1).swap) = flip cmp x

Tactic:
funext x

Result:
case h.e_cut.h
α : Type u_1
cmp : α → α → Ordering
x✝ : α
inst✝ : OrientedCmp cmp
t : RBNode α
x : α
⊢ (cmp x✝ x).swap = flip cmp x✝ x

Proof state:
case h
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ MemP (fun x_1 => (cmp x x_1).swap) t = MemP (flip cmp x) t

Tactic:
congr

Result:
case h.e_cut
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ (fun x_1 => (cmp x x_1).swap) = flip cmp x

Proof state:
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ Mem cmp x t.reverse ↔ Mem (flip cmp) x t

Tactic:
simp [Mem]

Result:
α : Type u_1
cmp : α → α → Ordering
x : α
inst✝ : OrientedCmp cmp
t : RBNode α
⊢ MemP (fun x_1 => (cmp x x_1).swap) t ↔ MemP (flip cmp x) t

Proof state:
case h.e_cut.h
α : Type u_1
cmp : α → α → Ordering
x✝ : α
inst✝ : OrientedCmp cmp
t : RBNode α
x : α
⊢ cmp x x✝ = flip cmp x✝ x

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem powerSeriesFamily_smul (r : R) :
    powerSeriesFamily hx (r • f) = HahnSeries.single (0 : Γ) r • powerSeriesFamily hx f

Proof state:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
f : PowerSeries R
r : R
n : ℕ
⊢ (powerSeriesFamily hx (r • f)) n = ((HahnSeries.single 0) r • powerSeriesFamily hx f) n

Tactic:
simp [mul_smul]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
f : PowerSeries R
r : R
⊢ powerSeriesFamily hx (r • f) = (HahnSeries.single 0) r • powerSeriesFamily hx f

Tactic:
ext1 n

Result:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
f : PowerSeries R
r : R
n : ℕ
⊢ (powerSeriesFamily hx (r • f)) n = ((HahnSeries.single 0) r • powerSeriesFamily hx f) n
-- Mathlib/RingTheory/Jacobson/Semiprimary.lean
theorem IsSemisimpleModule.jacobson_le_annihilator [IsSemisimpleModule R M] :
    Ring.jacobson R ≤ Module.annihilator R M :=
  fun r hr ↦ Module.mem_annihilator.mpr fun m ↦ by
    have := Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr
    rwa [jacobson_eq_bot] at this

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
r : R
hr : r ∈ Ring.jacobson R
m : M
this : r ∈ Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)
⊢ r • m = 0

Tactic:
rwa [jacobson_eq_bot] at this

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
r : R
hr : r ∈ Ring.jacobson R
m : M
⊢ r • m = 0

Tactic:
have := Module.le_comap_jacobson (LinearMap.toSpanSingleton R M m) hr

Result:
R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
r : R
hr : r ∈ Ring.jacobson R
m : M
this : r ∈ Submodule.comap (LinearMap.toSpanSingleton R M m) (Module.jacobson R M)
⊢ r • m = 0
-- Mathlib/Topology/ContinuousMap/Units.lean
theorem continuous_isUnit_unit {f : C(X, R)} (h : ∀ x, IsUnit (f x)) :
    Continuous fun x => (h x).unit

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse ↑⋯.unit
⊢ ContinuousAt (fun x => ↑((fun x => ⋯.unit) x)⁻¹) x

Tactic:
simp only

Result:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse ↑⋯.unit
⊢ ContinuousAt (fun x => ↑⋯.unit⁻¹) x

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse ↑⋯.unit
⊢ ContinuousAt (fun x => ↑⋯.unit⁻¹) x

Tactic:
simp only [← Ring.inverse_unit, IsUnit.unit_spec] at this ⊢

Result:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse (f x)
⊢ ContinuousAt (fun x => Ring.inverse (f x)) x

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
⊢ Continuous fun x => ⋯.unit

Tactic:
refine
  continuous_induced_rng.2
    (Continuous.prod_mk f.continuous
      (MulOpposite.continuous_op.comp (continuous_iff_continuousAt.mpr fun x => ?_)))

Result:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
⊢ ContinuousAt (fun x => ↑((fun x => ⋯.unit) x)⁻¹) x

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
⊢ ContinuousAt (fun x => ↑((fun x => ⋯.unit) x)⁻¹) x

Tactic:
have := NormedRing.inverse_continuousAt (h x).unit

Result:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse ↑⋯.unit
⊢ ContinuousAt (fun x => ↑((fun x => ⋯.unit) x)⁻¹) x

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
x : X
this : ContinuousAt Ring.inverse (f x)
⊢ ContinuousAt (fun x => Ring.inverse (f x)) x

Tactic:
exact this.comp (f.continuousAt x)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma image_iterate_eq {f : α → α} {n : ℕ} : image (f^[n]) = (image f)^[n]

Proof state:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]

Tactic:
rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

Result:
no goals

Proof state:
case zero
α : Type u_1
f : α → α
⊢ image f^[0] = (image f)^[0]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : ℕ
⊢ image f^[n] = (image f)^[n]

Tactic:
induction n with
| zero => simp
| succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sq_sin_pi_div_three : sin (π / 3) ^ 2 = 3 / 4

Proof state:
case e_a.e_x

⊢ π / 2 - π / 3 = π / 6

Tactic:
ring

Result:
no goals

Proof state:
⊢ sin (π / 3) ^ 2 = 3 / 4

Tactic:
rw [← cos_pi_div_two_sub, ← sq_cos_pi_div_six]

Result:
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2

Proof state:
⊢ cos (π / 2 - π / 3) ^ 2 = cos (π / 6) ^ 2

Tactic:
congr

Result:
case e_a.e_x

⊢ π / 2 - π / 3 = π / 6
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_hcongr {β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β')
    (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (map f m) (map f' m)

Proof state:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ a ∈ m, HEq (f a) (f' a)
⊢ HEq (map f m) (map f' m)

Tactic:
simp at hf

Result:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ a ∈ m, f a = f' a
⊢ HEq (map f m) (map f' m)

Proof state:
α : Type u_1
β β' : Type v
m : Multiset α
f : α → β
f' : α → β'
h : β = β'
hf : ∀ a ∈ m, HEq (f a) (f' a)
⊢ HEq (map f m) (map f' m)

Tactic:
subst h

Result:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ a ∈ m, HEq (f a) (f' a)
⊢ HEq (map f m) (map f' m)

Proof state:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ a ∈ m, f a = f' a
⊢ HEq (map f m) (map f' m)

Tactic:
simp [map_congr rfl hf]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem codisjoint_hnot_hnot_left_iff : Codisjoint (￢￢a) b ↔ Codisjoint a b

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
⊢ Codisjoint (￢￢a) b ↔ Codisjoint a b

Tactic:
simp_rw [← hnot_le_iff_codisjoint_right, hnot_hnot_hnot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatten_mkVector_singleton : (mkVector n #v[a]).flatten = (mkVector n a).cast (by simp)

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (mkVector n { toArray := #[a], size_toArray := ⋯ }).flatten = Vector.cast ⋯ (mkVector n a)

Tactic:
ext i h

Result:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n * 1
⊢ (mkVector n { toArray := #[a], size_toArray := ⋯ }).flatten[i] = (Vector.cast ⋯ (mkVector n a))[i]

Proof state:
n : Nat
a : ?m.348968
⊢ n = n * 1

Tactic:
simp

Result:
no goals

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
h : i < n * 1
⊢ (mkVector n { toArray := #[a], size_toArray := ⋯ }).flatten[i] = (Vector.cast ⋯ (mkVector n a))[i]

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem LinearOrder.strictConvexOn_of_lt (hs : Convex 𝕜 s)
    (hf : ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 →
      f (a • x + b • y) < a • f x + b • f y) :
    StrictConvexOn 𝕜 s f

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • y) < a • f x + b • f y

Tactic:
wlog h : x < y

Result:
case inr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
this :
  ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E]
    [inst_2 : OrderedAddCommMonoid β] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 β] [inst_5 : LinearOrder E] {s : Set E}
    {f : E → β},
    Convex 𝕜 s →
      (∀ ⦃x : E⦄,
          x ∈ s →
            ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y) →
        ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∀ (a b : 𝕜), 0 < a → 0 < b → a + b = 1 → x < y → f (a • x + b • y) < a • f x + b • f y
h : ¬x < y
⊢ f (a • x + b • y) < a • f x + b • f y

𝕜✝ : Type u_1
E✝ : Type u_2
β✝ : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜✝
inst✝¹⁰ : AddCommMonoid E✝
inst✝⁹ : OrderedAddCommMonoid β✝
inst✝⁸ : Module 𝕜✝ E✝
inst✝⁷ : Module 𝕜✝ β✝
inst✝⁶ : LinearOrder E✝
s✝ : Set E✝
f✝ : E✝ → β✝
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : LinearOrder E
s : Set E
f : E → β
hs : Convex 𝕜 s
hf :
  ∀ ⦃x : E⦄,
    x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < a • f x + b • f y
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : x < y
⊢ f (a • x + b • y) < a • f x + b • f y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/Lemmas.lean
theorem getD_unitOfList
    {l : List α} {k : α} {fallback : Unit} :
    getD (unitOfList l) k fallback = ()

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
l : List α
k : α
fallback : Unit
⊢ (unitOfList l).getD k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem mem_or_mem_of_zipWith_swap_prod_ne : ∀ {l l' : List α} {x : α},
    (zipWith swap l l').prod x ≠ x → x ∈ l ∨ x ∈ l'
  | [], _, _ => by simp
  | _, [], _ => by simp
  | a::l, b::l', x => fun hx ↦
    if h : (zipWith swap l l').prod x = x then
      (eq_or_eq_of_swap_apply_ne_self (a := a) (b := b) (x := x) (by simpa [h] using hx)).imp
        (by rintro rfl; exact .head _) (by rintro rfl; exact .head _)
    else
     (mem_or_mem_of_zipWith_swap_prod_ne h).imp (.tail _) (.tail _)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith swap l l').prod x = x
⊢ x = a → x ∈ a :: l

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
b : α
l' : List α
x : α
h : (zipWith swap l l').prod x = x
hx : (zipWith swap (x :: l) (b :: l')).prod x ≠ x
⊢ x ∈ x :: l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith swap l l').prod x = x
⊢ (swap a b) x ≠ x

Tactic:
simpa [h] using hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : (zipWith swap (a :: l) (b :: l')).prod x ≠ x
h : (zipWith swap l l').prod x = x
⊢ x = b → x ∈ b :: l'

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l l' : List α
x : α
h : (zipWith swap l l').prod x = x
hx : (zipWith swap (a :: l) (x :: l')).prod x ≠ x
⊢ x ∈ x :: l'

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x✝¹ : List α
x✝ : α
⊢ (zipWith swap [] x✝¹).prod x✝ ≠ x✝ → x✝ ∈ [] ∨ x✝ ∈ x✝¹

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x✝¹ : List α
x✝ : α
⊢ (zipWith swap x✝¹ []).prod x✝ ≠ x✝ → x✝ ∈ x✝¹ ∨ x✝ ∈ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
b : α
l' : List α
x : α
h : (zipWith swap l l').prod x = x
hx : (zipWith swap (x :: l) (b :: l')).prod x ≠ x
⊢ x ∈ x :: l

Tactic:
exact .head _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l l' : List α
x : α
h : (zipWith swap l l').prod x = x
hx : (zipWith swap (a :: l) (x :: l')).prod x ≠ x
⊢ x ∈ x :: l'

Tactic:
exact .head _

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem algebraMap_image (h : QuasispectrumRestricts a f) :
    algebraMap R S '' quasispectrum R a = quasispectrum S a

Proof state:
case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a ⊆ quasispectrum S a

Tactic:
simpa only [quasispectrum.preimage_algebraMap] using
  (quasispectrum S a).image_preimage_subset (algebraMap R S)

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a

Tactic:
refine Set.eq_of_subset_of_subset ?_ fun s hs => ⟨f s, ?_⟩

Result:
case refine_1
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
⊢ ⇑(algebraMap R S) '' quasispectrum R a ⊆ quasispectrum S a

case refine_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a ∧ (algebraMap R S) (f s) = s

Proof state:
case refine_2
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Algebra R S
a : A
f : S → R
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
h : QuasispectrumRestricts a f
s : S
hs : s ∈ quasispectrum S a
⊢ f s ∈ quasispectrum R a ∧ (algebraMap R S) (f s) = s

Tactic:
exact ⟨quasispectrum.of_algebraMap_mem S ((h.rightInvOn hs).symm ▸ hs), h.rightInvOn hs⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod {m : Fin n → 𝕜} :
    (iteratedFDerivWithin 𝕜 n f s x : (Fin n → 𝕜) → F) m =
      (∏ i, m i) • iteratedDerivWithin n f s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDerivWithin 𝕜 n f s x) m = (∏ i : Fin n, m i) • iteratedDerivWithin n f s x

Tactic:
rw [iteratedDerivWithin_eq_iteratedFDerivWithin, ← ContinuousMultilinearMap.map_smul_univ]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDerivWithin 𝕜 n f s x) m = (iteratedFDerivWithin 𝕜 n f s x) fun i => m i • 1

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
m : Fin n → 𝕜
⊢ (iteratedFDerivWithin 𝕜 n f s x) m = (iteratedFDerivWithin 𝕜 n f s x) fun i => m i • 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_mul_natCast (x : ℝ≥0) (y : ℝ) (n : ℕ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x : ℝ≥0
y : ℝ
n : ℕ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_natCast]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isCharThreeJNeZeroNF : W.c₄ = 16 * W.a₂ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.c₄ = 16 * W.a₂ ^ 2

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma measure_symmDiff_eq (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) :
    μ (s ∆ t) = μ (s \ t) + μ (t \ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ μ (s ∆ t) = μ (s \ t) + μ (t \ s)

Tactic:
simpa only [symmDiff_def, sup_eq_union]
  using measure_union₀ (ht.diff hs) disjoint_sdiff_sdiff.aedisjoint

Result:
no goals