harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioc a u', Ico a u ⊆ s :=
  (TFAE_mem_nhdsGE hu' s).out 0 3 (by norm_num) (by norm_num)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].get? 3 =
    some (∃ u ∈ Ioc a u', Ico a u ⊆ s)

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].get? 0 =
    some (s ∈ 𝓝[≥] a)

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem keys_ext {s₁ s₂ : AList β} : keys ⟦s₁⟧ = keys ⟦s₂⟧ ↔ s₁.keys ~ s₂.keys

Proof state:
α : Type u
β : α → Type v
s₁ s₂ : AList β
⊢ ⟦s₁⟧.keys = ⟦s₂⟧.keys ↔ s₁.keys ~ s₂.keys

Tactic:
simp [keys, AList.keys]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem sheafify_hom_ext {P Q : Cᵒᵖ ⥤ D} (η γ : sheafify J P ⟶ Q) (hQ : Presheaf.IsSheaf J Q)
    (h : toSheafify J P ≫ η = toSheafify J P ≫ γ) : η = γ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ η = γ

Tactic:
rw [sheafifyLift_unique J _ hQ _ h, ← h]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ sheafifyLift J (toSheafify J P ≫ η) hQ = γ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q : Cᵒᵖ ⥤ D
η γ : sheafify J P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : toSheafify J P ≫ η = toSheafify J P ≫ γ
⊢ sheafifyLift J (toSheafify J P ≫ η) hQ = γ

Tactic:
exact (sheafifyLift_unique J _ hQ _ h.symm).symm

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
theorem cmp_eq_compare (a b : α) : cmp a b = compare a b

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 => x1 < x2) a b
h2 : ¬(fun x1 x2 => x1 < x2) b a
⊢ Ordering.eq.Compares a b

Tactic:
exact le_antisymm (not_lt.1 h2) (not_lt.1 h1)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Tactic:
unfold cmp cmpUsing

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (if (fun x1 x2 => x1 < x2) a b then Ordering.lt
      else if (fun x1 x2 => x1 < x2) b a then Ordering.gt else Ordering.eq).Compares
    a b

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : (fun x1 x2 => x1 < x2) a b
⊢ Ordering.lt.Compares a b

Tactic:
exact h1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ cmp a b = compare a b

Tactic:
refine ((compare_iff ..).2 ?_).symm

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 => x1 < x2) a b
h2 : (fun x1 x2 => x1 < x2) b a
⊢ Ordering.gt.Compares a b

Tactic:
exact h2

Result:
no goals

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

Tactic:
split_ifs with h1 h2

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : (fun x1 x2 => x1 < x2) a b
⊢ Ordering.lt.Compares a b

case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 => x1 < x2) a b
h2 : (fun x1 x2 => x1 < x2) b a
⊢ Ordering.gt.Compares a b

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h1 : ¬(fun x1 x2 => x1 < x2) a b
h2 : ¬(fun x1 x2 => x1 < x2) b a
⊢ Ordering.eq.Compares a b
-- Mathlib/CategoryTheory/Yoneda.lean
/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
    than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
    can avoid the "motive is not type correct" error. -/
lemma map_yonedaEquiv' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.map g (yonedaEquiv f) = f.app Y g.unop

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ F.map g (yonedaEquiv f) = f.app Y g.unop

Tactic:
rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
lemma iff_appLE : P f ↔ ∀ (U : Y.affineOpens) (V : X.affineOpens) (e), Q (f.appLE U V e).hom

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
⊢ P f ↔
    ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
rw [eq_affineLocally P, affineLocally_iff_affineOpens_le]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem isIso_of_comp_hom_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : f ≫ g = 𝟙 Y) : IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso (inv g)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso f

Tactic:
rw [(comp_hom_eq_id _).mp h]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : f ≫ g = 𝟙 Y
⊢ IsIso (inv g)
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t'_fst_fst_fst (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) ≫ pullback.fst (𝒰.map j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
  pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_fst,
  pullbackRightPullbackFstIso_hom_fst_assoc]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_eq_self_iff (x : E) : reflection K x = x ↔ x ∈ K

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
⊢ 2 ≠ 0

Tactic:
exact two_ne_zero

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
⊢ (reflection K) x = x ↔ x ∈ K

Tactic:
rw [← orthogonalProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
  two_smul ℕ, ← two_smul 𝕜]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
⊢ 2 • ↑((orthogonalProjection K) x) = 2 • x ↔ ↑((orthogonalProjection K) x) = x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
⊢ 2 • ↑((orthogonalProjection K) x) = 2 • x ↔ ↑((orthogonalProjection K) x) = x

Tactic:
refine (smul_right_injective E ?_).eq_iff

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x : E
⊢ 2 ≠ 0
-- Mathlib/Algebra/Quandle.lean
theorem self_invAct_eq_iff_eq {x y : R} : x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
h : op x ◃ op x = op y ◃ op y ↔ op x = op y
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y

