harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/FintypeCat.lean
lemma uSwitch_map_uSwitch_map {X Y : FintypeCat.{u}} (f : X ⟶ Y) :
    uSwitch.map (uSwitch.map f) =
    (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom ≫
      f ≫ (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans
      Y.uSwitchEquiv)).inv

Proof state:
X Y : FintypeCat
f : X ⟶ Y
⊢ uSwitch.map (uSwitch.map f) =
    (equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom ≫
      f ≫ (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv

Tactic:
ext x

Result:
case h
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj (uSwitch.obj X)).carrier
⊢ uSwitch.map (uSwitch.map f) x =
    ((equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom ≫
        f ≫ (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv)
      x

Proof state:
case h
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj (uSwitch.obj X)).carrier
⊢ uSwitch.map (uSwitch.map f) x =
    ((equivEquivIso ((uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv)).hom ≫
        f ≫ (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv)
      x

Tactic:
simp only [comp_apply, equivEquivIso_apply_hom, Equiv.trans_apply]

Result:
case h
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj (uSwitch.obj X)).carrier
⊢ uSwitch.map (uSwitch.map f) x =
    (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv
      (f (X.uSwitchEquiv ((uSwitch.obj X).uSwitchEquiv x)))

Proof state:
case h
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj (uSwitch.obj X)).carrier
⊢ uSwitch.map (uSwitch.map f) x =
    (equivEquivIso ((uSwitch.obj Y).uSwitchEquiv.trans Y.uSwitchEquiv)).inv
      (f (X.uSwitchEquiv ((uSwitch.obj X).uSwitchEquiv x)))

Tactic:
rfl

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem Primrec.to_comp {α σ} [Primcodable α] [Primcodable σ] {f : α → σ} (hf : Primrec f) :
    Computable f :=
  (Nat.Partrec.ppred.comp (Nat.Partrec.of_primrec hf)).of_eq fun n => by
    simp; cases decode (α := α) n <;> simp

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(encode (Option.map f (decode n))).ppred = (↑(decode n)).bind fun a => Part.some (encode (f a))

Tactic:
cases decode (α := α) n <;> simp

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ (do
      let n ← (↑fun n => encode (Option.map f (decode n))) n
      ↑n.ppred) =
    (↑(decode n)).bind fun a => map encode (↑f a)

Tactic:
simp

Result:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ ↑(encode (Option.map f (decode n))).ppred = (↑(decode n)).bind fun a => Part.some (encode (f a))
-- Mathlib/Order/Iterate.lean
theorem iterate_pos_lt_iff_map_lt (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n}
    (hn : 0 < n) : f^[n] x < g^[n] x ↔ f x < g x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
rcases lt_trichotomy (f x) (g x) with (H | H | H)

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Proof state:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
simp only [*, iterate_pos_lt_of_map_lt]

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filterMap_filter (f : α → Option β) (s : Multiset α) :
    filterMap f (filter p s) = filterMap (fun x => if p x then f x else none) s :=
  Quot.inductionOn s fun l => congr_arg ofList <| by simpa using List.filterMap_filter p f l

Proof state:
α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b => decide (p b)) l) = List.filterMap (fun x => if p x then f x else none) l

Tactic:
simpa using List.filterMap_filter p f l

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[simp]
lemma lift_fst_snd {X Y : C} : lift (fst X Y) (snd X Y) = 𝟙 (X ⊗ Y)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y : C
⊢ lift (fst X Y) (snd X Y) = 𝟙 (X ⊗ Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_filter_add_dens_filter_not_eq_dens {α : Type*} [Fintype α] {s : Finset α}
    (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
    dens (s.filter p) + dens (s.filter fun a ↦ ¬ p a) = dens s

Proof state:
α : Type u_4
inst✝² : Fintype α
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ (filter p s).dens + (filter (fun a => ¬p a) s).dens = s.dens

Tactic:
classical
rw [← dens_union_of_disjoint (disjoint_filter_filter_neg ..), filter_union_filter_neg_eq]

Result:
no goals

Proof state:
α : Type u_4
inst✝² : Fintype α
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ (filter p s).dens + (filter (fun a => ¬p a) s).dens = s.dens

Tactic:
rw [← dens_union_of_disjoint (disjoint_filter_filter_neg ..), filter_union_filter_neg_eq]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_insert (x : E) {s : Set E} :
    IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
x : E
s : Set E
⊢ IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s

Tactic:
simp only [← singleton_union, isVonNBounded_union, isVonNBounded_singleton, true_and]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma partSize_le (m : Fin c.length) : c.partSize m ≤ n

Proof state:
n : ℕ
c : OrderedFinpartition n
m : Fin c.length
⊢ c.partSize m ≤ n

Tactic:
simpa only [Fintype.card_fin] using Fintype.card_le_of_injective _ (c.emb_strictMono m).injective

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem OneOneReducible.of_equiv_symm {α β} [Primcodable α] [Primcodable β] {e : α ≃ β}
    (q : β → Prop) (h : Computable e.symm) : q ≤₁ (q ∘ e)

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ⇑e) ∘ ⇑e.symm) x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
⊢ q ≤₁ (q ∘ ⇑e)

Tactic:
convert OneOneReducible.of_equiv _ h

Result:
case h.e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
⊢ q = (q ∘ ⇑e) ∘ ⇑e.symm

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
⊢ q = (q ∘ ⇑e) ∘ ⇑e.symm

Tactic:
funext

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
e : α ≃ β
q : β → Prop
h : Computable ⇑e.symm
x✝ : β
⊢ q x✝ = ((q ∘ ⇑e) ∘ ⇑e.symm) x✝
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem lt_nadd_iff : a < b ♯ c ↔ (∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c'

Proof state:
a b c : Ordinal.{u}
⊢ a < (⨆ x, succ (↑x ♯ c)) ⊔ ⨆ x, succ (b ♯ ↑x) ↔ (∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c'

Tactic:
simp [Ordinal.lt_iSup_iff]

Result:
no goals

Proof state:
a b c : Ordinal.{u}
⊢ a < b ♯ c ↔ (∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c'

Tactic:
rw [nadd]

Result:
a b c : Ordinal.{u}
⊢ a < (⨆ x, succ (↑x ♯ c)) ⊔ ⨆ x, succ (b ♯ ↑x) ↔ (∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c'
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem nonzeroMinimum_eq_zero_iff {xs : List Nat} :
    xs.nonzeroMinimum = 0 ↔ ∀ x ∈ xs, x = 0

Proof state:
xs : List Nat
⊢ xs.nonzeroMinimum = 0 ↔ ∀ (x : Nat), x ∈ xs → x = 0

Tactic:
simp [nonzeroMinimum, Option.getD_eq_iff, min?_eq_none_iff, min?_eq_some_iff'',
  filter_eq_nil_iff, mem_filter]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem coeff_mul {a₃ c₂ k : ℕ}
    (a₁ a₂ : ℕ) (_ : a₃ = c₂ * k) : a₁ ^ a₂ * a₃ = (a₁ ^ a₂ * c₂) * k

Proof state:
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
a₃ c₂ k a₁ a₂ : ℕ
x✝ : a₃ = c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

Tactic:
subst_vars

Result:
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
-- Mathlib/Data/Set/Card.lean
lemma cast_ncard_sdiff {R : Type*} [AddGroupWithOne R] (hst : s ⊆ t) (ht : t.Finite) :
    ((t \ s).ncard : R) = t.ncard - s.ncard

Proof state:
α : Type u_1
s t : Set α
R : Type u_3
inst✝ : AddGroupWithOne R
hst : s ⊆ t
ht : t.Finite
⊢ ↑(t \ s).ncard = ↑t.ncard - ↑s.ncard

Tactic:
rw [ncard_diff hst (ht.subset hst), Nat.cast_sub (ncard_le_ncard hst ht)]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn (hf : HasFPowerSeriesOnBall f p x r) :
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
      (EMetric.ball (0 : E) r)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (EMetric.ball 0 r)

Tactic:
simpa using hf.tendstoLocallyUniformlyOn

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (EMetric.ball 0 r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (EMetric.ball 0 r)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_ediv_self (a : Int) (h : a ≠ 0) : (-a) / a = -1

Proof state:
a : Int
h : a ≠ 0
⊢ -a / a = -1

Tactic:
rw [neg_ediv_of_dvd (Int.dvd_refl a), Int.ediv_self h]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Icc_iff_Ici (h : a < b) :
    ContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIciTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Icc a b) a ↔ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsGE h]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem iInter_Iic_rat : ⋂ r : ℚ, Iic (r : ℝ) = ∅

Proof state:
⊢ ⋂ r, Iic ↑r = ∅

Tactic:
exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_sub_mul_self_real (x y : F) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
simpa using h

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
have h := @norm_sub_mul_self ℝ _ _ _ _ x y

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
-- Mathlib/CategoryTheory/Preadditive/Mat.lean
theorem id_apply_self (M : Mat R) (i : M) : (𝟙 M : Matrix M M R) i i = 1

Proof state:
R : Type u
inst✝ : Semiring R
M : Mat R
i : M.carrier
⊢ 𝟙 M i i = 1

Tactic:
simp [id_apply]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma left_mul_prod_Ioo (h : a < b) : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x

Tactic:
rw [Ico_eq_cons_Ioo h, prod_cons]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
    (∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k)) =
      ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

Proof state:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

Tactic:
rw [prod_sigma', prod_sigma']

Result:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m => range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m => range (n - m), f x.fst x.snd

Proof state:
case refine_1
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a b : ℕ), a < n → b ≤ a → b < n

Tactic:
exact fun a b han hba ↦ lt_of_le_of_lt hba han

Result:
no goals

Proof state:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∏ x ∈ (range n).sigma fun m => range (m + 1), f x.snd (x.fst - x.snd) =
    ∏ x ∈ (range n).sigma fun m => range (n - m), f x.fst x.snd

Tactic:
refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
  simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
    Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, imp_self,
    implies_true, Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
    add_tsub_cancel_left, heq_eq_eq]

Result:
case refine_1
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : ℕ → ℕ → M
⊢ ∀ (a b : ℕ), a < n → b ≤ a → b < n
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_add_one {f : ι → α} (s : Finset ι) :
    ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
f : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
simp only [prod_add, prod_const_one, mul_one]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
f : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

Tactic:
classical simp only [prod_add, prod_const_one, mul_one]

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Basic.lean
theorem LinearMap.isNoetherian_iff_of_bijective {S P} [Semiring S] [AddCommMonoid P] [Module S P]
    {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective l) :
    IsNoetherian R M ↔ IsNoetherian S P

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
e : Submodule R M ≃o Submodule S P := orderIsoMapComapOfBijective l hl
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)

