harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Max.lean
theorem min'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α)
    (h : (s.image f).Nonempty) : (s.image f).min' h = f (s.min' h.of_image)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)

Tactic:
exact .symm <| comp_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).min' h = f (s.min' ⋯)

Tactic:
simp only [min', inf'_image]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.inf' ⋯ (id ∘ f) = f (s.inf' ⋯ id)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_smul_left (x y : V) (r : ℝ) :
    (o.oangle (x - r • y) y).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle (x - r • y) y).sign = (o.oangle x y).sign

Tactic:
rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_cons (f : α → β) (g : α → Multiset β) :
    (s.bind fun a => f a ::ₘ g a) = map f s + s.bind g :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [add_comm, add_left_comm, add_assoc])

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ ∀ (a : α) (s : Multiset α),
    (s.bind fun a => f a ::ₘ g a) = map f s + s.bind g →
      ((a ::ₘ s).bind fun a => f a ::ₘ g a) = map f (a ::ₘ s) + (a ::ₘ s).bind g

Tactic:
simp +contextual [add_comm, add_left_comm, add_assoc]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
g : α → Multiset β
⊢ (bind 0 fun a => f a ::ₘ g a) = map f 0 + bind 0 g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finsupp/Indicator.lean
lemma single_eq_indicator (b : α) : single i b = indicator {i} (fun _ _ => b)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
i : ι
b : α
⊢ single i b = indicator {i} fun x x => b

Tactic:
classical
ext j
simp [single_apply, indicator_apply, @eq_comm _ j]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
i : ι
b : α
⊢ single i b = indicator {i} fun x x => b

Tactic:
ext j

Result:
case h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
i : ι
b : α
j : ι
⊢ (single i b) j = (indicator {i} fun x x => b) j

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝ : Zero α
i : ι
b : α
j : ι
⊢ (single i b) j = (indicator {i} fun x x => b) j

Tactic:
simp [single_apply, indicator_apply, @eq_comm _ j]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isOpen_image (h : X ≃ₜ Y) {s : Set X} : IsOpen (h '' s) ↔ IsOpen s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ IsOpen (⇑h '' s) ↔ IsOpen s

Tactic:
rw [← preimage_symm, isOpen_preimage]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
    preserves finite biproducts. -/
lemma preservesBiproduct_of_preservesProduct {f : J → C} [PreservesLimit (Discrete.functor f) F] :
    PreservesBiproduct f F where
  preserves {b} hb :=
    ⟨isBilimitOfIsLimit _ <|
      IsLimit.ofIsoLimit
          ((IsLimit.postcomposeHomEquiv (Discrete.compNatIsoDiscrete _ _) (F.mapCone b.toCone)).symm
            (isLimitOfPreserves F hb.isLimit)) <|
        Cones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

Proof state:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesLimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
as✝ : J
⊢ ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app { as := as✝ } =
    (Iso.refl ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt).hom ≫
      (F.mapBicone b).toCone.π.app { as := as✝ }

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesLimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
⊢ ∀ (j : Discrete J),
    ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app j =
      (Iso.refl ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt).hom ≫
        (F.mapBicone b).toCone.π.app j

Tactic:
rintro ⟨⟩

