harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csSup_image2_eq_csSup_csSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) (hs₀ : s.Nonempty) (hs₁ : BddAbove s)
    (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (image2 l s t) = l (sSup s) (sSup t)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
c : γ
⊢ sSup (image2 l s t) ≤ c ↔ l (sSup s) (sSup t) ≤ c

Tactic:
rw [csSup_le_iff (hs₁.image2 (fun _ => (h₁ _).monotone_l) (fun _ => (h₂ _).monotone_l) ht₁)
    (hs₀.image2 ht₀),
  forall_mem_image2, forall₂_swap, (h₂ _).le_iff_le, csSup_le_iff ht₁ ht₀]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
c : γ
⊢ (∀ i₂ ∈ t, ∀ i₁ ∈ s, l i₁ i₂ ≤ c) ↔ ∀ b ∈ t, b ≤ u₂ (sSup s) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
c : γ
⊢ (∀ i₂ ∈ t, ∀ i₁ ∈ s, l i₁ i₂ ≤ c) ↔ ∀ b ∈ t, b ≤ u₂ (sSup s) c

Tactic:
simp_rw [← (h₂ _).le_iff_le, (h₁ _).le_iff_le, csSup_le_iff hs₁ hs₀]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sSup (image2 l s t) = l (sSup s) (sSup t)

Tactic:
refine eq_of_forall_ge_iff fun c => ?_

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddAbove t
c : γ
⊢ sSup (image2 l s t) ≤ c ↔ l (sSup s) (sSup t) ≤ c
-- Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
theorem μ_forget_apply {G H : AddGrp.{u}} (p : G) (q : H) :
    Functor.LaxMonoidal.μ (forget AddGrp.{u}) G H (p, q) = (p, q)

Proof state:
G H : AddGrp
p : ↑G
q : ↑H
⊢ Functor.LaxMonoidal.μ (forget AddGrp) G H (p, q) = (p, q)

Tactic:
apply Prod.ext

Result:
case fst
G H : AddGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddGrp) G H (p, q)).1 = (p, q).1

case snd
G H : AddGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddGrp) G H (p, q)).2 = (p, q).2

Proof state:
case snd
G H : AddGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddGrp) G H (p, q)).2 = (p, q).2

Tactic:
exact congrFun (Functor.Monoidal.μ_snd (forget AddGrp.{u}) G H) (p, q)

Result:
no goals

Proof state:
case fst
G H : AddGrp
p : ↑G
q : ↑H
⊢ (Functor.LaxMonoidal.μ (forget AddGrp) G H (p, q)).1 = (p, q).1

Tactic:
exact congrFun (Functor.Monoidal.μ_fst (forget AddGrp.{u}) G H) (p, q)

Result:
no goals
-- Mathlib/Data/Nat/Periodic.lean
theorem filter_multiset_Ico_card_eq_of_periodic (n a : ℕ) (p : ℕ → Prop) [DecidablePred p]
    (pp : Periodic p a) : card (filter p (Ico n (n + a))) = a.count p

Proof state:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun x => p x) ∘ fun x => x % a) (Ico n (n + a)))

Tactic:
congr

Result:
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = (fun x => p x) ∘ fun x => x % a

Proof state:
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = (fun x => p x) ∘ fun x => x % a

Tactic:
funext n

Result:
case e_a.e_f.h
n✝ a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = ((fun x => p x) ∘ fun x => x % a) n

Proof state:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ (filter p (Ico n (n + a))).card = count p a

Tactic:
rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ←
  multiset_Ico_map_mod n, ← map_count_True_eq_filter_card, ← map_count_True_eq_filter_card,
  map_map]

Result:
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) =
    Multiset.count True (map ((fun x => p x) ∘ fun x => x % a) (Ico n (n + a)))

Proof state:
case e_a.e_f.h
n✝ a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = ((fun x => p x) ∘ fun x => x % a) n

