harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
theorem norm_toContinuousLinearMap [Nontrivial E] [RingHomIsometric σ₁₂] (f : E →ₛₗᵢ[σ₁₂] F) :
    ‖f.toContinuousLinearMap‖ = 1 :=
  f.toContinuousLinearMap.homothety_norm <| by simp

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : Nontrivial E
inst✝ : RingHomIsometric σ₁₂
f : E →ₛₗᵢ[σ₁₂] F
⊢ ∀ (x : E), ‖f.toContinuousLinearMap x‖ = 1 * ‖x‖

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma leftRightHomologyComparison'_naturality (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData)
    (h₂ : S₁.RightHomologyData) (h₁' : S₂.LeftHomologyData) (h₂' : S₂.RightHomologyData) :
    leftHomologyMap' φ h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' =
      leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' φ h₂ h₂'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₁.RightHomologyData
h₁' : S₂.LeftHomologyData
h₂' : S₂.RightHomologyData
⊢ leftHomologyMap' φ h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' φ h₂ h₂'

Tactic:
simp only [← cancel_epi h₁.π, ← cancel_mono h₂'.ι, assoc,
  leftHomologyπ_naturality'_assoc, rightHomologyι_naturality',
  π_leftRightHomologyComparison'_ι, π_leftRightHomologyComparison'_ι_assoc,
  cyclesMap'_i_assoc, p_opcyclesMap']

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

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

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

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_C_mul_X_sub_C_of_IsUnit (b : R) (a : Rˣ) : (C (a : R) * X - C b).roots =
    {a⁻¹ * b}

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}

Tactic:
exact roots_X_sub_C (a⁻¹ * b)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (C ↑a * X - C b).roots = {↑a⁻¹ * b}

Tactic:
rw [← roots_C_mul _ (Units.ne_zero a⁻¹), mul_sub, ← mul_assoc, ← C_mul, ← C_mul,
  Units.inv_mul, C_1, one_mul]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
b : R
a : Rˣ
⊢ (X - C (↑a⁻¹ * b)).roots = {↑a⁻¹ * b}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldl_loop_lt (f : α → Fin n → α) (x) (h : i < n) :
    foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i+1)

Proof state:
α : Sort u_1
n i : Nat
f : α → Fin n → α
x : α
h : i < n
⊢ foldl.loop n f x i = foldl.loop n f (f x ⟨i, h⟩) (i + 1)

Tactic:
rw [foldl.loop, dif_pos h]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem not_bddAbove_iff {α : Type*} [LinearOrder α] {s : Set α} :
    ¬BddAbove s ↔ ∀ x, ∃ y ∈ s, x < y

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ ¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y

Tactic:
simp only [not_bddAbove_iff', not_le]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive exists_pos_norm_le]
lemma Bornology.IsBounded.exists_pos_norm_le' (hs : IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R :=
  let ⟨R₀, hR₀⟩ := hs.exists_norm_le'
  ⟨max R₀ 1, by positivity, fun x hx => (hR₀ x hx).trans <| le_max_left _ _⟩

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
hs : IsBounded s
R₀ : ℝ
hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀
⊢ R₀ ⊔ 1 > 0

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂)

Proof state:
α : Sort u
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ (a₁ = b₁) = (a₂ = b₂)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_sup : a ∆ b = a ⊔ b ↔ Disjoint a b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b

Tactic:
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b

Tactic:
exact h.of_disjoint_inf_of_le le_sup_left

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b

