harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_lt_of_one_lt_right [ExistsAddOfLE α] [PosMulStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    (ha : a < 0) (h : 1 < b) : a * b < a

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

Tactic:
simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_le_inv_of_neg (ha : a < 0) (hb : b < 0) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem epi_map_iff_epi [hF₁ : PreservesEpimorphisms F] [hF₂ : ReflectsEpimorphisms F] :
    Epi (F.map f) ↔ Epi f

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
h : Epi f
⊢ Epi (F.map f)

Tactic:
exact F.map_epi f

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

Tactic:
exact F.epi_of_epi_map

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi f → Epi (F.map f)

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
h : Epi f
⊢ Epi (F.map f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) ↔ Epi f

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi f → Epi (F.map f)
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem lowerCrossingTime_mono (hnm : n ≤ m) :
    lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
this : Monotone fun n => lowerCrossingTime a b f N n ω
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω

Tactic:
exact this hnm

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n => lowerCrossingTime a b f N n ω

Tactic:
exact monotone_nat_of_le_succ fun n =>
  le_trans lowerCrossingTime_le_upperCrossingTime_succ upperCrossingTime_le_lowerCrossingTime

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ lowerCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N m ω

Tactic:
suffices Monotone fun n => lowerCrossingTime a b f N n ω by exact this hnm

Result:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n m : ℕ
ω : Ω
hnm : n ≤ m
⊢ Monotone fun n => lowerCrossingTime a b f N n ω
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma isOver_iff [X.Over S] [Y.Over S] {f : X.PartialMap Y} :
    f.IsOver S ↔ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Proof state:
X Y S : Scheme
inst✝¹ : X.Over S
inst✝ : Y.Over S
f : X.PartialMap Y
⊢ IsOver S f ↔ (f.compHom (Y ↘ S)).hom = f.domain.ι ≫ X ↘ S

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp]
lemma _root_.finCongr_refl (h : n = n := rfl) : finCongr h = Equiv.refl (Fin n)

Proof state:
n : ℕ
h : optParam (n = n) ⋯
⊢ finCongr h = Equiv.refl (Fin n)

Tactic:
ext

Result:
case H.h
n : ℕ
h : optParam (n = n) ⋯
x✝ : Fin n
⊢ ↑((finCongr h) x✝) = ↑((Equiv.refl (Fin n)) x✝)

Proof state:
case H.h
n : ℕ
h : optParam (n = n) ⋯
x✝ : Fin n
⊢ ↑((finCongr h) x✝) = ↑((Equiv.refl (Fin n)) x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem Function.Injective.preimage_pullbackDiagonal {f : X → Y} {g : Z → X} (inj : g.Injective) :
    mapPullback g id g (by rfl) (by rfl) ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g) :=
  ext fun _ ↦ inj.eq_iff

Proof state:
X : Type ?u.102728
Y : Sort ?u.102702
Z : Type ?u.102729
f : X → Y
g : Z → X
inj : Injective g
⊢ f ∘ g = id ∘ f ∘ g

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_mod_mul (x y z : Ordinal) : (x * y) % (x * z) = x * (y % z)

Proof state:
case inl
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)

Tactic:
simp

Result:
no goals

Proof state:
x y z : Ordinal.{u_4}
⊢ x * y % (x * z) = x * (y % z)

Tactic:
obtain rfl | hx := Ordinal.eq_zero_or_pos x

Result:
case inl
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)

case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)

Proof state:
case inr
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)

Tactic:
convert mul_add_mod_mul hx y z using 1 <;>
rw [add_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem tan_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖

Tactic:
rw [sub_eq_add_neg, tan_angle_add_of_inner_eq_zero h, norm_neg]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem le_of_dvd : ∀ {a b : Cardinal}, b ≠ 0 → a ∣ b → a ≤ b
  | a, x, b0, ⟨b, hab⟩ => by
    simpa only [hab, mul_one] using
      mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => b0 (by rwa [h, mul_zero] at hab)) a

Proof state:
a x : Cardinal.{u_1}
b0 : x ≠ 0
b : Cardinal.{u_1}
hab : x = a * b
h : b = 0
⊢ x = 0

Tactic:
rwa [h, mul_zero] at hab

Result:
no goals

Proof state:
a x : Cardinal.{u_1}
b0 : x ≠ 0
b : Cardinal.{u_1}
hab : x = a * b
⊢ a ≤ x