Tactic:
exact (Function.Periodic.map_mod_nat pp n).symm

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Basic.lean
theorem conj_id (e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id

Proof state:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃ₗ[R] M₂
x✝ : M₂
⊢ (e.conj LinearMap.id) x✝ = LinearMap.id x✝

Tactic:
simp [conj_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃ₗ[R] M₂
⊢ e.conj LinearMap.id = LinearMap.id

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
e : M ≃ₗ[R] M₂
x✝ : M₂
⊢ (e.conj LinearMap.id) x✝ = LinearMap.id x✝
-- Mathlib/ModelTheory/Skolem.lean
theorem card_functions_sum_skolem₁ :
    #(Σ n, (L.sum L.skolem₁).Functions n) = #(Σ n, L.BoundedFormula Empty (n + 1))

Proof state:
L : Language
⊢ ((sum fun i => lift.{max u v, u} #(L.Functions i)) +
      sum fun i => lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) =
    sum fun i => #(L.BoundedFormula Empty (i + 1))

Tactic:
conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]

Result:
L : Language
⊢ ((sum fun i => lift.{max u v, u} #(L.Functions i)) + sum fun i => #(L.BoundedFormula Empty (i + 1))) =
    sum fun i => #(L.BoundedFormula Empty (i + 1))

Proof state:
L : Language
⊢ (sum fun i => lift.{max u v, u} #(L.Functions i)) ≤ sum fun i => #(L.BoundedFormula Empty (i + 1))

Tactic:
refine sum_le_sum _ _ fun n => ?_

Result:
L : Language
n : ℕ
⊢ lift.{max u v, u} #(L.Functions n) ≤ #(L.BoundedFormula Empty (n + 1))

Proof state:
L : Language
n : ℕ
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))

Tactic:
refine ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => ?_⟩⟩

Result:
L : Language
n : ℕ
f g : L.Functions n
h : (fun f => func f default =' func f default) f = (fun f => func f default =' func f default) g
⊢ f = g

Proof state:
L : Language
n : ℕ
f g : L.Functions n
h : (fun f => func f default =' func f default) f = (fun f => func f default =' func f default) g
⊢ f = g

Tactic:
rcases h with ⟨rfl, ⟨rfl⟩⟩

Result:
case refl
L : Language
n : ℕ
f : L.Functions n
⊢ f = f

Proof state:
case refl
L : Language
n : ℕ
f : L.Functions n
⊢ f = f

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
⊢ ℵ₀ ≤ sum fun i => #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [← mk_sigma]

Result:
L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))

Proof state:
L : Language
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) = #((n : ℕ) × L.BoundedFormula Empty (n + 1))

Tactic:
simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']

Result:
L : Language
⊢ ((sum fun i => lift.{max u v, u} #(L.Functions i)) +
      sum fun i => lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) =
    sum fun i => #(L.BoundedFormula Empty (i + 1))

Proof state:
L : Language
⊢ ((sum fun i => lift.{max u v, u} #(L.Functions i)) + sum fun i => #(L.BoundedFormula Empty (i + 1))) =
    sum fun i => #(L.BoundedFormula Empty (i + 1))

Tactic:
rw [add_comm, add_eq_max, max_eq_left]

Result:
L : Language
⊢ (sum fun i => lift.{max u v, u} #(L.Functions i)) ≤ sum fun i => #(L.BoundedFormula Empty (i + 1))

L : Language
⊢ ℵ₀ ≤ sum fun i => #(L.BoundedFormula Empty (i + 1))

Proof state:
L : Language
n : ℕ
⊢ lift.{max u v, u} #(L.Functions n) ≤ #(L.BoundedFormula Empty (n + 1))

Tactic:
rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]

Result:
L : Language
n : ℕ
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))

Proof state:
L : Language
⊢ ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))

Tactic:
exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
  (Sigma.mk.inj_iff.1 xy).1)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_C_mul [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {a : T} (p : T[X]) (ha : a ≠ 0) :
    (C a * p).aroots S = p.aroots S

Proof state:
case ha.hf
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
p : T[X]
ha : a ≠ 0
⊢ Function.Injective ⇑(algebraMap T S)

Tactic:
exact FaithfulSMul.algebraMap_injective T S

Result:
no goals

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (C a * p).aroots S = p.aroots S

Tactic:
rw [aroots_def, Polynomial.map_mul, map_C, roots_C_mul]

Result:
case ha
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (algebraMap T S) a ≠ 0

Proof state:
case ha
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
p : T[X]
ha : a ≠ 0
⊢ (algebraMap T S) a ≠ 0

Tactic:
rwa [map_ne_zero_iff]

Result:
case ha.hf
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
a : T
p : T[X]
ha : a ≠ 0
⊢ Function.Injective ⇑(algebraMap T S)
-- Mathlib/Data/Complex/Norm.lean
theorem dist_of_re_eq {z w : ℂ} (h : z.re = w.re) : dist z w = dist z.im w.im

Proof state:
z w : ℂ
h : z.re = w.re
⊢ dist z w = dist z.im w.im

Tactic:
rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_mono : Monotone τ := fun f g h =>
  le_of_tendsto_of_tendsto' f.tendsto_translation_number₀ g.tendsto_translation_number₀ fun n => by
    gcongr; exact pow_mono h _ _

Proof state:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 / ↑n ≤ (g ^ n) 0 / ↑n

Tactic:
gcongr

Result:
case hab
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 ≤ (g ^ n) 0

Proof state:
case hab
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ (f ^ n) 0 ≤ (g ^ n) 0

Tactic:
exact pow_mono h _ _

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Noetherian.lean
lemma finite_setOf_isMin :
    {x : PrimeSpectrum R | IsMin x}.Finite

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | x.asIdeal ∈ minimalPrimes R}).Finite

Tactic:
exact (minimalPrimes.finite_of_isNoetherianRing R).subset (Set.image_preimage_subset _ _)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ {x | IsMin x}.Finite

Tactic:
refine Set.Finite.of_finite_image (f := asIdeal) ?_ this.injOn

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | IsMin x}).Finite

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | IsMin x}).Finite