Tactic:
refine ⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
-- Mathlib/Algebra/Order/Module/Defs.lean
@[simp]
lemma smul_pos_iff_of_pos_left [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
    0 < a • b ↔ 0 < b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulZeroClass α β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ 0 < a • b ↔ 0 < b

Tactic:
simpa only [smul_zero] using smul_lt_smul_iff_of_pos_left ha (b₁ := 0) (b₂ := b)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ _k ∈ range n, b

Proof state:
β : Type u_4
inst✝ : CommMonoid β
b : β
⊢ ∀ (n : ℕ), b ^ n = ∏ _k ∈ range n, b

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem mul_leftInvEquiv_symm (x : S) : (x : M) * (S.leftInvEquiv hS).symm x = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑x * ↑((S.leftInvEquiv hS).symm x) = 1

Tactic:
convert S.leftInvEquiv_mul hS ((S.leftInvEquiv hS).symm x)

Result:
case h.e'_2.h.e'_5.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ x = (S.leftInvEquiv hS) ((S.leftInvEquiv hS).symm x)

Proof state:
case h.e'_2.h.e'_5.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ x = (S.leftInvEquiv hS) ((S.leftInvEquiv hS).symm x)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_mul_left_add_left (m n k : ℕ) : Coprime (n * k + m) n ↔ Coprime m n

Proof state:
m n k : ℕ
⊢ (n * k + m).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_mul_left_add_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_append_left' (l₁ : Vector α m) {l₂ : Vector α n} {i : Nat} (hi : i < m) :
    l₁[i] = (l₁ ++ l₂)[i]

Proof state:
α : Type u_1
m n : Nat
l₁ : Vector α m
l₂ : Vector α n
i : Nat
hi : i < m
⊢ l₁[i] = (l₁ ++ l₂)[i]

Tactic:
rw [getElem_append_left] <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma measure_inter_conull (ht : μ tᶜ = 0) : μ (s ∩ t) = μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : μ tᶜ = 0
⊢ μ (s ∩ t) = μ s

Tactic:
rw [← diff_compl, measure_diff_null ht]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem nontrivial_of_einfsep_lt_top (hs : s.einfsep < ∞) : s.Nontrivial

Proof state:
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.einfsep < ⊤
⊢ s.Nontrivial

Tactic:
rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.einfsep < ⊤
w✝¹ : α
hx : w✝¹ ∈ s
w✝ : α
hy : w✝ ∈ s
hxy : w✝¹ ≠ w✝
right✝ : edist w✝¹ w✝ < ⊤
⊢ s.Nontrivial

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.einfsep < ⊤
w✝¹ : α
hx : w✝¹ ∈ s
w✝ : α
hy : w✝ ∈ s
hxy : w✝¹ ≠ w✝
right✝ : edist w✝¹ w✝ < ⊤
⊢ s.Nontrivial

Tactic:
exact ⟨_, hx, _, hy, hxy⟩

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
lemma δ_comp_δ'_apply {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : Fin.castSucc i < j)
    (x : S _⦋n + 2⦌) : S.δ i (S.δ j x) =
      S.δ (j.pred fun (hj : j = 0) => by simp [hj, Fin.not_lt_zero] at H) (S.δ i.castSucc x) :=
  congr_fun (S.δ_comp_δ' H) x

Proof state:
S : SSet
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
x : S _⦋n + 2⦌
hj : j = 0
⊢ False

Tactic:
simp [hj, Fin.not_lt_zero] at H

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_bot : a ⇔ ⊥ = aᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇔ ⊥ = aᶜ

Tactic:
simp [bihimp]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem LocallyConvexSpace.ofBasisZero {ι : Type*} (b : ι → Set E) (p : ι → Prop)
    (hbasis : (𝓝 0).HasBasis p b) (hconvex : ∀ i, p i → Convex 𝕜 (b i)) :
    LocallyConvexSpace 𝕜 E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : (𝓝 0).HasBasis p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ (𝓝 x).HasBasis ((fun x => p) x) ((fun x i => (fun x_1 => x + x_1) '' b i) x)

Tactic:
rw [← map_add_left_nhds_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : (𝓝 0).HasBasis p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ (map (fun x_1 => x + x_1) (𝓝 0)).HasBasis ((fun x => p) x) ((fun x i => (fun x_1 => x + x_1) '' b i) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : (𝓝 0).HasBasis p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ (map (fun x_1 => x + x_1) (𝓝 0)).HasBasis ((fun x => p) x) ((fun x i => (fun x_1 => x + x_1) '' b i) x)

Tactic:
exact hbasis.map _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Continuum.lean
theorem continuum_le_lift {c : Cardinal.{u}} : 𝔠 ≤ lift.{v} c ↔ 𝔠 ≤ c

Proof state:
c : Cardinal.{u}
⊢ 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c

Tactic:
rw [← lift_continuum.{v, u}, lift_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem containsThenInsert_fst (h : m.WF) {k : α} {v : β k} :
    (m.containsThenInsert k v).1 = m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝¹ : BEq α
inst✝ : Hashable α
h : m.WF
k : α
v : β k
⊢ (m.containsThenInsert k v).fst = m.contains k

Tactic:
simp_to_raw using Raw₀.containsThenInsert_fst

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem forall_coeff_eq_zero (φ : R⟦X⟧) : (∀ n, coeff R n φ = 0) ↔ φ = 0 :=
  ⟨fun h => ext h, fun h => by simp [h]⟩

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : φ = 0
⊢ ∀ (n : ℕ), (coeff R n) φ = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_C (r : R) :
    m.degree (C r) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
⊢ m.degree (C r) = 0

Tactic:
rw [degree_eq_zero_iff_totalDegree_eq_zero, totalDegree_C]

Result:
no goals
-- Mathlib/Computability/TuringMachine.lean
theorem trStmts₁_run {k : K} {s : StAct K Γ σ k} {q : TM2.Stmt Γ Λ σ} :
open scoped Classical in
    trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q

Tactic:
cases s <;> simp only [trStmts₁, stRun]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem loopyOn_empty (α : Type*) : loopyOn (∅ : Set α) = emptyOn α

Proof state:
α : Type u_2
⊢ loopyOn ∅ = emptyOn α

Tactic:
rw [← ground_eq_empty_iff, loopyOn_ground]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem generate_eq_biInf (S : Set (Set α)) : generate S = ⨅ s ∈ S, 𝓟 s :=
  eq_of_forall_le_iff fun f => by simp [le_generate_iff, le_principal_iff, subset_def]

Proof state:
α : Type u
S : Set (Set α)
f : Filter α
⊢ f ≤ generate S ↔ f ≤ ⨅ s ∈ S, 𝓟 s

Tactic:
simp [le_generate_iff, le_principal_iff, subset_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_setIfInBounds (as : Array α) (i : Nat) (h : i < as.size) (a : α) :
    a ∈ as.setIfInBounds i a

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ a ∈ as.setIfInBounds i a

Tactic:
simp [mem_iff_getElem]

Result:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ ∃ i_1 h, (as.setIfInBounds i a)[i_1] = a

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ ∃ i_1 h, (as.setIfInBounds i a)[i_1] = a

Tactic:
exact ⟨i, (by simpa using h), by simp⟩

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ (as.setIfInBounds i a)[i] = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
a : α
⊢ i < as.size

Tactic:
simpa using h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_lift_add_lift {a : Cardinal.{u}} {b : Cardinal.{v}} (ha : a < ℵ₀) (hb : b < ℵ₀) :
    toNat (lift.{v} a + lift.{u} b) = toNat a + toNat b

Proof state:
a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ toNat (lift.{v, u} a + lift.{u, v} b) = toNat a + toNat b

Tactic:
simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean
theorem whiskerRight_naturality (f : a ⟶ b) (g : G.obj b ⟶ a') :
    F.map f ◁ Γ.app b ▷ g ≫ (α_ _ _ _).inv ≫ θ.naturality f ▷ g =
      (α_ _ _ _).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G : OplaxFunctor B C
η θ : F ⟶ G
Γ : Modification η θ
a b : B
a' : C
f : a ⟶ b
g : G.obj b ⟶ a'
⊢ F.map f ◁ Γ.app b ▷ g ≫ (α_ (F.map f) (θ.app b) g).inv ≫ θ.naturality f ▷ g =
    (α_ (F.map f) (η.app b) g).inv ≫ η.naturality f ▷ g ≫ Γ.app a ▷ G.map f ▷ g

Tactic:
simp_rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight, naturality]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Filter.EventuallyEq.prodMap_nhds {α β : Type*} {f₁ f₂ : X → α} {g₁ g₂ : Y → β}
    {x : X} {y : Y} (hf : f₁ =ᶠ[𝓝 x] f₂) (hg : g₁ =ᶠ[𝓝 y] g₂) :
    Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
rw [nhds_prod_eq]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂

Tactic:
exact hf.prod_map hg

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma integrable_compProd_iff [SFinite μ] [IsSFiniteKernel κ] {E : Type*} [NormedAddCommGroup E]
    {f : α × β → E} (hf : AEStronglyMeasurable f (μ ⊗ₘ κ)) :
    Integrable f (μ ⊗ₘ κ) ↔
      (∀ᵐ x ∂μ, Integrable (fun y => f (x, y)) (κ x)) ∧
        Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂(κ x)) μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝² : SFinite μ
inst✝¹ : IsSFiniteKernel κ
E : Type u_3
inst✝ : NormedAddCommGroup E
f : α × β → E
hf : AEStronglyMeasurable f (μ ⊗ₘ κ)
⊢ Integrable f (μ ⊗ₘ κ) ↔
    (∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y)) (κ x)) ∧ Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂κ x) μ

Tactic:
simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply,
  Kernel.const_apply]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem length_le_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
    s.length h ≤ n ↔ s.TerminatedAt n

Proof state:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ ∃ h, s.length h ≤ n

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ s.TerminatedAt n

Tactic:
rw [← length_le_iff']

Result:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length h ≤ n ↔ ∃ h, s.length h ≤ n
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
@[simp] lemma cfc_apply_one {f : R → R} : cfc f (1 : A) = algebraMap R A (f 1)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
⊢ cfc f 1 = (algebraMap R A) (f 1)

Tactic:
simpa using cfc_algebraMap (A := A) 1 f

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma normEDS_two : normEDS b c d 2 = b

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 2 = b

Tactic:
erw [normEDS_ofNat, preNormEDS'_two, one_mul, if_pos even_two]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma sinKernel_neg (a : UnitAddCircle) (x : ℝ) :
    sinKernel (-a) x = -sinKernel a x

Proof state:
a : UnitAddCircle
x : ℝ
⊢ sinKernel (-a) x = -sinKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
| H a => simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, sinKernel_def, jacobiTheta₂'_neg_left,
    neg_div]

Result:
no goals

Proof state:
case H
x a : ℝ
⊢ sinKernel (-↑a) x = -sinKernel (↑a) x

Tactic:
simp [← ofReal_inj, ← QuotientAddGroup.mk_neg, sinKernel_def, jacobiTheta₂'_neg_left,
neg_div]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
theorem exists_vecMul_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
    {M : Matrix n n A} : (∃ v ≠ 0, v ᵥ* M = 0) ↔ M.det = 0

Proof state:
n : Type u_1
inst✝³ : Fintype n
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∃ v, v ≠ 0 ∧ v ᵥ* M = 0) ↔ M.det = 0

Tactic:
simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombinationLineMapWeights_apply_left [DecidableEq ι] {i j : ι} (h : i ≠ j) (c : k) :
    affineCombinationLineMapWeights i j c i = 1 - c

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c i = 1 - c

Tactic:
simp [affineCombinationLineMapWeights, h.symm, sub_eq_neg_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
lemma coeff_det_one_add_X_smul_one (M : Matrix n n R) :
    (det (1 + (X : R[X]) • M.map C)).coeff 1 = trace M

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ (1 + X • M.map ⇑C).det.coeff 1 = M.trace

Tactic:
simp only [← derivative_det_one_add_X_smul, ← coeff_zero_eq_eval_zero,
  coeff_derivative, zero_add, Nat.cast_zero, mul_one]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_mul_of_div_eq (h : a / c = b) : a = b * c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a / c = b
⊢ a = b * c

Tactic:
simp [← h]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem integral_normed_smul {X} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [CompleteSpace X] (z : X) : ∫ x, f.normed μ x • z ∂μ = z

Proof state:
E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : HasContDiffBump E
inst✝⁷ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝⁶ : BorelSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : IsLocallyFiniteMeasure μ
inst✝³ : μ.IsOpenPosMeasure
X : Type u_2
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : CompleteSpace X
z : X
⊢ ∫ (x : E), f.normed μ x • z ∂μ = z

Tactic:
simp_rw [integral_smul_const, f.integral_normed (μ := μ), one_smul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem darts_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) :
    (p.concat h).darts = p.darts.concat ⟨(v, w), h⟩

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ (p.concat h).darts = p.darts.concat { toProd := (v, w), adj := h }

Tactic:
induction p <;> simp [*, concat_nil]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem mem_foldr_permutationsAux2 {t : α} {ts : List α} {r L : List (List α)} {l' : List α} :
    l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔
      l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a ∈ L, ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ flatMap (fun y => (permutationsAux2 t ts [] y id).2) L ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_flatMap,
  append_assoc, cons_append, exists_prop]

Result:
no goals

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
have :
  (∃ a : List α,
      a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
  ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ =>
    ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩

Result:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a ∈ L, ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a ∈ L, ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
rw [foldr_permutationsAux2]

Result:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a ∈ L, ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ flatMap (fun y => (permutationsAux2 t ts [] y id).2) L ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma zero :
    (0 : End R M).invtSubmodule = ⊤ :=
  eq_top_iff.mpr fun x ↦ by simp [invtSubmodule]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : Submodule R M
⊢ x ∈ ⊤ → x ∈ invtSubmodule 0

Tactic:
simp [invtSubmodule]

Result:
no goals