harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem StrongEpi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
    (e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f ↔ StrongEpi g

Tactic:
constructor <;> intro

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongEpi f
⊢ StrongEpi g

case mpr
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongEpi g
⊢ StrongEpi f

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongEpi f
⊢ StrongEpi g

case mpr
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongEpi g
⊢ StrongEpi f

Tactic:
exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem isOrtho_span {s t : Set E} :
    span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u⦄, u ∈ s → ∀ ⦃v⦄, v ∈ t → ⟪u, v⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s t : Set E
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → inner u v = 0

Tactic:
simp_rw [span_eq_iSup_of_singleton_spans s, span_eq_iSup_of_singleton_spans t, isOrtho_iSup_left,
  isOrtho_iSup_right, isOrtho_iff_le, span_le, Set.subset_def, SetLike.mem_coe,
  mem_orthogonal_singleton_iff_inner_left, Set.mem_singleton_iff, forall_eq]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma mul_stabilizer_self : s * stabilizer G s = s

Proof state:
G : Type u_1
inst✝ : CommGroup G
s : Set G
⊢ s * ↑(stabilizer G s) = s

Tactic:
rw [mul_comm, stabilizer_mul_self]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem im_eq_zero_of_le {a : K} (h : ‖a‖ ≤ re a) : im a = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ im a = 0

Tactic:
simpa only [mul_self_norm a, normSq_apply, self_eq_add_right, mul_self_eq_zero]
  using congr_arg (fun z => z * z) ((re_le_norm a).antisymm h)

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
/-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`. -/
@[to_additive]
lemma smul_mul_smul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
    [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β) :
    (a • b) * (c • d) = (a * c) • (b * d)

Proof state:
α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
this : SMulCommClass β α β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
exact smul_smul_smul_comm a b c d

Result:
no goals

Proof state:
α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
have : SMulCommClass β α β := .symm ..

Result:
α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
this : SMulCommClass β α β
⊢ a • b * c • d = (a * c) • (b * d)
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0)
    (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith K f s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ≥0
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y
⊢ LipschitzOnWith K f s

Tactic:
simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k} :
    (m.modify k f).getKey! k' =
      if k == k' then
        if m.contains k then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
inst✝ : Inhabited α
k k' : α
f : β k → β k
⊢ (m.modify k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

Tactic:
simp_to_model [modify] using List.getKey!_modifyKey

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_erase_self (ha : a ∈ s) : s \ s.erase a = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ s \ s.erase a = {a}

Tactic:
rw [sdiff_erase ha, Finset.sdiff_self, insert_emptyc_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {i : Nat}, l₁.length ≤ i →
  (l₁ ++ l₂)[i]? = l₂[i - l₁.length]?
| [], _, _, _ => rfl
| a :: l, _, i+1, h₁ => by
  rw [cons_append]
  simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]

Proof state:
α : Type u_1
a : α
l x✝ : List α
i : Nat
h₁ : (a :: l).length ≤ i + 1
⊢ (a :: (l ++ x✝))[i + 1]? = x✝[i + 1 - (a :: l).length]?

Tactic:
simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]

Result:
no goals

Proof state:
α : Type u_1
a : α
l x✝ : List α
i : Nat
h₁ : (a :: l).length ≤ i + 1
⊢ (a :: l ++ x✝)[i + 1]? = x✝[i + 1 - (a :: l).length]?

Tactic:
rw [cons_append]

Result:
α : Type u_1
a : α
l x✝ : List α
i : Nat
h₁ : (a :: l).length ≤ i + 1
⊢ (a :: (l ++ x✝))[i + 1]? = x✝[i + 1 - (a :: l).length]?
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_compl_finset_of_infinite {α : Type*} [Infinite α] (s : Finset α) :
    #((↑s)ᶜ : Set α) = #α

Proof state:
case h2
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑↑s < #α

Tactic:
exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑(↑s)ᶜ = #α

Tactic:
apply mk_compl_of_infinite

Result:
case h2
α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑↑s < #α
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem continuousWithinAt_iff [PseudoMetricSpace β] {f : α → β} {a : α} {s : Set α} :
    ContinuousWithinAt f s a ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε

Tactic:
rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem Subsingleton.stronglyMeasurable' [Subsingleton α] (f : α → β) : StronglyMeasurable f :=
  stronglyMeasurable_const' fun x y => by rw [Subsingleton.elim x y]

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Subsingleton α
f : α → β
x y : α
⊢ f x = f y

Tactic:
rw [Subsingleton.elim x y]

Result:
no goals
-- Mathlib/Order/CompleteSublattice.lean
protected lemma isCompl_iff {a b : L} :
    IsCompl a b ↔ IsCompl (a : α) (b : α)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ IsCompl a b ↔ IsCompl ↑a ↑b

Tactic:
rw [isCompl_iff, isCompl_iff, CompleteSublattice.disjoint_iff, CompleteSublattice.codisjoint_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem IsPushout.of_map_of_faithful [ReflectsColimit (span f g) F] [F.Faithful]
    (H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) : IsPushout f g h i :=
  H.of_map F (F.map_injective <| by simpa only [F.map_comp] using H.w)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝¹ : ReflectsColimit (span f g) F
inst✝ : F.Faithful
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ F.map (f ≫ h) = F.map (g ≫ i)

Tactic:
simpa only [F.map_comp] using H.w

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eqRecOn_heq.{u_1, u_2} {α : Sort u_2} {a : α}
        {motive : (x : α) → a = x → Sort u_1} {b : α} (h : a = b) (v : motive a (Eq.refl a))
        : HEq (@Eq.recOn α a motive b h v) v

Proof state:
α : Sort u_2
a : α
motive : (x : α) → a = x → Sort u_1
b : α
h : a = b
v : motive a ⋯
⊢ HEq (Eq.recOn h v) v

Tactic:
subst h

Result:
α : Sort u_2
a : α
motive : (x : α) → a = x → Sort u_1
v : motive a ⋯
⊢ HEq (Eq.recOn ⋯ v) v

Proof state:
α : Sort u_2
a : α
motive : (x : α) → a = x → Sort u_1
v : motive a ⋯
⊢ HEq (Eq.recOn ⋯ v) v

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_map_left (l₁ : List α) (l₂ : List β) (f : α → α') (g : α' → β → γ) :
    zipWith g (l₁.map f) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
α' : Type u_3
γ : Type u_4
l₁ : List α
l₂ : List β
f : α → α'
g : α' → β → γ
⊢ zipWith g (map f l₁) l₂ = zipWith (fun a b => g (f a) b) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem Nodup.sigma {σ : α → Type*} {t : ∀ a, Multiset (σ a)} :
    Nodup s → (∀ a, Nodup (t a)) → Nodup (s.sigma t) :=
  Quot.induction_on s fun l₁ => by
    choose f hf using fun a => Quotient.exists_rep (t a)
    simpa [← funext hf] using List.Nodup.sigma

Proof state:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), ⟦f a⟧ = t a
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
simpa [← funext hf] using List.Nodup.sigma

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup

Tactic:
choose f hf using fun a => Quotient.exists_rep (t a)

Result:
α : Type u_1
s : Multiset α
σ : α → Type u_5
t : (a : α) → Multiset (σ a)
l₁ : List α
f : (a : α) → List (σ a)
hf : ∀ (a : α), ⟦f a⟧ = t a
⊢ Nodup (Quot.mk (⇑(List.isSetoid α)) l₁) →
    (∀ (a : α), (t a).Nodup) → (Multiset.sigma (Quot.mk (⇑(List.isSetoid α)) l₁) t).Nodup
-- Mathlib/Data/Nat/ModEq.lean
theorem le_mod_add_mod_of_dvd_add_of_not_dvd {a b c : ℕ} (h : c ∣ a + b) (ha : ¬c ∣ a) :
    c ≤ a % c + b % c :=
  by_contradiction fun hc => by
    have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
    simp_all [dvd_iff_mod_eq_zero]

Proof state:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
this : (a + b) % c = a % c + b % c
⊢ False

Tactic:
simp_all [dvd_iff_mod_eq_zero]

Result:
no goals

Proof state:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
⊢ False

Tactic:
have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)

Result:
a b c : ℕ
h : c ∣ a + b
ha : ¬c ∣ a
hc : ¬c ≤ a % c + b % c
this : (a + b) % c = a % c + b % c
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sub_ediv_of_dvd_sub {a b c : Int}
    (hcab : c ∣ a - b) : (a - b) / c = a / c - b / c

Proof state:
a b c : Int
hcab : c ∣ a - b
⊢ (a - b) / c = a / c - b / c

Tactic:
rw [← Int.add_sub_cancel ((a-b) / c), ← Int.add_ediv_of_dvd_left hcab, Int.sub_add_cancel]

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem mem_ssubsets {s t : Finset α} : t ∈ s.ssubsets ↔ t ⊂ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∈ s.ssubsets ↔ t ⊂ s

Tactic:
rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
@[simp]
lemma map_union [DecidableEq β] {f : α → β} (finj : Function.Injective f) {s t : Multiset α} :
    map f (s ∪ t) = map f s ∪ map f t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ =>
    congr_arg ofList (by rw [List.map_append f, List.map_diff finj])

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂

Tactic:
rw [List.map_append f, List.map_diff finj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem positivize?_eq_some (w : positivize? (s, x) = some (s', x')) :
    positivizeConstraint s x = s' ∧ positivizeCoeffs s x = x'

Proof state:
s : Constraint
x : Coeffs
s' : Constraint
x' : Coeffs
w : positivize? (s, x) = some (s', x')
⊢ positivizeConstraint s x = s' ∧ positivizeCoeffs s x = x'

Tactic:
simp_all [positivizeConstraint, positivizeCoeffs, positivize]

Result:
no goals
-- Mathlib/Data/Multiset/Dedup.lean
theorem _root_.List.Subset.dedup_append_left {s t : List α} (h : t ⊆ s) :
    List.dedup (s ++ t) ~ List.dedup s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (s ++ t).dedup ~ s.dedup

Tactic:
rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_iff_right_eq_or_left_mem_image_Ici {x y z : P} :
    Wbtw R x y z ↔ z = y ∨ x ∈ lineMap z y '' Set.Ici (1 : R)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
⊢ Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(lineMap z y) '' Set.Ici 1

Tactic:
rw [wbtw_comm, wbtw_iff_left_eq_or_right_mem_image_Ici]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/T0Sierpinski.lean
theorem productOfMemOpens_isInducing : IsInducing (productOfMemOpens X)

Proof state:
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ i, induced (fun x => x ∈ i) inferInstance

Tactic:
apply eq_induced_by_maps_to_sierpinski

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsInducing ⇑(productOfMemOpens X)

Tactic:
convert inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u

Result:
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
⊢ inst✝ = ⨅ i, induced (fun x => x ∈ i) inferInstance
-- Mathlib/Data/List/Infix.lean
theorem get_inits (l : List α) (n : Fin (length (inits l))) : (inits l).get n = l.take n

Proof state:
α : Type u_1
l : List α
n : Fin l.inits.length
⊢ l.inits.get n = take (↑n) l

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_tProd_mk (l : List δ) : Measurable (@TProd.mk δ π l)

Proof state:
case cons
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
i : δ
l : List δ
ih : Measurable (TProd.mk l)
⊢ Measurable (TProd.mk (i :: l))

Tactic:
exact (measurable_pi_apply i).prod_mk ih

Result:
no goals

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
l : List δ
⊢ Measurable (TProd.mk l)

Tactic:
induction' l with i l ih

Result:
case nil
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
⊢ Measurable (TProd.mk [])

case cons
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
i : δ
l : List δ
ih : Measurable (TProd.mk l)
⊢ Measurable (TProd.mk (i :: l))

Proof state:
case nil
δ : Type u_4
π : δ → Type u_6
inst✝ : (x : δ) → MeasurableSpace (π x)
⊢ Measurable (TProd.mk [])

Tactic:
exact measurable_const

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem coprod_neBot_iff : (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (f.coprod g).NeBot ↔ f.NeBot ∧ Nonempty β ∨ Nonempty α ∧ g.NeBot

Tactic:
simp [Filter.coprod]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_disjiUnion (s : Finset ι) (t : ι → Finset α) (h) :
    ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x

Proof state:
case e_b
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ 1 = Multiset.foldr (fun x1 x2 => x1 * x2) 1 (Multiset.map (fun i => 1) s.val)

Tactic:
exact prod_const_one.symm

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ Multiset.foldr (fun x1 x2 => x1 * x2) 1 (Multiset.map (fun x => f x) (s.val.bind fun a => (t a).val)) =
    Multiset.foldr (fun x1 x2 => x1 * x2) (Multiset.foldr (fun x1 x2 => x1 * x2) 1 (Multiset.map (fun i => 1) s.val))
      (Multiset.map (fun x => f x) (s.val.bind fun a => (t a).val))

Tactic:
congr

Result:
case e_b
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ 1 = Multiset.foldr (fun x1 x2 => x1 * x2) 1 (Multiset.map (fun i => 1) s.val)

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x

Tactic:
refine Eq.trans ?_ (fold_disjiUnion h)

Result:
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.disjiUnion t h, f x =
    fold (fun x1 x2 => x1 * x2) (fold (fun x1 x2 => x1 * x2) 1 (fun i => 1) s) (fun x => f x) (s.disjiUnion t h)

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.disjiUnion t h, f x =
    fold (fun x1 x2 => x1 * x2) (fold (fun x1 x2 => x1 * x2) 1 (fun i => 1) s) (fun x => f x) (s.disjiUnion t h)

Tactic:
dsimp [Finset.prod, Multiset.prod, Multiset.fold, Finset.disjUnion, Finset.fold]

Result:
ι : Type u_1
α : Type u_3
β : Type u_4
f : α → β
inst✝ : CommMonoid β
s : Finset ι
t : ι → Finset α
h : (↑s).PairwiseDisjoint t
⊢ Multiset.foldr (fun x1 x2 => x1 * x2) 1 (Multiset.map (fun x => f x) (s.val.bind fun a => (t a).val)) =
    Multiset.foldr (fun x1 x2 => x1 * x2) (Multiset.foldr (fun x1 x2 => x1 * x2) 1 (Multiset.map (fun i => 1) s.val))
      (Multiset.map (fun x => f x) (s.val.bind fun a => (t a).val))
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem eqToHom_f {P Q : Karoubi C} (h : P = Q) :
    Karoubi.Hom.f (eqToHom h) = P.p ≫ eqToHom (congr_arg Karoubi.X h)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (eqToHom ⋯).f = P.p ≫ eqToHom ⋯

Tactic:
simp only [eqToHom_refl, Karoubi.id_f, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
h : P = Q
⊢ (eqToHom h).f = P.p ≫ eqToHom ⋯

Tactic:
subst h

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (eqToHom ⋯).f = P.p ≫ eqToHom ⋯
-- Mathlib/Order/Filter/AtTopBot/ModEq.lean
theorem frequently_odd : ∃ᶠ m : ℕ in atTop, Odd m

Proof state:
⊢ ∃ᶠ (m : ℕ) in atTop, Odd m

Tactic:
simpa only [odd_iff] using frequently_mod_eq one_lt_two

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_nhds_of_mem_interior_range {x : M} (hx : x ∈ f.source)
    (h'x : f.extend I x ∈ interior (range I)) :
    map (f.extend I) (𝓝 x) = 𝓝 (f.extend I x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
⊢ map (↑(f.extend I)) (𝓝 x) = 𝓝 (↑(f.extend I) x)

Tactic:
rw [f.map_extend_nhds hx, nhdsWithin_eq_nhds]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
⊢ range ↑I ∈ 𝓝 (↑(f.extend I) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : ↑(f.extend I) x ∈ interior (range ↑I)
⊢ range ↑I ∈ 𝓝 (↑(f.extend I) x)

Tactic:
exact mem_of_superset (isOpen_interior.mem_nhds h'x) interior_subset

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
theorem opNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖ :=
  le_antisymm (by simpa only [flip_flip] using le_norm_flip f.flip) (le_norm_flip f)

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
E : Type u_4
F : Type u_6
G : Type u_8
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✝¹ : RingHomIsometric σ₂₃
inst✝ : RingHomIsometric σ₁₃
f : E →SL[σ₁₃] F →SL[σ₂₃] G
⊢ ‖f.flip‖ ≤ ‖f‖

Tactic:
simpa only [flip_flip] using le_norm_flip f.flip

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getThenInsertIfNew?_snd_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF)
    {a : α} {b : β a} : (m.getThenInsertIfNew? a b).2 =
      (Raw₀.getThenInsertIfNew? ⟨m, h.size_buckets_pos⟩ a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ (m.getThenInsertIfNew? a b).snd = (Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).snd.val

Tactic:
simp [Raw.getThenInsertIfNew?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem quotientToQuotientRangePowQuotSuccAux_mk {i : ℕ} {a : S} (a_mem : a ∈ P ^ i) (x : S) :
    quotientToQuotientRangePowQuotSuccAux p P a_mem (Submodule.Quotient.mk x) =
      Submodule.Quotient.mk ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩

Proof state:
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
p : Ideal R
P : Ideal S
inst✝ : Algebra R S
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Submodule.Quotient.mk x) =
    Submodule.Quotient.mk ⟨(Quotient.mk (P ^ e)) (a * x), ⋯⟩

Tactic:
apply Quotient.map'_mk''

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma coe_ennreal_toReal {x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x

Proof state:
x : ℝ≥0∞
hx : x ≠ ⊤
⊢ ↑x.toReal = ↑x

Tactic:
lift x to ℝ≥0 using hx

Result:
case intro
x : ℝ≥0
⊢ ↑(↑x).toReal = ↑↑x

Proof state:
case intro
x : ℝ≥0
⊢ ↑(↑x).toReal = ↑↑x

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_pi {π : α → Sort*} : IsEmpty (∀ a, π a) ↔ ∃ a, IsEmpty (π a)

Proof state:
α : Sort u_1
π : α → Sort u_4
⊢ IsEmpty ((a : α) → π a) ↔ ∃ a, IsEmpty (π a)

Tactic:
simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem map_ceil (f : F) (hf : StrictMono f) (a : α) : ⌈f a⌉ = ⌈a⌉ :=
  ceil_congr fun n => by rw [← map_intCast f, hf.le_iff_le]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : LinearOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
n : ℤ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
rw [← map_intCast f, hf.le_iff_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_cons_of_true [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
    getValue? a (⟨k, v⟩ :: l) = some v

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
⊢ getValue? a (⟨k, v⟩ :: l) = some v

Tactic:
simp [getValue?, h]

Result:
no goals