Tactic:
have h := @self_act_eq_iff_eq _ _ (op x) (op y)

Result:
R : Type u_1
inst✝ : Rack R
x y : R
h : op x ◃ op x = op y ◃ op y ↔ op x = op y
⊢ x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
-- Mathlib/Data/Set/Prod.lean
theorem prod_eq_empty_iff : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Tactic:
simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_sub_le_iff_left (qn : q.natDegree ≤ n) :
    (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Proof state:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
rw [← natDegree_neg] at qn

Result:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Proof state:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]

Result:
no goals
-- Mathlib/Data/Set/UnionLift.lean
theorem iUnionLift_const (c : T) (ci : ∀ i, S i) (hci : ∀ i, (ci i : α) = c) (cβ : β)
    (h : ∀ i, f i (ci i) = cβ) : iUnionLift S f hf T hT c = cβ

Proof state:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
this : ci i = ⟨↑c, hi⟩
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
rw [iUnionLift_of_mem _ hi, ← this, h]

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
let ⟨i, hi⟩ := Set.mem_iUnion.1 (hT c.prop)

Result:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
⊢ iUnionLift S f hf T hT c = cβ

Proof state:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
⊢ iUnionLift S f hf T hT c = cβ

Tactic:
have : ci i = ⟨c, hi⟩ := Subtype.ext (hci i)

Result:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
this : ci i = ⟨↑c, hi⟩
⊢ iUnionLift S f hf T hT c = cβ
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
lemma rightHomologyMap'_congr (h : Homotopy φ₁ φ₂) (h₁ : S₁.RightHomologyData)
    (h₂ : S₂.RightHomologyData) : rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem coe_image_Ioc_eq : ((↑) : 𝕜 → AddCircle p) '' Ioc a (a + p) = univ

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ QuotientAddGroup.mk '' Ioc a (a + p) = univ

Tactic:
rw [image_eq_range]

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x => ↑↑x) = univ

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ (range fun x => ↑↑x) = univ

Tactic:
exact (equivIoc p a).symm.range_eq_univ

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive]
lemma prod_min_le [LinearOrder M] [MulLeftMono M]
    [MulRightMono M] (l : List α) (f g : α → M) :
    (l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i => f i ⊓ g i) l).prod ≤ (map f l).prod ∧ (map (fun i => f i ⊓ g i) l).prod ≤ (map g l).prod

Tactic:
constructor <;> apply List.prod_le_prod' <;> intros

Result:
case left.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ⊓ g i✝ ≤ f i✝

case right.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ⊓ g i✝ ≤ g i✝

Proof state:
case left.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ⊓ g i✝ ≤ f i✝

Tactic:
apply min_le_left

Result:
no goals

Proof state:
case right.h
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
i✝ : α
a✝ : i✝ ∈ l
⊢ f i✝ ⊓ g i✝ ≤ g i✝

Tactic:
apply min_le_right

Result:
no goals

Proof state:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i => f i ⊓ g i) l).prod ≤ (map f l).prod ⊓ (map g l).prod

Tactic:
rw [le_min_iff]

Result:
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i => f i ⊓ g i) l).prod ≤ (map f l).prod ∧ (map (fun i => f i ⊓ g i) l).prod ≤ (map g l).prod
-- Mathlib/Data/Set/Countable.lean
theorem Countable.exists_eq_range {s : Set α} (hc : s.Countable) (hs : s.Nonempty) :
    ∃ f : ℕ → α, s = range f

Proof state:
case intro
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)

Tactic:
rw [hf.range_comp, Subtype.range_coe]

Result:
no goals

Proof state:
case intro
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f

Tactic:
refine ⟨(↑) ∘ f, ?_⟩

Result:
case intro
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ s = range (Subtype.val ∘ f)

Proof state:
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
⊢ ∃ f, s = range f

Tactic:
rcases hc.exists_surjective hs with ⟨f, hf⟩

Result:
case intro
α : Type u
s : Set α
hc : s.Countable
hs : s.Nonempty
f : ℕ → ↑s
hf : Surjective f
⊢ ∃ f, s = range f
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.1)
    {a : α} {f : β → β} :
    Perm (toListModel (Const.modify m a f).1.2) (Const.modifyKey a f (toListModel m.1.2))

Proof state:
α : Type u
β : Type v
m : Raw₀ α fun x => β
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
h : Raw.WFImp m.val
a : α
f : β → β
⊢ toListModel (modify m a f).val.buckets ~ Const.modifyKey a f (toListModel m.val.buckets)

Tactic:
rw [Const.modify_eq_alter, Const.modifyKey_eq_alterKey]

Result:
α : Type u
β : Type v
m : Raw₀ α fun x => β
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
h : Raw.WFImp m.val
a : α
f : β → β
⊢ toListModel (alter m a fun x => Option.map f x).val.buckets ~
    Const.alterKey a (fun x => Option.map f x) (toListModel m.val.buckets)

