harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_diff_null (ht : μ t = 0) : μ (s \ t) = μ s :=
  (measure_mono diff_subset).antisymm <| calc
    μ s ≤ μ (s ∩ t) + μ (s \ t) := measure_le_inter_add_diff _ _ _
    _ ≤ μ t + μ (s \ t)

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ t + μ (s \ t)

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ s ∩ t ⊆ t

Proof state:
case bc.h
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ s ∩ t ⊆ t

Tactic:
apply inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
ht : μ t = 0
⊢ μ t + μ (s \ t) = μ (s \ t)

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
lemma isUnit_iff' :
    IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ P %ₘ X + X * (P /ₘ X) = C (eval 0 P) + X * (P /ₘ X)

Tactic:
simp [modByMonic_X]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ P = C (eval 0 P) + X * (P /ₘ X)

Tactic:
conv_lhs => rw [← modByMonic_add_div P monic_X]

Result:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ P %ₘ X + X * (P /ₘ X) = C (eval 0 P) + X * (P /ₘ X)

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
this : P = C (eval 0 P) + X * (P /ₘ X)
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Tactic:
conv_lhs => rw [this]; simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Tactic:
suffices P = C (eval 0 P) + X * (P /ₘ X) by
  conv_lhs => rw [this]; simp

Result:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ P = C (eval 0 P) + X * (P /ₘ X)
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem col_eq_prod {μ : YoungDiagram} {j : ℕ} : μ.col j = Finset.range (μ.colLen j) ×ˢ {j}

Proof state:
case h.mk
μ : YoungDiagram
j a b : ℕ
⊢ b = j → (a < μ.colLen b ↔ a < μ.colLen j)

Tactic:
rintro rfl

Result:
case h.mk
μ : YoungDiagram
a b : ℕ
⊢ a < μ.colLen b ↔ a < μ.colLen b

Proof state:
μ : YoungDiagram
j : ℕ
⊢ μ.col j = Finset.range (μ.colLen j) ×ˢ {j}

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
μ : YoungDiagram
j a b : ℕ
⊢ (a, b) ∈ μ.col j ↔ (a, b) ∈ Finset.range (μ.colLen j) ×ˢ {j}

Proof state:
case h.mk
μ : YoungDiagram
a b : ℕ
⊢ a < μ.colLen b ↔ a < μ.colLen b

Tactic:
rfl

Result:
no goals

Proof state:
case h.mk
μ : YoungDiagram
j a b : ℕ
⊢ (a, b) ∈ μ.col j ↔ (a, b) ∈ Finset.range (μ.colLen j) ×ˢ {j}

Tactic:
simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_col_iff,
  mem_iff_lt_colLen, and_comm, and_congr_right_iff]

Result:
case h.mk
μ : YoungDiagram
j a b : ℕ
⊢ b = j → (a < μ.colLen b ↔ a < μ.colLen j)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p.denote ctx

Proof state:
ctx : Context
p : Poly
⊢ Expr.denote ctx (toExpr []) = denote ctx []

Tactic:
simp [toExpr, Expr.denote, Poly.denote]

Result:
no goals

Proof state:
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ Expr.denote ctx (toExpr ((k, v) :: p)) = denote ctx ((k, v) :: p)

Tactic:
simp [toExpr, Expr.denote, Poly.denote]

Result:
no goals

Proof state:
ctx : Context
p : Poly
⊢ Expr.denote ctx p.toExpr = denote ctx p

Tactic:
match p with
| [] => simp [toExpr, Expr.denote, Poly.denote]
| (k, v) :: p => simp [toExpr, Expr.denote, Poly.denote]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem card_le_card_of_forall_subsingleton (hs : ∀ a ∈ s, ∃ b, b ∈ t ∧ r a b)
    (ht : ∀ b ∈ t, ({ a ∈ s | r a b } : Set α).Subsingleton) : #s ≤ #t

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s * 1 ≤ #t * 1

Tactic:
exact card_mul_le_card_mul r
  (fun a h ↦ card_pos.2 (by
    rw [← coe_nonempty, coe_bipartiteAbove]
    exact hs _ h : (t.bipartiteAbove r a).Nonempty))
  (fun b h ↦ card_le_one.2 (by
    simp_rw [mem_bipartiteBelow]
    exact ht _ h))

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ {b | b ∈ t ∧ r a b}.Nonempty

Tactic:
exact hs _ h

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s ≤ #t