Result:
case mk
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
D : Type u'
inst✝⁴ : Category.{v', u'} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : PreservesLimit (Discrete.functor f) F
b : Bicone f
hb : b.IsBilimit
as✝ : J
⊢ ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app { as := as✝ } =
    (Iso.refl ((Cones.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt).hom ≫
      (F.mapBicone b).toCone.π.app { as := as✝ }
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integral_fun_snd (f : β → E) : ∫ z, f z.2 ∂μ.prod ν = (μ univ).toReal • ∫ y, f y ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : β → E
⊢ ∫ (z : α × β), f z.2 ∂μ.prod ν = (μ univ).toReal • ∫ (y : β), f y ∂ν

Tactic:
simpa using integral_prod_smul (1 : α → ℝ) f

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_lt_one_of_neg₀ (ha : 1 < a) (hn : n < 0) : a ^ n < 1

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha : 1 < a
hn : n < 0
⊢ a ^ n < 1

Tactic:
simpa using zpow_right_strictMono₀ ha hn

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Projective.lean
theorem Module.finrank_of_isLocalizedModule_of_free
    (Rₛ : Type*) {Mₛ : Type*} [AddCommGroup Mₛ] [Module R Mₛ]
    [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ Mₛ] [IsScalarTower R Rₛ Mₛ] (S : Submonoid R)
    (f : M →ₗ[R] Mₛ) [IsLocalization S Rₛ] [IsLocalizedModule S f] [Module.Free R M]
    [Nontrivial Rₛ] :
    Module.finrank Rₛ Mₛ = Module.finrank R M

Proof state:
R : Type u_1
M : Type uM
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
Rₛ : Type u_4
Mₛ : Type u_5
inst✝⁹ : AddCommGroup Mₛ
inst✝⁸ : Module R Mₛ
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ Mₛ
inst✝⁴ : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst✝³ : IsLocalization S Rₛ
inst✝² : IsLocalizedModule S f
inst✝¹ : Free R M
inst✝ : Nontrivial Rₛ
⊢ finrank Rₛ Mₛ = finrank R M

Tactic:
simpa using congr(Cardinal.toNat $(Module.lift_rank_of_isLocalizedModule_of_free Rₛ S f))

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.balRight (hl : l.Balanced cl (n + 1)) (hr : r.RedRed True n) :
    (balRight l v r).RedRed (cl = red) (n + 1)

Proof state:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cl : RBColor
n : Nat
hl : l.Balanced cl (n + 1)
hr : RedRed True r n
⊢ RedRed (cl = red) (l.balRight v r) (n + 1)

Tactic:
rw [← reverse_reverse (balRight ..), reverse_balRight]

Result:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cl : RBColor
n : Nat
hl : l.Balanced cl (n + 1)
hr : RedRed True r n
⊢ RedRed (cl = red) (r.reverse.balLeft v l.reverse).reverse (n + 1)

Proof state:
α✝ : Type u_1
l : RBNode α✝
v : α✝
r : RBNode α✝
cl : RBColor
n : Nat
hl : l.Balanced cl (n + 1)
hr : RedRed True r n
⊢ RedRed (cl = red) (r.reverse.balLeft v l.reverse).reverse (n + 1)

Tactic:
exact .reverse <| hl.reverse.balLeft hr.reverse

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem merge_eq_mergeTR : @merge = @mergeTR

Proof state:
⊢ @merge = @mergeTR

Tactic:
funext

Result:
case h.h.h.h
x✝³ : Type u_1
x✝² x✝¹ : List x✝³
x✝ : autoParam (x✝³ → x✝³ → Bool) _auto✝
⊢ x✝².merge x✝¹ x✝ = mergeTR x✝² x✝¹ x✝

Proof state:
case h.h.h.h
x✝³ : Type u_1
x✝² x✝¹ : List x✝³
x✝ : autoParam (x✝³ → x✝³ → Bool) _auto✝
⊢ x✝².merge x✝¹ x✝ = mergeTR x✝² x✝¹ x✝

Tactic:
simp [mergeTR, mergeTR_go_eq]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem tail_update_succ : tail (update q i.succ y) = update (tail q) i y

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
rw [h]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
by_cases h : j = i

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : ¬j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
⊢ tail (update q i.succ y) = update (tail q) i y

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
⊢ tail (update q i.succ y) j = update (tail q) i y j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i

Tactic:
simp [tail]

Result:
no goals

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : ¬j = i
⊢ tail (update q i.succ y) j = update (tail q) i y j

Tactic:
simp [tail, (Fin.succ_injective n).ne h, h]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph_succ (o : Ordinal) : ℵ_ (succ o) = succ (ℵ_ o)

Proof state:
o : Ordinal.{u_1}
⊢ ℵ_ (succ o) = succ (ℵ_ o)

Tactic:
rw [aleph_eq_preAleph, add_succ, preAleph_succ, aleph_eq_preAleph]

Result:
no goals
-- Mathlib/Topology/Homotopy/Product.lean
theorem pi_lift (γ : ∀ i, Path (as i) (bs i)) :
    (Path.Homotopic.pi fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.map Path.pi ⋯ (Quotient.choice fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ (pi fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧

Tactic:
unfold pi

Result:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
as bs : (i : ι) → X i
γ : (i : ι) → Path (as i) (bs i)
⊢ Quotient.map Path.pi ⋯ (Quotient.choice fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma infIrred_iff_of_finite : InfIrred s ↔ ∃ a, Ici a = s

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
a : α
ha : a ∈ ↑s
has : ∀ a' ∈ ↑s, id a' ≤ id a → id a = id a'
⊢ ∀ b ∈ s, b ≤ a → b = a

Tactic:
simpa [eq_comm] using has

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
⊢ (∃ a, Ici a = s) → InfIrred s

Tactic:
rintro ⟨a, rfl⟩

Result:
case refine_2.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ InfIrred (Ici a)

Proof state:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
⊢ ∃ a, Ici a = s

Tactic:
obtain ⟨a, ha, has⟩ := (s : Set α).toFinite.exists_minimal_wrt id _ (coe_nonempty.2 hs.ne_top)

Result:
case refine_1.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
a : α
ha : a ∈ ↑s
has : ∀ a' ∈ ↑s, id a' ≤ id a → id a = id a'
⊢ ∃ a, Ici a = s

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
⊢ InfIrred s ↔ ∃ a, Ici a = s

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
⊢ ∃ a, Ici a = s

case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
⊢ (∃ a, Ici a = s) → InfIrred s

Proof state:
case refine_1.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
s : UpperSet α
inst✝ : Finite α
hs : InfIrred s
a : α
ha : a ∈ ↑s
has : ∀ a' ∈ ↑s, id a' ≤ id a → id a = id a'
⊢ ∃ a, Ici a = s

Tactic:
exact ⟨a, (hs.2 <| erase_inf_Ici ha <| by simpa [eq_comm] using has).resolve_left
  (lt_erase.2 ha).ne'⟩

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
a : α
⊢ InfIrred (Ici a)

Tactic:
exact infIrred_Ici _

Result:
no goals
-- Mathlib/Data/ZMod/QuotientGroup.lean
theorem minimalPeriod_eq_card [Fintype (orbit (zpowers a) b)] :
    minimalPeriod (a • ·) b = Fintype.card (orbit (zpowers a) b)

Proof state:
α : Type u_3
β : Type u_4
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit (↥(zpowers a)) b)
⊢ minimalPeriod (fun x => a • x) b = Fintype.card ↑(orbit (↥(zpowers a)) b)

Tactic:
rw [← Fintype.ofEquiv_card (orbitZPowersEquiv a b), @ZMod.card _ (_)]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableWithinAt_sub_const_iff (c : F) :
    DifferentiableWithinAt 𝕜 (fun y => f y - c) s x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ DifferentiableWithinAt 𝕜 (fun y => f y - c) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [sub_eq_add_neg, differentiableWithinAt_add_const_iff]

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma Algebra.adjoin_root_eq_top_of_isSplittingField :
    Algebra.adjoin K {α} = ⊤

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ adjoin K {α} = ⊤

Tactic:
apply Subalgebra.map_injective (B := K[n√a]) (f := (adjoinRootXPowSubCEquiv hζ H hα).symm)
  (adjoinRootXPowSubCEquiv hζ H hα).symm.injective

Result:
case a
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm) (adjoin K {α}) =
    Subalgebra.map ↑(adjoinRootXPowSubCEquiv hζ H hα).symm ⊤

Proof state:
case a
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ Subalgebra.map (↑(adjoinRootXPowSubCEquiv hζ H hα).symm) (adjoin K {α}) =
    Subalgebra.map ↑(adjoinRootXPowSubCEquiv hζ H hα).symm ⊤

Tactic:
rw [Algebra.map_top, (AlgHom.range_eq_top _).mpr
  (adjoinRootXPowSubCEquiv hζ H hα).symm.surjective, AlgHom.map_adjoin,
  Set.image_singleton, AlgHom.coe_coe, adjoinRootXPowSubCEquiv_symm_eq_root, adjoinRoot_eq_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_congr {p q : α → Bool} :
    ∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
  | [], _ => rfl
  | a :: l, h => by
    rw [forall_mem_cons] at h; by_cases pa : p a
    · simp [pa, h.1 ▸ pa, filter_congr h.2]
    · simp [pa, h.1 ▸ pa, filter_congr h.2]

Proof state:
α : Type u_1
p q : α → Bool
a : α
l : List α
h : p a = q a ∧ ∀ (x : α), x ∈ l → p x = q x
⊢ filter p (a :: l) = filter q (a :: l)

Tactic:
by_cases pa : p a

Result:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
h : p a = q a ∧ ∀ (x : α), x ∈ l → p x = q x
pa : p a = true
⊢ filter p (a :: l) = filter q (a :: l)

case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
h : p a = q a ∧ ∀ (x : α), x ∈ l → p x = q x
pa : ¬p a = true
⊢ filter p (a :: l) = filter q (a :: l)

Proof state:
case neg
α : Type u_1
p q : α → Bool
a : α
l : List α
h : p a = q a ∧ ∀ (x : α), x ∈ l → p x = q x
pa : ¬p a = true
⊢ filter p (a :: l) = filter q (a :: l)

Tactic:
simp [pa, h.1 ▸ pa, filter_congr h.2]

Result:
no goals

Proof state:
case pos
α : Type u_1
p q : α → Bool
a : α
l : List α
h : p a = q a ∧ ∀ (x : α), x ∈ l → p x = q x
pa : p a = true
⊢ filter p (a :: l) = filter q (a :: l)

Tactic:
simp [pa, h.1 ▸ pa, filter_congr h.2]

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
a : α
l : List α
h : ∀ (x : α), x ∈ a :: l → p x = q x
⊢ filter p (a :: l) = filter q (a :: l)

Tactic:
rw [forall_mem_cons] at h

Result:
α : Type u_1
p q : α → Bool
a : α
l : List α
h : p a = q a ∧ ∀ (x : α), x ∈ l → p x = q x
⊢ filter p (a :: l) = filter q (a :: l)
-- Mathlib/Order/WellQuasiOrder.lean
theorem WellQuasiOrdered.wellFounded {α : Type*} {r : α → α → Prop} [IsPreorder α r]
    (h : WellQuasiOrdered r) : WellFounded fun a b ↦ r a b ∧ ¬ r b a

Proof state:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
⊢ WellFounded fun a b => r a b ∧ ¬r b a

Tactic:
let _ : Preorder α :=
  { le := r
    le_refl := refl_of r
    le_trans := fun _ _ _ => trans_of r }

Result:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := Preorder.mk ⋯ ⋯ ⋯
⊢ WellFounded fun a b => r a b ∧ ¬r b a

Proof state:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := Preorder.mk ⋯ ⋯ ⋯
this : WellQuasiOrderedLE α
⊢ WellFounded fun a b => r a b ∧ ¬r b a

Tactic:
exact wellFounded_lt

Result:
no goals

Proof state:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := Preorder.mk ⋯ ⋯ ⋯
⊢ WellFounded fun a b => r a b ∧ ¬r b a

Tactic:
have : WellQuasiOrderedLE α := ⟨h⟩

Result:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := Preorder.mk ⋯ ⋯ ⋯
this : WellQuasiOrderedLE α
⊢ WellFounded fun a b => r a b ∧ ¬r b a
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConcaveOn.sub (hf : UniformConcaveOn s φ f) (hg : UniformConvexOn s ψ g) :
    UniformConcaveOn s (φ + ψ) (f - g)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConvexOn s ψ g
⊢ UniformConcaveOn s (φ + ψ) (f - g)

Tactic:
simpa using hf.add hg.neg

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
lemma moduleCat_exact_iff_range_eq_ker :
    S.Exact ↔ LinearMap.range S.f.hom = LinearMap.ker S.g.hom

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ LinearMap.ker (ModuleCat.Hom.hom S.g) ≤ LinearMap.range (ModuleCat.Hom.hom S.f) ↔
    LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)

Tactic:
aesop

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)

Tactic:
rw [moduleCat_exact_iff_ker_sub_range]

Result:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ LinearMap.ker (ModuleCat.Hom.hom S.g) ≤ LinearMap.range (ModuleCat.Hom.hom S.f) ↔
    LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : Array α) (l' : Array β) :
    map (Function.uncurry f) (l.zip l') = zipWith f l l'

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l' : Array β
toList✝ : List α
⊢ map (Function.uncurry f) ({ toList := toList✝ }.zip l') = zipWith f { toList := toList✝ } l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ map (Function.uncurry f) ({ toList := toList✝¹ }.zip { toList := toList✝ }) =
    zipWith f { toList := toList✝¹ } { toList := toList✝ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
toList✝¹ : List α
toList✝ : List β
⊢ map (Function.uncurry f) ({ toList := toList✝¹ }.zip { toList := toList✝ }) =
    zipWith f { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.map_uncurry_zip_eq_zipWith]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : Array α
l' : Array β
⊢ map (Function.uncurry f) (l.zip l') = zipWith f l l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l' : Array β
toList✝ : List α
⊢ map (Function.uncurry f) ({ toList := toList✝ }.zip l') = zipWith f { toList := toList✝ } l'
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem factors_rel_of_associated {a b : α} (h : Associated a b) :
    Multiset.Rel Associated (factors a) (factors b)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Multiset.Rel Associated (factors a) (factors b)

Tactic:
rcases iff_iff_and_or_not_and_not.mp h.eq_zero_iff with (⟨rfl, rfl⟩ | ⟨ha, hb⟩)

Result:
case inl.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
h : 0 ~ᵤ 0
⊢ Multiset.Rel Associated (factors 0) (factors 0)

case inr.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ Multiset.Rel Associated (factors a) (factors b)

Proof state:
case inl.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
h : 0 ~ᵤ 0
⊢ Multiset.Rel Associated (factors 0) (factors 0)

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ (factors a).prod ~ᵤ (factors b).prod

Tactic:
exact ((factors_prod ha).trans h).trans (factors_prod hb).symm

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ Multiset.Rel Associated (factors a) (factors b)

Tactic:
refine factors_unique irreducible_of_factor irreducible_of_factor ?_

Result:
case inr.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : ¬a = 0
hb : ¬b = 0
⊢ (factors a).prod ~ᵤ (factors b).prod
-- Mathlib/Algebra/Order/Floor.lean
theorem Int.natCast_ceil_eq_ceil (ha : 0 ≤ a) : (⌈a⌉₊ : ℤ) = ⌈a⌉

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
ha : 0 ≤ a
⊢ ↑⌈a⌉₊ = ⌈a⌉

Tactic:
rw [← Int.ceil_toNat, Int.toNat_of_nonneg (Int.ceil_nonneg ha)]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iSup₂_iff {f : ∀ i, κ i → LowerSet α} : (a ∈ ⨆ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → LowerSet α
⊢ a ∈ ⨆ i, ⨆ j, f i j ↔ ∃ i j, a ∈ f i j

Tactic:
simp_rw [mem_iSup_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_monomial {n : ℕ} {r : R} : (monomial n r).eval₂ f x = f r * x ^ n

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x ((monomial n) r) = f r * x ^ n

Tactic:
simp [eval₂_eq_sum]

Result:
no goals