harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_map_mul (a : α) (s : Multiset α) : (s.map (a * ·)).gcd = normalize a * s.gcd

Proof state:
case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (map (fun x => a * x) s).gcd = GCDMonoid.gcd (a * b) (a * s.gcd)

Tactic:
rw [ih]

Result:
case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (normalize a * s.gcd) = GCDMonoid.gcd (a * b) (a * s.gcd)

Proof state:
case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x => a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd

Tactic:
simp_rw [map_cons, gcd_cons, ← gcd_mul_left]

Result:
case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (map (fun x => a * x) s).gcd = GCDMonoid.gcd (a * b) (a * s.gcd)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x => a * x) s).gcd = normalize a * s.gcd

Tactic:
refine s.induction_on ?_ fun b s ih ↦ ?_

Result:
case refine_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x => a * x) 0).gcd = normalize a * gcd 0

case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd
⊢ (map (fun x => a * x) (b ::ₘ s)).gcd = normalize a * (b ::ₘ s).gcd

Proof state:
case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s✝ : Multiset α
b : α
s : Multiset α
ih : (map (fun x => a * x) s).gcd = normalize a * s.gcd
⊢ GCDMonoid.gcd (a * b) (normalize a * s.gcd) = GCDMonoid.gcd (a * b) (a * s.gcd)

Tactic:
apply ((normalize_associated a).mul_right _).gcd_eq_right

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ (map (fun x => a * x) 0).gcd = normalize a * gcd 0

Tactic:
simp_rw [map_zero, gcd_zero, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isGE_iff (n : ℤ) :
    K.IsGE n ↔ ∀ (i : ℤ) (_ : i < n), K.ExactAt i

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n → ∀ i < n, ExactAt K i

Tactic:
intro _ i hi

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsGE n
i : ℤ
hi : i < n
⊢ ExactAt K i

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
⊢ K.IsGE n

Tactic:
refine IsSupported.mk (fun i hi ↦ ?_)

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ ExactAt K i

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
a✝ : K.IsGE n
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
exact K.exactAt_of_isGE n i hi

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, ExactAt K i) → K.IsGE n

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
⊢ K.IsGE n

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
exact h i hi

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i
⊢ ExactAt K i

Tactic:
rw [not_mem_range_embeddingUpIntGE_iff] at hi

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : i < n
⊢ ExactAt K i

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n ↔ ∀ i < n, ExactAt K i

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n → ∀ i < n, ExactAt K i

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ i < n, ExactAt K i) → K.IsGE n
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem log_rpow {x : ℝ} (hx : 0 < x) (y : ℝ) : log (x ^ y) = y * log x

Proof state:
x : ℝ
hx : 0 < x
y : ℝ
⊢ log (x ^ y) = y * log x

Tactic:
apply exp_injective

Result:
case a
x : ℝ
hx : 0 < x
y : ℝ
⊢ rexp (log (x ^ y)) = rexp (y * log x)

Proof state:
case a
x : ℝ
hx : 0 < x
y : ℝ
⊢ rexp (log (x ^ y)) = rexp (y * log x)

Tactic:
rw [exp_log (rpow_pos_of_pos hx y), ← exp_log hx, mul_comm, rpow_def_of_pos (exp_pos (log x)) y]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zero_zpow_eq (n : ℤ) : (0 : G₀) ^ n = if n = 0 then 1 else 0

Proof state:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

Tactic:
rw [h, zpow_zero]

Result:
no goals

Proof state:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
rw [zero_zpow _ h]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) :
    idealOfSet 𝕜 (setOfIdeal I) = I.closure

Proof state:
case intro.intro.intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ < ε

Tactic:
by_cases hx : x ∈ t

Result:
case pos
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∈ t
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ < ε