Tactic:
simp_rw [isMin_iff]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ (asIdeal '' {x | x.asIdeal ∈ minimalPrimes R}).Finite

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ {x | IsMin x}.Finite

Tactic:
have : Function.Injective (asIdeal (R := R)) := @PrimeSpectrum.ext _ _

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : Function.Injective asIdeal
⊢ {x | IsMin x}.Finite
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.inv_param_mul (hk : Tendsto k l atTop)
    (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (k⁻¹ * f)

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k⁻¹ * f)

Tactic:
simpa using hf.param_zpow_mul hk (-1)

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem sub_sub_sub {X Y : C} (a b c d : X ⟶ Y) : a - c - (b - d) = a - b - (c - d)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ a - c - (b - d) = a - b - (c - d)

Tactic:
rw [sub_def, ← lift_sub_lift, sub_def, Category.assoc, σ_comp, prod.lift_map_assoc]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_succ
    {f : ℂⁿ⁺¹ → E} {c : ℂⁿ⁺¹} {R : ℝⁿ⁺¹} (hf : TorusIntegrable f c R) :
    (∯ x in T(c, R), f x) =
      ∮ x in C(c 0, R 0), ∯ y in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c 0, R 0), ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, R ∘ Fin.succ), f (Fin.cons x y)

Tactic:
simpa using torusIntegral_succAbove hf 0

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
lemma AffineIndependent.eq_of_sum_eq_sum (hp : AffineIndependent k p)
    (hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i) (hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i) :
    ∀ i ∈ s, w₁ i = w₂ i

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → V
hp : AffineIndependent k p
hw : ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i
hwp : ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i
⊢ ∀ i ∈ s, w₁ i = w₂ i

Tactic:
refine fun i hi ↦ sub_eq_zero.1 (hp.eq_zero_of_sum_eq_zero (w := w₁ - w₂) ?_ ?_ _ hi) <;>
  simpa [sub_mul, sub_smul, sub_eq_zero]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/EpiMono.lean
theorem epi_iff_surjective {X Y : TopCat.{u}} (f : X ⟶ Y) : Epi f ↔ Function.Surjective f

Proof state:
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Function.Surjective ((forget TopCat).map f) ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rfl

Result:
no goals

Proof state:
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)

Tactic:
constructor

Result:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)

case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f

Proof state:
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [this, CategoryTheory.epi_iff_surjective]

Result:
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Function.Surjective ((forget TopCat).map f) ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Proof state:
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f

Tactic:
apply Functor.epi_of_epi_map

Result:
no goals

Proof state:
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
suffices Epi f ↔ Epi ((forget TopCat).map f) by
  rw [this, CategoryTheory.epi_iff_surjective]
  rfl

Result:
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)

Proof state:
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)

Tactic:
intro

Result:
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `lt_mul_inv_iff₀` for a version with multiplication on the other side. -/
lemma lt_mul_inv_iff₀' (hc : 0 < c) : a < b * c⁻¹ ↔ c * a < b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
⊢ a < b * c⁻¹ ↔ c * a < b

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
this : MulPosStrictMono G₀
⊢ a < b * c⁻¹ ↔ c * a < b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
this : MulPosStrictMono G₀
⊢ a < b * c⁻¹ ↔ c * a < b

Tactic:
rw [lt_mul_inv_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma pentagon_aux₂ {X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε} (i : X₂ ≅ Y₂) :
    ((X₁ ◁ i.hom) ▷ X₃) ≫ (α_ X₁ Y₂ X₃).hom ≫ (X₁ ◁ (i.inv ▷ X₃)) = (α_ X₁ X₂ X₃).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
i : X₂ ≅ Y₂
⊢ (X₁ ◁ i.hom) ▷ X₃ ≫ (α_ X₁ Y₂ X₃).hom ≫ X₁ ◁ i.inv ▷ X₃ = (α_ X₁ X₂ X₃).hom

Tactic:
simp only [associator_naturality₂_assoc, ← whiskerLeft_comp, ← whiskerRight_comp,
  Iso.hom_inv_id, whiskerRight_id, whiskerLeft_id, comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_lt_mul_of_neg_left [ExistsAddOfLE α] [PosMulStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    (h : b < a) (hc : c < 0) : c * a < c * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) = d * b

Tactic:
rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]

Result:
no goals

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
⊢ c * a < c * b

Tactic:
obtain ⟨d, hcd⟩ := exists_add_of_le hc.le

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ c * a < c * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ d * a = c * b + (d * b + d * a)

Tactic:
rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ c * a < c * b

Tactic:
refine (add_lt_add_iff_right (d * b + d * a)).1 ?_

Result:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) < c * b + (d * b + d * a)

Proof state:
case intro
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
h : b < a
hc : c < 0
d : α
hcd : 0 = c + d
⊢ c * a + (d * b + d * a) < c * b + (d * b + d * a)

Tactic:
calc
  _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
  _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
  _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Result:
no goals