Tactic:
rw [← mul_one #s, ← mul_one #t]

Result:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s * 1 ≤ #t * 1

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ (bipartiteAbove r t a).Nonempty

Tactic:
rw [← coe_nonempty, coe_bipartiteAbove]

Result:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
a : α
h : a ∈ s
⊢ {b | b ∈ t ∧ r a b}.Nonempty

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1

Tactic:
exact ht _ h

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1

Tactic:
simp_rw [mem_bipartiteBelow]

Result:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ (a : α), a ∈ s ∧ r a b → ∀ (b_1 : α), b_1 ∈ s ∧ r b_1 b → a = b_1

Proof state:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
⊢ #s ≤ #t

Tactic:
classical
  rw [← mul_one #s, ← mul_one #t]
  exact card_mul_le_card_mul r
    (fun a h ↦ card_pos.2 (by
      rw [← coe_nonempty, coe_bipartiteAbove]
      exact hs _ h : (t.bipartiteAbove r a).Nonempty))
    (fun b h ↦ card_le_one.2 (by
      simp_rw [mem_bipartiteBelow]
      exact ht _ h))

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem eqv_class_mem' {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {x} :
    { y : α | mkClasses c H x y } ∈ c

Proof state:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x : α
⊢ {y | (mkClasses c H) x y} ∈ c

Tactic:
convert @Setoid.eqv_class_mem _ _ H x using 3

Result:
case h.e'_5.h.e'_2.h.a
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x x✝ : α
⊢ (mkClasses c H) x x✝ ↔ (mkClasses c H) x✝ x

Proof state:
case h.e'_5.h.e'_2.h.a
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x x✝ : α
⊢ (mkClasses c H) x x✝ ↔ (mkClasses c H) x✝ x

Tactic:
rw [Setoid.comm']

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- Consider a product of `g i (f i)` over a finset.  Suppose `g` is a function such as
`n ↦ (· ^ n)`, which maps a second argument of `1` to `1`. Then if `f` is replaced by the
corresponding multiplicative indicator function, the finset may be replaced by a possibly larger
finset without changing the value of the product. -/
@[to_additive "Consider a sum of `g i (f i)` over a finset.  Suppose `g` is a function such as
`n ↦ (n • ·)`, which maps a second argument of `0` to `0` (or a weighted sum of `f i * h i` or
`f i • h i`, where `f` gives the weights that are multiplied by some other function `h`). Then if
`f` is replaced by the corresponding indicator function, the finset may be replaced by a possibly
larger finset without changing the value of the sum."]
lemma prod_mulIndicator_subset_of_eq_one [One α] (f : ι → α) (g : ι → α → β) {s t : Finset ι}
    (h : s ⊆ t) (hg : ∀ a, g a 1 = 1) :
    ∏ i ∈ t, g i (mulIndicator ↑s f i) = ∏ i ∈ s, g i (f i)

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
⊢ ∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i ((↑s).mulIndicator f i)

Tactic:
rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
⊢ ∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)

Tactic:
calc
  _ = ∏ i ∈ s, g i (mulIndicator ↑s f i) := by rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
  _ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : One α
f : ι → α
g : ι → α → β
s t : Finset ι
h : s ⊆ t
hg : ∀ (a : ι), g a 1 = 1
i : ι
x✝ : i ∈ t
hn : i ∉ s
⊢ g i ((↑s).mulIndicator f i) = 1

Tactic:
simp [hn, hg]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean
theorem tendsto_measure_thickening_of_isClosed {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (thickening R s) ≠ ∞) (h's : IsClosed s) :
    Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ⊤
h's : IsClosed s
⊢ Tendsto (fun r => μ (thickening r s)) (𝓝[>] 0) (𝓝 (μ s))

Tactic:
convert tendsto_measure_thickening hs

Result:
case h.e'_5.h.e'_3.h.e'_6
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ⊤
h's : IsClosed s
⊢ s = closure s

Proof state:
case h.e'_5.h.e'_3.h.e'_6
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (thickening R s) ≠ ⊤
h's : IsClosed s
⊢ s = closure s

Tactic:
exact h's.closure_eq.symm

Result:
no goals
-- Mathlib/Analysis/Complex/LocallyUniformLimit.lean
theorem logDeriv_tendsto {ι : Type*} {p : Filter ι} (f : ι → ℂ → ℂ) (g : ℂ → ℂ)
    {s : Set ℂ} (hs : IsOpen s) (x : s) (hF : TendstoLocallyUniformlyOn f g p s)
    (hf : ∀ᶠ n : ι in p, DifferentiableOn ℂ (f n) s) (hg : g x ≠ 0) :
    Tendsto (fun n : ι => logDeriv (f n) x) p (𝓝 ((logDeriv g) x))

Proof state:
ι : Type u_3
p : Filter ι
f : ι → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
hs : IsOpen s
x : ↑s
hF : TendstoLocallyUniformlyOn f g p s
hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s
hg : g ↑x ≠ 0
⊢ Tendsto (fun n => (deriv (f n) / f n) ↑x) p (𝓝 ((deriv g / g) ↑x))

Tactic:
apply Tendsto.div ((hF.deriv hf hs).tendsto_at x.2) (hF.tendsto_at x.2) hg

Result:
no goals

Proof state:
ι : Type u_3
p : Filter ι
f : ι → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
hs : IsOpen s
x : ↑s
hF : TendstoLocallyUniformlyOn f g p s
hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s
hg : g ↑x ≠ 0
⊢ Tendsto (fun n => logDeriv (f n) ↑x) p (𝓝 (logDeriv g ↑x))

Tactic:
simp_rw [logDeriv]

Result:
ι : Type u_3
p : Filter ι
f : ι → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
hs : IsOpen s
x : ↑s
hF : TendstoLocallyUniformlyOn f g p s
hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s
hg : g ↑x ≠ 0
⊢ Tendsto (fun n => (deriv (f n) / f n) ↑x) p (𝓝 ((deriv g / g) ↑x))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem aux4 {a b c : Nat} (hidx : a < b * c) (h : c ≤ n) : a < b * n

Proof state:
case inr
n a b c : Nat
hidx : a < b * c
h✝ : c ≤ n
h : c = n
⊢ a < b * n

Tactic:
simp_all

Result:
no goals

Proof state:
n a b c : Nat
hidx : a < b * c
h : c ≤ n
⊢ a < b * n

Tactic:
cases Nat.lt_or_eq_of_le h with
| inl h => apply aux3 <;> assumption
| inr h => simp_all

Result:
no goals

Proof state:
case inl
n a b c : Nat
hidx : a < b * c
h✝ : c ≤ n
h : c < n
⊢ a < b * n

Tactic:
apply aux3 <;> assumption

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) :
    foldr (fun y r => (permutationsAux2 t ts r y id).2) r L =
      (L.flatMap fun y => (permutationsAux2 t ts [] y id).2) ++ r

Proof state:
case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).2) r L = flatMap (fun y => (permutationsAux2 t ts [] y id).2) L ++ r
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2) r (l :: L) =
    flatMap (fun y => (permutationsAux2 t ts [] y id).2) (l :: L) ++ r