Tactic:
simpa only [hab, mul_one] using
  mul_le_mul_left' (one_le_iff_ne_zero.2 fun h : b = 0 => b0 (by rwa [h, mul_zero] at hab)) a

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_apply_prod {κ : Kernel α β} {η : Kernel (α × β) γ}
    [IsSFiniteKernel κ] [IsSFiniteKernel η] {a : α}
    {s : Set β} {t : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t) :
    (κ ⊗ₖ η) a (s ×ˢ t) = ∫⁻ b in s, η (a, b) t ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ((κ ⊗ₖ η) a) (s ×ˢ t) = ∫⁻ (b : β) in s, (η (a, b)) t ∂κ a

Tactic:
rw [compProd_apply (hs.prod ht), ← lintegral_indicator hs]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ a = ∫⁻ (a_1 : β), s.indicator (fun b => (η (a, b)) t) a_1 ∂κ a

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
⊢ (η (a✝, a)) {c | (a, c) ∈ s ×ˢ t} = s.indicator (fun b => (η (a✝, b)) t) a

Tactic:
by_cases ha : a ∈ s <;> simp [ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ a = ∫⁻ (a_1 : β), s.indicator (fun b => (η (a, b)) t) a_1 ∂κ a

Tactic:
congr with a

Result:
case e_f.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a✝ : α
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
a : β
⊢ (η (a✝, a)) {c | (a, c) ∈ s ×ˢ t} = s.indicator (fun b => (η (a✝, b)) t) a
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_div {M : Type*} [CommGroup M] (f : ℕ → M) (n : ℕ) :
    (∏ i ∈ range n, f (i + 1) / f i) = f n / f 0

Proof state:
M : Type u_6
inst✝ : CommGroup M
f : ℕ → M
n : ℕ
⊢ ∏ i ∈ range n, f (i + 1) / f i = f n / f 0

Tactic:
apply prod_range_induction <;> simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem exp_add_mul_I : exp (x + y * I) = exp x * (cos y + sin y * I)

Proof state:
x y : ℂ
⊢ cexp (x + y * I) = cexp x * (cos y + sin y * I)

Tactic:
rw [exp_add, exp_mul_I]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma localized'_ker_eq_ker_localizedMap (g : M →ₗ[R] P) :
    (ker g).localized' S p f = ker ((map p f f' g).extendScalarsOfIsLocalization p S) :=
  SetLike.ext (by apply SetLike.ext_iff.mp (f.ker_localizedMap_eq_localized₀_ker p f' g).symm)

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module S N
inst✝⁹ : IsScalarTower R S N
p : Submonoid R
inst✝⁸ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁷ : IsLocalizedModule p f
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ∀ (x : N),
    x ∈ localized' S p f (ker g) ↔ x ∈ ker (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))

Tactic:
apply SetLike.ext_iff.mp (f.ker_localizedMap_eq_localized₀_ker p f' g).symm

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem step5 {P : Sylow (Nat.card N).minFac N} : P.1 ≠ ⊥

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
⊢ ↑P ≠ ⊥

Tactic:
haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩

Result:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ ↑P ≠ ⊥

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ ↑P ≠ ⊥

Tactic:
apply P.ne_bot_of_dvd_card

Result:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ (Nat.card ↥N).minFac ∣ Nat.card ↥N

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
P : Sylow (Nat.card ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ (Nat.card ↥N).minFac ∣ Nat.card ↥N

Tactic:
exact (Nat.card N).minFac_dvd

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem wellFounded_of_trans_of_irrefl (r : α → α → Prop) [IsTrans α r] [IsIrrefl α r] :
    WellFounded r

Proof state:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ filter (fun z => r z x) univ ⊂ filter (fun z => r z y) univ

Tactic:
simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
    Finset.subset_iff, mem_filter, true_and, mem_univ, hxy]

Result:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x

Proof state:
case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
this : ∀ (x y : α), r x y → #(filter (fun z => r z x) univ) < #(filter (fun z => r z y) univ)
⊢ WellFounded r

Tactic:
exact Subrelation.wf (this _ _) (measure _).wf

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
⊢ WellFounded r

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
⊢ WellFounded r

Proof state:
case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
⊢ WellFounded r

Tactic:
have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
  Finset.card_lt_card <| by
    simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter, true_and, mem_univ, hxy]
    exact
      ⟨fun z hzx => _root_.trans hzx hxy,
        not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩

Result:
case intro
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
this : ∀ (x y : α), r x y → #(filter (fun z => r z x) univ) < #(filter (fun z => r z y) univ)
⊢ WellFounded r

Proof state:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
⊢ WellFounded r

Tactic:
classical
cases nonempty_fintype α
have (x y) (hxy : r x y) : #{z | r z x} < #{z | r z y} :=
  Finset.card_lt_card <| by
    simp only [Finset.lt_iff_ssubset.symm, lt_iff_le_not_le, Finset.le_iff_subset,
        Finset.subset_iff, mem_filter, true_and, mem_univ, hxy]
    exact
      ⟨fun z hzx => _root_.trans hzx hxy,
        not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩
exact Subrelation.wf (this _ _) (measure _).wf

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsIrrefl α r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x

Tactic:
exact
  ⟨fun z hzx => _root_.trans hzx hxy,
    not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem nonuniformWitnesses_spec (h : ¬G.IsUniform ε s t) :
    ε ≤
      |G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 -
          G.edgeDensity s t|

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|

Tactic:
rw [nonuniformWitnesses, dif_pos h]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ε ≤ ↑|G.edgeDensity (⋯.choose, ⋯.choose).1 (⋯.choose, ⋯.choose).2 - G.edgeDensity s t|

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
⊢ ε ≤ ↑|G.edgeDensity (⋯.choose, ⋯.choose).1 (⋯.choose, ⋯.choose).2 - G.edgeDensity s t|

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.2

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Centralizer.lean
theorem mem_centralizer_iff_commutator_eq_one {g : G} {s : Set G} :
    g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1

Proof state:
G : Type u_1
inst✝ : Group G
g : G
s : Set G
⊢ g ∈ centralizer s ↔ ∀ h ∈ s, h * g * h⁻¹ * g⁻¹ = 1

Tactic:
simp only [mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_sup {u v : ℕ → ℝ≥0∞} :
    expGrowthSup (u ⊔ v) = expGrowthSup u ⊔ expGrowthSup v

Proof state:
u v : ℕ → ℝ≥0∞
⊢ limsup (fun n => ((u ⊔ v) n).log / ↑n) atTop = limsup (fun a => (u a).log / ↑a ⊔ (v a).log / ↑a) atTop

Tactic:
refine limsup_congr (Eventually.of_forall fun n ↦ ?_)

Result:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊔ v) n).log / ↑n = (u n).log / ↑n ⊔ (v n).log / ↑n

Proof state:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup (u ⊔ v) = expGrowthSup u ⊔ expGrowthSup v

Tactic:
rw [expGrowthSup, expGrowthSup, expGrowthSup, ← limsup_max]

Result:
u v : ℕ → ℝ≥0∞
⊢ limsup (fun n => ((u ⊔ v) n).log / ↑n) atTop = limsup (fun a => (u a).log / ↑a ⊔ (v a).log / ↑a) atTop

Proof state:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u ⊔ v) n).log / ↑n = (u n).log / ↑n ⊔ (v n).log / ↑n

