harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Max.lean
theorem min'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
    (insert a s).min' (s.insert_nonempty a) = min (s.min' H) a :=
  (isLeast_min' _ _).unique <| by
    rw [coe_insert, min_comm]
    exact (isLeast_min' _ _).insert _

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (↑(insert a s)) (s.min' H ⊓ a)

Tactic:
rw [coe_insert, min_comm]

Result:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a ↑s) (a ⊓ s.min' H)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsLeast (insert a ↑s) (a ⊓ s.min' H)

Tactic:
exact (isLeast_min' _ _).insert _

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_of_lt_mul_left₀ [PosMulReflectLT α] (ha : 0 ≤ a) (h : a < a * b) : 1 < b :=
  lt_of_mul_lt_mul_left (by simpa) ha

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
ha : 0 ≤ a
h : a < a * b
⊢ a * 1 < a * b

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem countable_pi {π : α → Type*} [Finite α] {s : ∀ a, Set (π a)} (hs : ∀ a, (s a).Countable) :
    { f : ∀ a, π a | ∀ a, f a ∈ s a }.Countable

Proof state:
α : Type u
π : α → Type u_1
inst✝ : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), (s a).Countable
⊢ {f | ∀ (a : α), f a ∈ s a}.Countable

Tactic:
simpa only [← mem_univ_pi] using countable_univ_pi hs

Result:
no goals
-- Mathlib/Deprecated/Cardinal/PartENat.lean
lemma toPartENat_le_iff_of_lt_aleph0 {c c' : Cardinal} (hc' : c' < ℵ₀) :
    toPartENat c ≤ toPartENat c' ↔ c ≤ c'

Proof state:
c c' : Cardinal.{u_1}
hc' : c' < ℵ₀
⊢ toPartENat c ≤ toPartENat c' ↔ c ≤ c'

Tactic:
lift c' to ℕ using hc'

Result:
case intro
c : Cardinal.{u_1}
c' : ℕ
⊢ toPartENat c ≤ toPartENat ↑c' ↔ c ≤ ↑c'

Proof state:
case intro
c : Cardinal.{u_1}
c' : ℕ
⊢ toPartENat c ≤ toPartENat ↑c' ↔ c ≤ ↑c'

Tactic:
simp_rw [← partENatOfENat_toENat, toENat_nat, ← toENat_le_nat,
 ← PartENat.withTopOrderIso.symm.le_iff_le, PartENat.ofENat_le, map_le_map_iff]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem disjoint_compl_compl_right_iff : Disjoint a bᶜᶜ ↔ Disjoint a b

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint a bᶜᶜ ↔ Disjoint a b

Tactic:
simp_rw [← le_compl_iff_disjoint_right, compl_compl_compl]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_subset (x y : ∀ i, π i) :
    openSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i)

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => openSegment 𝕜 (x i) (y i)) i

Tactic:
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y : (i : ι) → π i
⊢ openSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i)

Tactic:
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => openSegment 𝕜 (x i) (y i)) i
-- Mathlib/Data/Multiset/Lattice.lean
theorem sup_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).sup = a ⊔ s.sup

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).sup = a ⊔ s.sup

Tactic:
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]

Result:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_add_lt_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c

Proof state:
a b c : Int
h✝ : a < b + c
h : -b + a < -b + (b + c)
⊢ -b + a < c

Tactic:
rwa [Int.neg_add_cancel_left] at h

Result:
no goals

Proof state:
a b c : Int
h : a < b + c
⊢ -b + a < c

Tactic:
have h := Int.add_lt_add_left h (-b)

Result:
a b c : Int
h✝ : a < b + c
h : -b + a < -b + (b + c)
⊢ -b + a < c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
    (a.set i v)[i]? = v

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
v : α
⊢ (a.set i v h)[i]? = some v

Tactic:
simp [getElem?_eq_getElem, h]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive (attr := simp)]
lemma map_comp_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) (n : ℕ) :
    f ∘ (g ^ n) = f ∘ g ^ n

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
⊢ ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝

Proof state:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
n : ℕ
x✝ : ι
⊢ (⇑f ∘ (g ^ n)) x✝ = (⇑f ∘ g ^ n) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem Convex.combo_affine_apply {x y : E} {a b : 𝕜} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
    f (a • x + b • y) = a • f x + b • f y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ f (b • (y -ᵥ x) + x) = b • (f y -ᵥ f x) + f x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ f (b • (y -ᵥ x) + x) = b • (f y -ᵥ f x) + f x

Tactic:
exact f.apply_lineMap _ _ _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma sin_sq_le_sq : sin x ^ 2 ≤ x ^ 2

Proof state:
x : ℝ
⊢ sin x ^ 2 ≤ x ^ 2

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl

⊢ sin 0 ^ 2 ≤ 0 ^ 2

case inr
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 ≤ x ^ 2

Proof state:
⊢ sin 0 ^ 2 ≤ 0 ^ 2

Tactic:
simp

Result:
no goals