Tactic:
simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]

Result:
no goals

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L = flatMap (fun y => (permutationsAux2 t ts [] y id).2) L ++ r

Tactic:
induction' L with l L ih

Result:
case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2) r [] =
    flatMap (fun y => (permutationsAux2 t ts [] y id).2) [] ++ r

case cons
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).2) r L = flatMap (fun y => (permutationsAux2 t ts [] y id).2) L ++ r
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2) r (l :: L) =
    flatMap (fun y => (permutationsAux2 t ts [] y id).2) (l :: L) ++ r

Proof state:
case nil
α : Type u_1
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).2) r [] =
    flatMap (fun y => (permutationsAux2 t ts [] y id).2) [] ++ r

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem elim_apply {f : γ → α → β} {x : α → β} {i : Option γ} {y : α} :
    i.elim x f y = i.elim (x y) fun j => f j y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : γ → α → β
x : α → β
i : Option γ
y : α
⊢ i.elim x f y = i.elim (x y) fun j => f j y

Tactic:
rw [elim_comp fun f : α → β => f y]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma uncurry_obj_curry_obj_flip_flip (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
    uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip = (F₁.prod F₂) ⋙ G :=
  Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
    dsimp
    simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])

Proof state:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁, 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁), F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁, F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))

Tactic:
simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp]

Result:
no goals

Proof state:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip).map (f₁, f₂) = eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp

Result:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁, 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁), F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁, F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))