Tactic:
rw [Pi.sup_apply, log_monotone.map_max]

Result:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u n).log ⊔ (v n).log) / ↑n = (u n).log / ↑n ⊔ (v n).log / ↑n

Proof state:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ ((u n).log ⊔ (v n).log) / ↑n = (u n).log / ↑n ⊔ (v n).log / ↑n

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_max

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem inertiaDeg_of_subsingleton [hp : p.IsMaximal] [hQ : Subsingleton (S ⧸ P)] :
    inertiaDeg p P = 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
hp : p.IsMaximal
hQ : Subsingleton (S ⧸ P)
⊢ p.inertiaDeg P = 0

Tactic:
have := Ideal.Quotient.subsingleton_iff.mp hQ

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
hp : p.IsMaximal
hQ : Subsingleton (S ⧸ P)
this : P = ⊤
⊢ p.inertiaDeg P = 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
hp : p.IsMaximal
hQ : Subsingleton (S ⧸ P)
this : P = ⊤
⊢ p.inertiaDeg P = 0

Tactic:
subst this

Result:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
inst✝ : Algebra R S
hp : p.IsMaximal
hQ : Subsingleton (S ⧸ ⊤)
⊢ p.inertiaDeg ⊤ = 0

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
inst✝ : Algebra R S
hp : p.IsMaximal
hQ : Subsingleton (S ⧸ ⊤)
⊢ p.inertiaDeg ⊤ = 0

Tactic:
exact dif_neg fun h => hp.ne_top <| h.symm.trans comap_top

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma deriv2_negMulLog (x : ℝ) : deriv^[2] negMulLog x = - x⁻¹

Proof state:
x : ℝ
⊢ deriv^[2] negMulLog x = -x⁻¹