Proof state:
case inl

⊢ sin 0 ^ 2 ≤ 0 ^ 2

case inr
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 ≤ x ^ 2

Tactic:
case inl => simp

Result:
case inr
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 ≤ x ^ 2

Proof state:
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 ≤ x ^ 2

Tactic:
exact (sin_sq_lt_sq hx).le

Result:
no goals

Proof state:
case inr
x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 ≤ x ^ 2

Tactic:
case inr => exact (sin_sq_lt_sq hx).le

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem continuousOn_mul {f g : ℝ → A} (hf : IntervalIntegrable f μ a b)
    (hg : ContinuousOn g [[a, b]]) : IntervalIntegrable (fun x => g x * f x) μ a b

Proof state:
A : Type u_5
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
⊢ IntervalIntegrable (fun x => g x * f x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hf ⊢

Result:
A : Type u_5
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x => g x * f x) (Ι a b) μ

Proof state:
A : Type u_5
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x => g x * f x) (Ι a b) μ

Tactic:
exact hf.continuousOn_mul_of_subset hg isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem max'_eq_sorted_last {s : Finset α} {h : s.Nonempty} :
    s.max' h =
      (s.sort (· ≤ ·))[(s.sort (· ≤ ·)).length - 1]'
        (by simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one) :=
  (sorted_last_eq_max'_aux _ (by simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one) _).symm

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length

Tactic:
simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.Nonempty
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).length - 1 < (sort (fun x1 x2 => x1 ≤ x2) s).length

Tactic:
simpa using Nat.sub_lt (card_pos.mpr h) Nat.zero_lt_one

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
@[to_additive addHaarScalarFactor_eq_integral_div]
lemma haarScalarFactor_eq_integral_div (μ' μ : Measure G) [IsHaarMeasure μ]
    [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] {f : G → ℝ} (hf : Continuous f)
    (h'f : HasCompactSupport f) (int_nonzero : ∫ x, f x ∂μ ≠ 0) :
    haarScalarFactor μ' μ = (∫ x, f x ∂μ') / ∫ x, f x ∂μ

Proof state:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ

Tactic:
have := integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport μ' μ hf h'f

Result:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
this : ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ

Proof state:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
this : ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ

Tactic:
rw [integral_smul_nnreal_measure] at this

Result:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
this : ∫ (x : G), f x ∂μ' = μ'.haarScalarFactor μ • ∫ (x : G), f x ∂μ
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ

Proof state:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous f
h'f : HasCompactSupport f
int_nonzero : ∫ (x : G), f x ∂μ ≠ 0
this : ∫ (x : G), f x ∂μ' = μ'.haarScalarFactor μ • ∫ (x : G), f x ∂μ
⊢ ↑(μ'.haarScalarFactor μ) = (∫ (x : G), f x ∂μ') / ∫ (x : G), f x ∂μ

Tactic:
exact EuclideanDomain.eq_div_of_mul_eq_left int_nonzero this.symm

Result:
no goals
-- Mathlib/Order/CompleteSublattice.lean
lemma isComplemented_iff : ComplementedLattice L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b

Proof state:
case refine_1.intro
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
x✝ : ComplementedLattice ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ b, IsCompl a b
b : ↥L
hb : IsCompl ⟨a, ha⟩ b
⊢ ∃ b ∈ L, IsCompl a b

Tactic:
exact ⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
b : α
hb : b ∈ L
hb' : IsCompl a b
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Tactic:
exact ⟨⟨b, hb⟩, CompleteSublattice.isCompl_iff.mpr hb'⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Tactic:
obtain ⟨b, hb, hb'⟩ := h a ha

Result:
case refine_2.intro.intro
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
b : α
hb : b ∈ L
hb' : IsCompl a b
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
⊢ ComplementedLattice ↥L ↔ ∀ a ∈ L, ∃ b ∈ L, IsCompl a b

Tactic:
refine ⟨fun ⟨h⟩ a ha ↦ ?_, fun h ↦ ⟨fun ⟨a, ha⟩ ↦ ?_⟩⟩

Result:
case refine_1
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
x✝ : ComplementedLattice ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ b, IsCompl a b
⊢ ∃ b ∈ L, IsCompl a b

case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Proof state:
case refine_1
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
x✝ : ComplementedLattice ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ b, IsCompl a b
⊢ ∃ b ∈ L, IsCompl a b

Tactic:
obtain ⟨b, hb⟩ := h ⟨a, ha⟩

Result:
case refine_1.intro
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
x✝ : ComplementedLattice ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ b, IsCompl a b
b : ↥L
hb : IsCompl ⟨a, ha⟩ b
⊢ ∃ b ∈ L, IsCompl a b
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pushoutIsoUnopPullback_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] :
    (pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op = (pushout.inr f g).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op = (pushout.inr f g).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op).unop = (pushout.inr f g).op.unop

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.snd f.op g.op).unop = (pushout.inr f g).op.unop