Proof state:
α : Type u
β : Type v
m : Raw₀ α fun x => β
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
h : Raw.WFImp m.val
a : α
f : β → β
⊢ toListModel (alter m a fun x => Option.map f x).val.buckets ~
    Const.alterKey a (fun x => Option.map f x) (toListModel m.val.buckets)

Tactic:
exact Const.toListModel_alter h

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_coeff (p : S[X]) (i : ℕ) :
    (integerNormalization M p).coeff i = coeffIntegerNormalization M p i

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
i : ℕ
⊢ (integerNormalization M p).coeff i = coeffIntegerNormalization M p i

Tactic:
simp +contextual [integerNormalization, coeff_monomial,
  coeffIntegerNormalization_of_not_mem_support]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_eq_one : n ! = 1 ↔ n ≤ 1

Proof state:
case mpr
n : ℕ
⊢ n ≤ 1 → n ! = 1

Tactic:
rintro (_|_|_) <;> rfl

Result:
no goals

Proof state:
case mp
n : ℕ
h : n ! = 1
⊢ n ≤ 1

Tactic:
rw [← not_lt, ← one_lt_factorial, h]

Result:
case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < 1

Proof state:
case mp
n : ℕ
⊢ n ! = 1 → n ≤ 1

Tactic:
intro h

Result:
case mp
n : ℕ
h : n ! = 1
⊢ n ≤ 1

Proof state:
n : ℕ
⊢ n ! = 1 ↔ n ≤ 1

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ n ! = 1 → n ≤ 1

case mpr
n : ℕ
⊢ n ≤ 1 → n ! = 1

Proof state:
case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < 1

Tactic:
apply lt_irrefl

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Coherence/Basic.lean
theorem mk_eq {α : Type _} (a b a' b' : α) (ha : a = a') (hb : b = b') (h : a' = b') : a = b

Proof state:
α : Type u_1
a b a' b' : α
ha : a = a'
hb : b = b'
h : a' = b'
⊢ a = b

Tactic:
simp [h, ha, hb]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
protected lemma TendstoUniformly.re {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ}
    (hf : TendstoUniformly f g p) :
    TendstoUniformly (fun n x => (f n x).re) (fun y => (g y).re) p

Proof state:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformly f g p
⊢ TendstoUniformly (fun n x => (f n x).re) (fun y => (g y).re) p

Tactic:
apply UniformContinuous.comp_tendstoUniformly uniformlyContinuous_re hf

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
lemma isNilpotent_trace_of_isNilpotent (hM : IsNilpotent M) :
    IsNilpotent (trace M)

Proof state:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent M.trace

Tactic:
suffices IsNilpotent (coeff (charpolyRev M) 1) by simpa using this

Result:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent (M.charpolyRev.coeff 1)

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
this : IsNilpotent (M.charpolyRev.coeff 1)
⊢ IsNilpotent M.trace

Tactic:
simpa using this

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
⊢ IsNilpotent M.trace

Tactic:
cases isEmpty_or_nonempty n

Result:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace

case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent M.trace

Proof state:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : Nonempty n
⊢ IsNilpotent (M.charpolyRev.coeff 1)

Tactic:
exact (isUnit_iff_coeff_isUnit_isNilpotent.mp (isUnit_charpolyRev_of_isNilpotent hM)).2
  _ one_ne_zero

Result:
no goals

Proof state:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
lemma normalClosure_mono (h : K ≤ K') : normalClosure F K L ≤ normalClosure F K' L

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K K' : IntermediateField F L
inst✝ : Normal F L
h : K ≤ K'
⊢ ⨆ f, map f K ≤ ⨆ f, map f K'

Tactic:
exact iSup_mono (fun f ↦ map_mono f h)

Result:
no goals

Proof state:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K K' : IntermediateField F L
inst✝ : Normal F L
h : K ≤ K'
⊢ normalClosure F (↥K) L ≤ normalClosure F (↥K') L

Tactic:
rw [normalClosure_def', normalClosure_def']

Result:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
K K' : IntermediateField F L
inst✝ : Normal F L
h : K ≤ K'
⊢ ⨆ f, map f K ≤ ⨆ f, map f K'
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFun_apply' (x : mixedSpace K) :
    convexBodySumFun x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ convexBodySumFun x = ∑ w : { w // w.IsReal }, ‖x.1 w‖ + 2 * ∑ w : { w // w.IsComplex }, ‖x.2 w‖

Tactic:
simp_rw [convexBodySumFun_apply, sum_eq_sum_add_sum, mult_isReal, mult_isComplex,
  Nat.cast_one, one_mul, Nat.cast_ofNat, normAtPlace_apply_of_isReal (Subtype.prop _),
  normAtPlace_apply_of_isComplex (Subtype.prop _), Finset.mul_sum]

Result:
no goals