Tactic:
rw [negMulLog_eq_neg]

Result:
x : ℝ
⊢ deriv^[2] (fun x => -(x * log x)) x = -x⁻¹

Proof state:
x : ℝ
⊢ deriv^[2] (fun x => -(x * log x)) x = -x⁻¹

Tactic:
have h := deriv2_mul_log

Result:
x : ℝ
h : ∀ (x : ℝ), deriv^[2] (fun x => x * log x) x = x⁻¹
⊢ deriv^[2] (fun x => -(x * log x)) x = -x⁻¹

Proof state:
x : ℝ
h : ∀ (x : ℝ), deriv (deriv fun x => x * log x) x = x⁻¹
⊢ -deriv (deriv fun y => y * log y) x = -x⁻¹

Tactic:
rw [h]

Result:
no goals

Proof state:
x : ℝ
h : ∀ (x : ℝ), deriv^[2] (fun x => x * log x) x = x⁻¹
⊢ deriv^[2] (fun x => -(x * log x)) x = -x⁻¹

Tactic:
simp only [Function.iterate_succ, Function.iterate_zero, Function.id_comp,
  Function.comp_apply, deriv.neg', differentiableAt_id', differentiableAt_log_iff, ne_eq] at h ⊢

Result:
x : ℝ
h : ∀ (x : ℝ), deriv (deriv fun x => x * log x) x = x⁻¹
⊢ -deriv (deriv fun y => y * log y) x = -x⁻¹
-- Mathlib/Data/PEquiv.lean
theorem trans_eq_none (f : α ≃. β) (g : β ≃. γ) (a : α) :
    f.trans g a = none ↔ ∀ b c, b ∉ f a ∨ c ∉ g b

Proof state:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (f.trans g) a = none ↔ ∀ (b : β) (c : γ), b ∉ f a ∨ c ∉ g b

Tactic:
simp only [eq_none_iff_forall_not_mem, mem_trans, imp_iff_not_or.symm]

Result:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b ∈ f a, a_1 ∈ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → c ∉ g b

Proof state:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ∀ b ∈ f a, a_1 ∉ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → c ∉ g b

Tactic:
exact forall_swap

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ¬∃ b ∈ f a, a_1 ∈ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → c ∉ g b

Tactic:
push_neg

Result:
α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (∀ (a_1 : γ), ∀ b ∈ f a, a_1 ∉ g b) ↔ ∀ (b : β) (c : γ), b ∈ f a → c ∉ g b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_eq_iff_getLast_eq_some {xs : List α} (h) : xs.getLast h = a ↔ xs.getLast? = some a

Proof state:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.reverse.head? = some a ↔ xs.getLast? = some a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.getLast h = a ↔ xs.getLast? = some a

Tactic:
rw [getLast_eq_head_reverse, head_eq_iff_head?_eq_some]

Result:
α : Type u_1
a : α
xs : List α
h : xs ≠ []
⊢ xs.reverse.head? = some a ↔ xs.getLast? = some a
-- Mathlib/.lake/packages/batteries/Batteries/WF.lean
theorem ndrec_eq_ndrecC : @Acc.ndrec = @Acc.ndrecC

Proof state:
⊢ @ndrec = @Acc.ndrecC

Tactic:
funext α r motive intro a t

Result:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : α → Sort u_2
intro : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x
a : α
t : Acc r a
⊢ ndrec intro t = Acc.ndrecC intro t

Proof state:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : α → Sort u_2
intro : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x
a : α
t : Acc r a
⊢ ndrec intro t = Acc.ndrecC intro t

Tactic:
rw [Acc.ndrec, rec_eq_recC, Acc.ndrecC]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) : arg (r * x) = arg x

Proof state:
x : ℂ
r : ℝ
hr : 0 < r
⊢ (↑r * x).arg = x.arg

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
r : ℝ
hr : 0 < r
⊢ (↑r * 0).arg = arg 0

case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg

Proof state:
case inr
x : ℂ
r : ℝ
hr : 0 < r
hx : x ≠ 0
⊢ (↑r * x).arg = x.arg

Tactic:
conv_lhs =>
  rw [← norm_mul_cos_add_sin_mul_I x, ← mul_assoc, ← ofReal_mul,
    arg_mul_cos_add_sin_mul_I (mul_pos hr (norm_pos_iff.mpr hx)) x.arg_mem_Ioc]

Result:
no goals

Proof state:
case inl
r : ℝ
hr : 0 < r
⊢ (↑r * 0).arg = arg 0

Tactic:
rw [mul_zero]

Result:
no goals