Tactic:
dsimp

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pullback.snd f.op g.op).unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inr f g

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pullback.snd f.op g.op).unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inr f g

Tactic:
rw [← pushoutIsoUnopPullback_inr_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem comp_assoc {δ : Type*} (r : Rel α β) (s : Rel β γ) (t : Rel γ δ) :
    (r • s) • t = r • (s • t)

Proof state:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) ↔ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

Tactic:
constructor

Result:
case a.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) → ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

case a.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w) → ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w

Proof state:
case a.h.a.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
z : γ
tzw : t z w
y : β
rxy : r x y
syz : s y z
⊢ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

Tactic:
exact ⟨y, rxy, z, syz, tzw⟩

Result:
no goals

Proof state:
case a.h.a.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
y : β
rxy : r x y
z : γ
syz : s y z
tzw : t z w
⊢ ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w

Tactic:
exact ⟨z, ⟨y, rxy, syz⟩, tzw⟩

Result:
no goals

Proof state:
case a.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) → ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

Tactic:
rintro ⟨z, ⟨y, rxy, syz⟩, tzw⟩

Result:
case a.h.a.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
z : γ
tzw : t z w
y : β
rxy : r x y
syz : s y z
⊢ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (r • s) • t = r • s • t

Tactic:
unfold comp

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (fun x z => ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y z) = fun x z => ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
⊢ (fun x z => ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y z) = fun x z => ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 z

Tactic:
ext (x w)

Result:
case a.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w) ↔ ∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w

Proof state:
case a.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
⊢ (∃ y, r x y ∧ ∃ y_1, s y y_1 ∧ t y_1 w) → ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w

Tactic:
rintro ⟨y, rxy, z, syz, tzw⟩

Result:
case a.h.a.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : Rel α β
s : Rel β γ
t : Rel γ δ
x : α
w : δ
y : β
rxy : r x y
z : γ
syz : s y z
tzw : t z w
⊢ ∃ y, (∃ y_1, r x y_1 ∧ s y_1 y) ∧ t y w
-- Mathlib/Data/Vector/Basic.lean
theorem get_cons_succ (a : α) (v : Vector α n) (i : Fin n) : get (a ::ᵥ v) i.succ = get v i

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
i : Fin n
⊢ (a ::ᵥ v).get i.succ = v.get i

Tactic:
rw [← get_tail_succ, tail_cons]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem isEmpty_of_chromaticNumber_eq_zero (G : SimpleGraph V) [Finite V]
    (h : G.chromaticNumber = 0) : IsEmpty V

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
h : G.chromaticNumber = 0
⊢ IsEmpty V

Tactic:
have h' := G.colorable_chromaticNumber_of_fintype

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
h : G.chromaticNumber = 0
h' : G.Colorable G.chromaticNumber.toNat
⊢ IsEmpty V

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
h : G.chromaticNumber = 0
h' : G.Colorable G.chromaticNumber.toNat
⊢ IsEmpty V

Tactic:
rw [h] at h'

Result:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
h : G.chromaticNumber = 0
h' : G.Colorable (ENat.toNat 0)
⊢ IsEmpty V

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
h : G.chromaticNumber = 0
h' : G.Colorable (ENat.toNat 0)
⊢ IsEmpty V

Tactic:
exact G.isEmpty_of_colorable_zero h'

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- Embedding a positive `Fin n` results in a positive `Fin (n + 1)` -/
lemma succAbove_pos [NeZero n] (p : Fin (n + 1)) (i : Fin n) (h : 0 < i) : 0 < p.succAbove i

Proof state:
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
⊢ 0 < p.succAbove i

Tactic:
by_cases H : castSucc i < p

Result:
case pos
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < p.succAbove i

case neg
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : ¬i.castSucc < p
⊢ 0 < p.succAbove i

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : ¬i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simp [succAbove_of_le_castSucc _ _ (Fin.not_lt.1 H)]

Result:
no goals

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simpa [succAbove_of_castSucc_lt _ _ H] using castSucc_pos' h

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Icc {a b : α} (hb : 0 ≤ b) :
    (Nat.cast : ℕ → α) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
simp [ceil_le, hb, le_floor_iff]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Icc a b = Icc ⌈a⌉₊ ⌊b⌋₊

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
hb : 0 ≤ b
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉₊ ⌊b⌋₊
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftMonoidWithZeroHom_apply_div' {L : Type*} [CommGroupWithZero L]
    (φ : MonoidWithZeroHom K[X] L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (p q : K[X]) :
    liftMonoidWithZeroHom φ hφ (algebraMap _ _ p) / liftMonoidWithZeroHom φ hφ (algebraMap _ _ q) =
      φ p / φ q

Proof state:
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p) /
      (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) q) =
    φ p / φ q

Tactic:
rw [← map_div₀, liftMonoidWithZeroHom_apply_div]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem radical_eq_iff : I.radical = I ↔ I.IsRadical

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
⊢ I.radical = I ↔ I.IsRadical

Tactic:
rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]

Result:
no goals