Tactic:
exact ⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)

Tactic:
let e := Submodule.orderIsoMapComapOfBijective l hl

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
e : Submodule R M ≃o Submodule S P := orderIsoMapComapOfBijective l hl
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ IsNoetherian R M ↔ IsNoetherian S P

Tactic:
simp_rw [isNoetherian_iff']

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective ⇑l
⊢ WellFoundedGT (Submodule R M) ↔ WellFoundedGT (Submodule S P)
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_comp_le (f : E →SL[σ₁₂] F) : ‖h.comp f‖ ≤ ‖h‖ * ‖f‖ :=
  csInf_le bounds_bddBelow
    ⟨mul_nonneg (opNorm_nonneg _) (opNorm_nonneg _), fun x => by
      rw [mul_assoc]
      exact h.le_opNorm_of_le (f.le_opNorm x)⟩

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup F
inst✝⁹ : SeminormedAddCommGroup G
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ ‖(h.comp f) x‖ ≤ ‖h‖ * (‖f‖ * ‖x‖)

Tactic:
exact h.le_opNorm_of_le (f.le_opNorm x)

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup F
inst✝⁹ : SeminormedAddCommGroup G
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ ‖(h.comp f) x‖ ≤ ‖h‖ * ‖f‖ * ‖x‖

Tactic:
rw [mul_assoc]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_5
G : Type u_7
inst✝¹¹ : SeminormedAddCommGroup E
inst✝¹⁰ : SeminormedAddCommGroup F
inst✝⁹ : SeminormedAddCommGroup G
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜₂
inst✝⁶ : NontriviallyNormedField 𝕜₃
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜₃ G
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
h : F →SL[σ₂₃] G
f : E →SL[σ₁₂] F
x : E
⊢ ‖(h.comp f) x‖ ≤ ‖h‖ * (‖f‖ * ‖x‖)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getCast?_eq [BEq α] [LawfulBEq α] {l : AssocList α β} {a : α} :
    l.getCast? a = getValueCast? a l.toList

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : AssocList α β
a : α
⊢ getCast? a l = getValueCast? a l.toList

Tactic:
induction l <;> simp_all [getCast?, List.getValueCast?]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_snd_darts {u v : V} (p : G.Walk u v) : p.darts.map (·.snd) = p.support.tail

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ List.map (fun x => x.toProd.2) p.darts = p.support.tail

Tactic:
simpa using congr_arg List.tail (cons_map_snd_darts p)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
lemma Pi.map_eq_prod_map [∀ i, Decidable (P i)] : Pi.map f =
    ((Pi.binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd _ _)).hom ≫
      prod.map (Pi.map (fun (i : {x : I // P x}) ↦ f i.val))
      (Pi.map (fun (i : {x : I // ¬ P x}) ↦ f i.val)) ≫
        ((Pi.binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd _ _)).inv

Proof state:
case h₂
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ (map f ≫
        ((Cones.forget (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).mapIso
            ((binaryFanOfPropIsLimit Y P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).pt) ⋯)))).hom) ≫
      prod.snd =
    (((Cones.forget (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).mapIso
            ((binaryFanOfPropIsLimit X P).uniqueUpToIso
              ((limit.isLimit (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).ofIsoLimit
                (Cones.ext (Iso.refl (limit.cone (pair (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).pt) ⋯)))).hom ≫
        prod.map (map fun i => f ↑i) (map fun i => f ↑i)) ≫
      prod.snd

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom ≫
      prod.map (map fun i => f ↑i) (map fun i => f ↑i) ≫
        ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).inv

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv]

Result:
C : Type u_1
I : Type u_2
inst✝⁷ : Category.{u_3, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i => X ↑i
inst✝³ : HasProduct fun i => X ↑i
inst✝² : HasProduct fun i => Y ↑i
inst✝¹ : HasProduct fun i => Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f ≫ ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i => Y ↑i) (∏ᶜ fun i => Y ↑i))).hom =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i))).hom ≫
      prod.map (map fun i => f ↑i) (map fun i => f ↑i)
-- Mathlib/Data/Set/Image.lean
theorem insert_image_compl_eq_range (f : α → β) (x : α) : insert (f x) (f '' {x}ᶜ) = range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ insert (f x) (f '' {x}ᶜ) = range f

Tactic:
rw [← image_insert_eq, insert_eq, union_compl_self, image_univ]

Result:
no goals