Proof state:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
⊢ ∀ (X : B × D), (uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip).obj X = (F₁.prod F₂ ⋙ G).obj X

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_eq_default [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    [Inhabited (β a)] (h : containsKey a l = false) : getValueCast! a l = default

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
a : α
inst✝ : Inhabited (β a)
h : getValueCast? a l = none
⊢ getValueCast! a l = default

Tactic:
rw [getValueCast!_eq_getValueCast?, h, Option.get!_none]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
a : α
inst✝ : Inhabited (β a)
h : containsKey a l = false
⊢ getValueCast! a l = default

Tactic:
rw [containsKey_eq_isSome_getValueCast?, Bool.eq_false_iff, ne_eq,
  Option.not_isSome_iff_eq_none] at h

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
a : α
inst✝ : Inhabited (β a)
h : getValueCast? a l = none
⊢ getValueCast! a l = default
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem orderTop_smul_not_lt (r : R) (x : HahnSeries Γ V) : ¬ (r • x).orderTop < x.orderTop

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
by_cases hrx : r • x = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : ¬r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : ¬r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
simp only [orderTop_of_ne hrx, orderTop_of_ne <| right_ne_zero_of_smul hrx, WithTop.coe_lt_coe]

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : ¬r • x = 0
⊢ ¬⋯.min ⋯ < ⋯.min ⋯

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : ¬r • x = 0
⊢ ¬⋯.min ⋯ < ⋯.min ⋯

Tactic:
exact Set.IsWF.min_of_subset_not_lt_min
  (Function.support_smul_subset_right (fun _ => r) x.coeff)

Result:
no goals

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop

Tactic:
exact not_top_lt

Result:
no goals

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : r • x = 0
⊢ ¬(r • x).orderTop < x.orderTop

Tactic:
rw [hrx, orderTop_zero]

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
V : Type u_8
inst✝¹ : Zero V
inst✝ : SMulZeroClass R V
r : R
x : HahnSeries Γ V
hrx : r • x = 0
⊢ ¬⊤ < x.orderTop
-- Mathlib/Order/Defs/LinearOrder.lean
lemma compare_gt_iff_gt : compare a b = .gt ↔ a > b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
⊢ True ↔ a > b

Tactic:
have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
h : b < a
⊢ True ↔ a > b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ a > b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]

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

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ True ↔ a > b

Tactic:
case _ h₁ h₂ =>
  have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
  rwa [true_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h₁ : ¬a < b
h₂ : ¬a = b
h : b < a
⊢ True ↔ a > b

Tactic:
rwa [true_iff]

Result:
no goals

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

Tactic:
split_ifs <;> simp only [*, lt_irrefl, not_lt_of_gt, reduceCtorEq]

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ True ↔ a > b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forM_append [Monad m] [LawfulMonad m] (l₁ : Vector α n) (l₂ : Vector α n') (f : α → m PUnit) :
    forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f)

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m PUnit
l₁ l₂ : Array α
⊢ forM ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ }) f = do
    forM { toArray := l₁, size_toArray := ⋯ } f
    forM { toArray := l₂, size_toArray := ⋯ } f

Tactic:
simp

Result:
no goals

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n' : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₂ : Vector α n'
f : α → m PUnit
l₁ : Array α
⊢ forM ({ toArray := l₁, size_toArray := ⋯ } ++ l₂) f = do
    forM { toArray := l₁, size_toArray := ⋯ } f
    forM l₂ f

Tactic:
rcases l₂ with ⟨l₂, rfl⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m PUnit
l₁ l₂ : Array α
⊢ forM ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ }) f = do
    forM { toArray := l₁, size_toArray := ⋯ } f
    forM { toArray := l₂, size_toArray := ⋯ } f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n n' : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₁ : Vector α n
l₂ : Vector α n'
f : α → m PUnit
⊢ forM (l₁ ++ l₂) f = do
    forM l₁ f
    forM l₂ f

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n' : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l₂ : Vector α n'
f : α → m PUnit
l₁ : Array α
⊢ forM ({ toArray := l₁, size_toArray := ⋯ } ++ l₂) f = do
    forM { toArray := l₁, size_toArray := ⋯ } f
    forM l₂ f
-- Mathlib/Logic/Godel/GodelBetaFunction.lean
lemma coprimes_lt (a : Fin m → ℕ) (i) : a i < coprimes a i

Proof state:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < Nat.supOfSeq a
⊢ a i < Nat.coprimes a i

Tactic:
have h₂ : supOfSeq a ≤ (i + 1) * (supOfSeq a)! + 1 :=
  le_trans (self_le_factorial _) (le_trans (Nat.le_mul_of_pos_left (supOfSeq a)! (succ_pos i))
    (le_add_right _ _))

Result:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < Nat.supOfSeq a
h₂ : Nat.supOfSeq a ≤ (↑i + 1) * (Nat.supOfSeq a)! + 1
⊢ a i < Nat.coprimes a i

Proof state:
m : ℕ
a : Fin m → ℕ
i : Fin m
⊢ i ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < Nat.supOfSeq a
h₂ : Nat.supOfSeq a ≤ (↑i + 1) * (Nat.supOfSeq a)! + 1
⊢ a i < Nat.coprimes a i

Tactic:
simpa only [coprimes] using lt_of_lt_of_le h₁ h₂

Result:
no goals

Proof state:
m : ℕ
a : Fin m → ℕ
i : Fin m
⊢ a i < Nat.coprimes a i

Tactic:
have h₁ : a i < supOfSeq a :=
  Nat.lt_add_one_iff.mpr (le_max_of_le_right <| Finset.le_sup (by simp))

Result:
m : ℕ
a : Fin m → ℕ
i : Fin m
h₁ : a i < Nat.supOfSeq a
⊢ a i < Nat.coprimes a i