case neg
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
f : C(X, 𝕜)
hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)
ε : ℝ≥0
hε : 0 < ε
t : Set X := {x | ε / 2 ≤ ‖f x‖₊}
ht : IsClosed t
htI : Disjoint t (setOfIdeal I)ᶜ
g : C(X, ℝ≥0)
hgI : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I
hg : ∀ (x : X), g x ≤ 1
hgt : Set.EqOn (⇑g) 1 t
x : X
hx : x ∉ t
⊢ ‖f x - f x * ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g) x‖₊ < ε
-- Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean
theorem abs_discr_ge (h : 1 < finrank ℚ K) :
    (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K ≤ |discr K|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 4 / 9 * (3 * π / 4) ^ 2 = 16 / ((4 / π) ^ 2 * 4)

Tactic:
field_simp

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
x : 𝓞 K
h_nz : x ≠ 0
h_nm : 1 ≤ ↑|(Algebra.norm ℚ) ↑x|
h_bd :
  ↑(finrank ℚ K) ^ (finrank ℚ K * 2) / ((4 / π) ^ (nrComplexPlaces K * 2) * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|
a : ℕ → ℝ := fun n => ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n : ℕ
⊢ 4 * (3 * π) ^ 2 * (4 ^ 2 * 4) = 16 * π ^ 2 * (9 * 4 ^ 2)
-- Mathlib/RepresentationTheory/Character.lean
theorem char_iso {V W : FDRep k G} (i : V ≅ W) : V.character = W.character

Proof state:
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ (trace k ↑V.V) (V.ρ g) = (trace k ↑W.V) ((isoToLinearEquiv i).conj (V.ρ g))

Tactic:
exact (trace_conj' (V.ρ g) _).symm

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
⊢ V.character = W.character

Tactic:
ext g

Result:
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ V.character g = W.character g

Proof state:
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ V.character g = W.character g

Tactic:
simp only [character, FDRep.Iso.conj_ρ i]

Result:
case h
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ (trace k ↑V.V) (V.ρ g) = (trace k ↑W.V) ((isoToLinearEquiv i).conj (V.ρ g))
-- Mathlib/Algebra/DualNumber.lean
theorem lift_apply_eps
    (fe : {fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a)}) :
    lift fe (ε : A[ε]) = fe.val.2

Proof state:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
⊢ (lift fe) ε = (↑fe).2

Tactic:
simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, map_one, one_mul, zero_add]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma RightFraction.op_map
    {X Y : C} (φ : W.RightFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    (φ.map L hL).op = φ.op.map L.op hL.op

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (L.map φ.f).op ≫ (inv (L.map φ.s)).op = (L.map φ.f).op ≫ inv (L.map φ.s).op

Tactic:
rw [op_inv]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (φ.map L hL).op = φ.op.map L.op ⋯

Tactic:
dsimp [map, LeftFraction.map]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ (L.map φ.f).op ≫ (inv (L.map φ.s)).op = (L.map φ.f).op ≫ inv (L.map φ.s).op
-- Mathlib/Data/Semiquot.lean
theorem get_mem {q : Semiquot α} (p) : get q p ∈ q

Proof state:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.get p ∈ q

Tactic:
unfold get

Result:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q

Proof state:
α : Type u_1
q : Semiquot α
p : q.IsPure
⊢ q.get p ∈ q

Tactic:
let ⟨a, h⟩ := exists_mem q

Result:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.get p ∈ q

Proof state:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ q.liftOn id p ∈ q

Tactic:
rw [liftOn_ofMem q _ _ a h]

Result:
α : Type u_1
q : Semiquot α
p : q.IsPure
a : α
h : a ∈ q
⊢ id a ∈ q
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem lipschitzOnWith_of_nnnorm_hasFDerivWithin_le {C : ℝ≥0}
    (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C)
    (hs : Convex ℝ s) : LipschitzOnWith C f s

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

Tactic:
intro x x_in y y_in

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ ‖f x - f y‖ ≤ ↑C * ‖x - y‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ LipschitzOnWith C f s

Tactic:
rw [lipschitzOnWith_iff_norm_sub_le]

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
⊢ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
C : ℝ≥0
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖₊ ≤ C
hs : Convex ℝ s
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ ‖f x - f y‖ ≤ ↑C * ‖x - y‖

Tactic:
exact hs.norm_image_sub_le_of_norm_hasFDerivWithin_le hf bound y_in x_in

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem sum_le' {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α}
    (hF : ∀ i ∈ s, padicNorm p (F i) ≤ t) (ht : 0 ≤ t) : padicNorm p (∑ i ∈ s, F i) ≤ t

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ i ∈ ∅, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ ∅, F i) ≤ t

Tactic:
simp [ht]

Result:
no goals

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
exact sum_le hs hF

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t

Tactic:
obtain rfl | hs := Finset.eq_empty_or_nonempty s

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 ≤ t
hF : ∀ i ∈ ∅, padicNorm p (F i) ≤ t
⊢ padicNorm p (∑ i ∈ ∅, F i) ≤ t

case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) ≤ t
ht : 0 ≤ t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) ≤ t
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem comp_tensor_id (f : W ⟶ X) (g : X ⟶ Y) : f ≫ g ⊗ 𝟙 Z = (f ⊗ 𝟙 Z) ≫ (g ⊗ 𝟙 Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ f ≫ g ⊗ 𝟙 Z = (f ⊗ 𝟙 Z) ≫ (g ⊗ 𝟙 Z)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Max.lean
theorem not_isMin_iff : ¬IsMin a ↔ ∃ b, b < a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ¬IsMin a ↔ ∃ b, b < a

Tactic:
simp [lt_iff_le_not_le, IsMin, not_forall, exists_prop]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
/-- If `M` is a finite `R`-module, then the canonical map
`AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
lemma ofTensorProduct_surjective_of_finite [Module.Finite R M] :
    Function.Surjective (ofTensorProduct I M)

Proof state:
case hg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
hfg : f = g
⊢ Function.Surjective ⇑(map I p)

Tactic:
exact AdicCompletion.map_surjective I hp

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
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
⊢ f = g

Tactic:
ext

Result:
case a.h.h.h.h
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
i✝ : Fin n
n✝ : ℕ
⊢ ↑(((AlgebraTensorModule.curry f) 1 ∘ₗ LinearMap.single R (fun i => R) i✝) 1) n✝ =
    ↑(((AlgebraTensorModule.curry g) 1 ∘ₗ LinearMap.single R (fun i => R) i✝) 1) n✝

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
⊢ Function.Surjective ⇑(ofTensorProduct I M)

Tactic:
let g := map I p ∘ₗ ofTensorProduct I (Fin n → R)

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
p : (Fin n → R) →ₗ[R] M
hp : Function.Surjective ⇑p
f : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  ofTensorProduct I M ∘ₗ LinearMap.baseChange (AdicCompletion I R) p
g : AdicCompletion I R ⊗[R] (Fin n → R) →ₗ[AdicCompletion I R] AdicCompletion I M :=
  map I p ∘ₗ ofTensorProduct I (Fin n → R)
⊢ Function.Surjective ⇑(ofTensorProduct I M)
-- Mathlib/Algebra/Lie/Engel.lean
theorem lie_top_eq_of_span_sup_eq_top (N : LieSubmodule R L M) :
    (↑⁅(⊤ : LieIdeal R L), N⁆ : Submodule R M) =
      (N : Submodule R M).map (toEnd R L M x) ⊔ (↑⁅I, N⁆ : Submodule R M)

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
n : M
hn : n ∈ N
t : R
z : L
hz : z ∈ I
⊢ ∃ y ∈ Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N),
    ∃ z_1 ∈ Submodule.span R {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}, y + z_1 = ⁅t • x + z, n⁆

Tactic:
exact
  ⟨t • ⁅x, n⁆, Submodule.subset_span ⟨t • n, N.smul_mem' t hn, lie_smul t x n⟩, ⁅z, n⁆,
    Submodule.subset_span ⟨z, hz, n, hn, rfl⟩, by simp⟩

Result:
no goals

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ Submodule.span R {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x} =
    Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})

Tactic:
refine le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)

Result:
case refine_1
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x} ⊆
    ↑(Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}))

case refine_2
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
I : LieIdeal R L
x : L
hxI : Submodule.span R {x} ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
z : M
hz : z ∈ (fun a => ⁅x, a⁆) '' ↑↑N ∪ {x | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}
⊢ z ∈ {x | ∃ x_1, ∃ n ∈ N, ⁅x_1, n⁆ = x}
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_congr (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E}
    {g : β → F} : f =O[𝓝 b] g ↔ (f ∘ e) =O[𝓝 (e.symm b)] (g ∘ e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔ (f ∘ ↑e) =O[𝓝 (↑e.symm b)] (g ∘ ↑e)

Tactic:
simp only [IsBigO_def]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ (∃ c, IsBigOWith c (𝓝 b) f g) ↔ ∃ c, IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)

Tactic:
exact exists_congr fun C => e.isBigOWith_congr hb

Result:
no goals